Struct VerifyEngine 

pub struct VerifyEngine<'tcx> {
    slicer: BackwardSlicer<'tcx>,
    verifier: ForwardVerifier<'tcx>,
    checker: SmtChecker<'tcx>,
}

Thin wrapper around the three-stage verification pipeline.

Each structural check (checkpoint or invariant) delegates to one of the two public methods; the engine handles visitor bookkeeping internally.

Fields

slicer: BackwardSlicer<'tcx>

verifier: ForwardVerifier<'tcx>

checker: SmtChecker<'tcx>

Implementations

impl<'tcx> VerifyEngine<'tcx>

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

Create an engine for the current compiler type context.

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

Run the invariant-check pipeline in bulk using a per-checkpoint path tree.

Calls visit_path_tree_for_checkpoint once, then forward + SMT per path. The tree already contains only paths reaching checkpoint; common prefixes are shared to avoid redundant backward analysis.

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

Run the checkpoint-check pipeline in bulk using a per-checkpoint path tree.

Calls visit_path_tree once, then forward + SMT per path.