Type Definition veriwasm::lattices::stackgrowthlattice::StackGrowthLattice

pub type StackGrowthLattice = ConstLattice<(i64, i64, i64)>;

Fields are: (stackgrowth, probestack, rbp_stackgrowth)

stackgrowth is a value that indicates how far downward the stack is valid.

rbp_stackgrowth is a copy of stackgrowth that is saved when rsp is copied to rbp during frame setup in the prologue. When rsp is restored from rbp in the epilogue, it is copied back.

Implementations

impl StackGrowthLattice

pub fn get_stackgrowth(&self) -> Option<i64>

pub fn get_probestack(&self) -> Option<i64>

pub fn get_rbp(&self) -> Option<i64>

Trait Implementations

impl VarState for StackGrowthLattice

type Var = i64

fn get(&self, _index: &Value) -> Option<Self::Var>

fn set(&mut self, _index: &Value, _v: Self::Var)

fn set_to_bot(&mut self, _index: &Value)

fn on_call(&mut self)

fn adjust_stack_offset(
    &mut self,
    _opcode: &Binopcode,
    _dst: &Value,
    _src1: &Value,
    _src2: &Value
)