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
Implementations
impl InvariantRelevance
This impl block contains no items.
This impl block contains functions that are mostly utilities functions and are only relevant within this file.
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