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

Implementations

impl PerFunctionRelevance

This impl block contains no items.

This impl block is about the analysis pass

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.