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