Struct bytecode::global_invariant_analysis::PerFunctionRelevance

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

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.

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.