pub struct InvariantAnalysisData {
pub fun_set_with_inv_check_on_exit: BTreeSet<QualifiedId<FunId>>,
pub fun_set_with_no_inv_check: BTreeSet<QualifiedId<FunId>>,
pub fun_to_inv_map: BTreeMap<QualifiedId<FunId>, InvariantRelevance>,
}
Expand description
Analysis info saved for the global_invariant_instrumentation phase
Fields
fun_set_with_inv_check_on_exit: BTreeSet<QualifiedId<FunId>>
Functions which have invariants checked on return instead of in body
fun_set_with_no_inv_check: BTreeSet<QualifiedId<FunId>>
Functions which invariants checking is turned-off anywhere in the function
fun_to_inv_map: BTreeMap<QualifiedId<FunId>, InvariantRelevance>
A mapping from function to the set of global invariants used and modified, respectively
Auto Trait Implementations
impl RefUnwindSafe for InvariantAnalysisData
impl Send for InvariantAnalysisData
impl Sync for InvariantAnalysisData
impl Unpin for InvariantAnalysisData
impl UnwindSafe for InvariantAnalysisData
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