Struct LinkedItemGraph 

pub struct LinkedItemGraph { /* private fields */ }

A graph of items connected via the hax attribute AttrPayload::AssociatedItem and UUIDs.

Implementations

impl LinkedItemGraph

pub fn new(items: &[Item], context: Context) -> Self

Clone items marked with UUIDs attributes to build a graph of linked items. This graph clones the items that represent linked items: e.g. pre and post conditions.

pub fn linked_items_iter( &self, item: &impl HasMetadata, ) -> impl Iterator<Item = (AssociationRole, Result<&Item, DiagnosticInfo>)>

Given a graph and an item item, returns an iterator of the various items that are linked with item.

pub fn linked_items( &self, item: &impl HasMetadata, ) -> HashMap<AssociationRole, Vec<Result<&Item, DiagnosticInfo>>>

Returns the items linked to a given item.

pub fn fn_like_linked_expressions( &self, item: &impl HasMetadata, self_id: Option<LocalId>, ) -> FnLikeAssocatedExpressions

Returns the precondition, postcondition and decreases clause, if any, for a given item. When operating on a linked function, self_id is the local identifier of self.

pub fn has_spec(&self, item: &Item) -> bool

Is there a specification that we should prove for this item?

Trait Implementations

impl Clone for LinkedItemGraph

fn clone(&self) -> LinkedItemGraph

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LinkedItemGraph

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for LinkedItemGraph

fn default() -> Self

Returns the “default value” for a type.