Struct 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<(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.