Struct SymbolicVm 

pub struct SymbolicVm<'tcx> {
    tcx: TyCtxt<'tcx>,
}

Entry point for symbolic MIR execution.

Stateless wrapper around a TyCtxt; creates VmState instances for each path by executing retained MIR items.

Fields

tcx: TyCtxt<'tcx>

Implementations

impl<'tcx> SymbolicVm<'tcx>

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

Create a symbolic VM for the given compiler context.

pub fn execute<'ctx>( &self, ctx: &'ctx Context, items: &ProofGoal<'tcx>, ) -> VmState<'ctx, 'tcx>

Execute retained MIR items and produce a symbolic VM state.

The ctx parameter provides a shared Z3 context; the resulting VmState borrows it so that a single context can be reused across property checks.