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
Auto Trait Implementations
impl RefUnwindSafe for InvariantRelevance
impl Send for InvariantRelevance
impl Sync for InvariantRelevance
impl Unpin for InvariantRelevance
impl UnwindSafe for InvariantRelevance
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more