Trait veriwasm::checkers::Checker

pub trait Checker<State: Lattice + Clone> {
    fn check(&self, result: AnalysisResult<State>) -> bool;
    fn irmap(&self) -> &IRMap;
    fn aexec(&self, state: &mut State, ir_stmt: &Stmt, loc: &LocIdx);
    fn check_statement(
        &self, 
        state: &State, 
        ir_stmt: &Stmt, 
        loc_idx: &LocIdx
    ) -> bool;

    fn check_state_at_statements(&self, result: AnalysisResult<State>) -> bool { ... }
}

Required methods

fn check(&self, result: AnalysisResult<State>) -> bool

fn irmap(&self) -> &IRMap

fn aexec(&self, state: &mut State, ir_stmt: &Stmt, loc: &LocIdx)

fn check_statement(
    &self,
    state: &State,
    ir_stmt: &Stmt,
    loc_idx: &LocIdx
) -> bool

Provided methods

fn check_state_at_statements(&self, result: AnalysisResult<State>) -> bool

Implementors

impl Checker<VariableState<SlotVal>> for LocalsChecker<'_>