pub struct InvariantAnalysisData {
pub target_fun_ids: BTreeSet<QualifiedId<FunId>>,
pub dep_fun_ids: BTreeSet<QualifiedId<FunId>>,
pub disabled_inv_fun_set: BTreeSet<QualifiedId<FunId>>,
pub non_inv_fun_set: BTreeSet<QualifiedId<FunId>>,
pub target_invariants: BTreeSet<GlobalId>,
pub funs_that_modify_inv: BTreeMap<GlobalId, BTreeSet<QualifiedId<FunId>>>,
pub invs_modified_by_fun: BTreeMap<QualifiedId<FunId>, BTreeSet<GlobalId>>,
pub funs_that_modify_some_inv: BTreeSet<QualifiedId<FunId>>,
pub funs_that_delegate_to_caller: BTreeSet<QualifiedId<FunId>>,
pub friend_fun_ids: BTreeSet<QualifiedId<FunId>>,
pub disabled_invs_for_fun: BTreeMap<QualifiedId<FunId>, BTreeSet<GlobalId>>,
}
Fields§
§target_fun_ids: BTreeSet<QualifiedId<FunId>>
The set of all functions in target module.
dep_fun_ids: BTreeSet<QualifiedId<FunId>>
Functions in dependent modules that are transitively called by functions in target module.
disabled_inv_fun_set: BTreeSet<QualifiedId<FunId>>
functions where invariants are disabled by pragma disable_invariants_in_body
non_inv_fun_set: BTreeSet<QualifiedId<FunId>>
Functions where invariants are disabled in a transitive caller, or by pragma delegate_invariant_to_caller
target_invariants: BTreeSet<GlobalId>
global and update invariants in the target module
funs_that_modify_inv: BTreeMap<GlobalId, BTreeSet<QualifiedId<FunId>>>
Maps invariant ID to set of functions that modify the invariant Does not include update invariants
invs_modified_by_fun: BTreeMap<QualifiedId<FunId>, BTreeSet<GlobalId>>
Maps function to the set of invariants that it modifies Does not include update invariants
funs_that_modify_some_inv: BTreeSet<QualifiedId<FunId>>
Functions that modify some invariant in the target Does not include update invariants
funs_that_delegate_to_caller: BTreeSet<QualifiedId<FunId>>
functions that are in non_inv_fun_set and M[I] for some I. We have to verify the callers, which may be in friend modules.
friend_fun_ids: BTreeSet<QualifiedId<FunId>>
Functions that are not in target or deps, but that call a function in non_inv_fun_set that modifies some invariant from target module and eventually calls a function in target mod or a dependency.
disabled_invs_for_fun: BTreeMap<QualifiedId<FunId>, BTreeSet<GlobalId>>
For each function, give the set of invariants that are disabled in that function. This is defined as the least set satisfying set inequalities: (1) in a function where invariants are disabled, it is the set of invariants modified in the function, and (2) in a function in non_inv_fun_set, it is the least set that includes all disabled_invs for calling functions.