Struct move_stackless_bytecode_interpreter::concrete::evaluator::Evaluator

pub struct Evaluator<'env> { /* private fields */ }

Implementations

impl<'env> Evaluator<'env>

pub fn new(
    holder: &'env FunctionTargetsHolder,
    target: &'env FunctionTarget<'env>,
    ty_args: &'env [BaseType],
    level: usize,
    exp_state: ExpState,
    eval_state: &'env EvalState,
    local_state: &'env LocalState,
    global_state: &'env GlobalState
) -> Self

pub fn check_assert(&self, exp: &Exp)

Check whether an assert expression holds

pub fn check_assume(
    &self,
    exp: &Exp
) -> Option<EvalResult<(TempIndex, TypedValue)>>

Check whether an assume expression holds, unless the assume expression represents a let binding. In that case, return the TypedValue of the let-binding as well as the local variable (index) the value should bind to.