pub struct InvariantRelevance {
pub accessed: BTreeSet<GlobalId>,
pub modified: BTreeSet<GlobalId>,
pub direct_accessed: BTreeSet<GlobalId>,
pub direct_modified: BTreeSet<GlobalId>,
}
Expand description
A named tuple for holding the information on how an invariant is relevant to a function.
Fields§
§accessed: BTreeSet<GlobalId>
Global invariants covering memories that are accessed in a function
modified: BTreeSet<GlobalId>
Global invariants covering memories that are modified in a function
direct_accessed: BTreeSet<GlobalId>
Global invariants covering memories that are directly accessed in a function
direct_modified: BTreeSet<GlobalId>
Global invariants covering memories that are directly modified in a function