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

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Should always be Self

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.