Struct VerifyEngine 

pub struct VerifyEngine<'tcx> {
    slicer: BackwardSlicer<'tcx>,
    vm: SymbolicVm<'tcx>,
    checker: PropertyChecker,
}

Fields

slicer: BackwardSlicer<'tcx>

vm: SymbolicVm<'tcx>

checker: PropertyChecker

Implementations

impl<'tcx> VerifyEngine<'tcx>

pub fn new(tcx: TyCtxt<'tcx>) -> Self

fn new_z3_context() -> Context

pub fn check_callsite_from_tree( &self, tree: &PathTree, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, caller_contracts: &[Property<'tcx>], ) -> Vec<(CheckResult, String)>

fn callee_is_simple(tcx: TyCtxt<'_>, callee_def_id: DefId) -> bool

fn inject_inline_callees( &self, items: Vec<RelevantItem<'tcx>>, caller_def_id: DefId, depth: usize, ) -> Vec<RelevantItem<'tcx>>

Scan the relevant items for unsupported Call terminators whose callee has available MIR. For each such call, inject CalleeEntry + callee MIR items + CalleeExit, replacing the original terminator.

fn build_callee_items( &self, callee_def_id: DefId, depth: usize, ) -> Vec<RelevantItem<'tcx>>

Build a linear sequence of relevant items for a callee’s MIR body. Walks BFS from the entry block, collecting statements and terminators.

fn bind_property_to_checkpoint( property: &Property<'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> Property<'tcx>

fn rebind_place( place: &ContractPlace<'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> ContractPlace<'tcx>

fn rebind_contract_expr( expr: &ContractExpr<'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> ContractExpr<'tcx>

pub fn check_invariant_from_tree( &self, def_id: DefId, tree: &PathTree, checkpoint: CheckpointLocation, invariant: &Property<'tcx>, entry_facts: &[RelevantItem<'tcx>], ) -> Vec<(CheckResult, String)>