Struct move_stackless_bytecode::global_invariant_analysis::PerFunctionRelevance

pub struct PerFunctionRelevance {
    pub entrypoint_assumptions: BTreeMap<GlobalId, PerBytecodeRelevance>,
    pub per_bytecode_assertions: BTreeMap<CodeOffset, BTreeMap<GlobalId, PerBytecodeRelevance>>,
    pub exitpoint_assertions: BTreeMap<GlobalId, PerBytecodeRelevance>,
    pub ghost_type_param_count: usize,
}

A named struct for holding the information on how invariants are relevant to a function.

Fields

entrypoint_assumptions: BTreeMap<GlobalId, PerBytecodeRelevance>

Invariants that needs to be assumed at function entrypoint

• Key: global invariants that needs to be assumed before the first instruction,
• Value: the instantiation information per each related invariant.

per_bytecode_assertions: BTreeMap<CodeOffset, BTreeMap<GlobalId, PerBytecodeRelevance>>

For each bytecode at given code offset, the associated value is a map of

• Key: global invariants that needs to be asserted after the bytecode instruction and
• Value: the instantiation information per each related invariant.

exitpoint_assertions: BTreeMap<GlobalId, PerBytecodeRelevance>

Invariants that needs to be asserted at function exitpoint

• Key: global invariants that needs to be assumed before the first instruction,
• Value: the instantiation information per each related invariant.

ghost_type_param_count: usize

Number of ghost type parameters introduced in order to instantiate all asserted invariants

Trait Implementations

impl Clone for PerFunctionRelevance

fn clone(&self) -> PerFunctionRelevance

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.