Struct SymbolicVm 

pub(crate) struct SymbolicVm;

Entry point for symbolic MIR execution.

Stateless: the inputs to a run (the Z3 context, compiler type context, and the sliced program) are passed to [run], so this struct carries no state of its own.

Implementations

impl SymbolicVm

pub(crate) fn new() -> Self

Create a symbolic VM.

pub(crate) fn run<'z3, 'tcx>( &self, z3_ctx: &'z3 Context, tcx: TyCtxt<'tcx>, goal: ProofGoal<'tcx>, ) -> VmState<'z3, 'tcx>

Run the sliced program goal (the path and its retained MIR items) and produce the resulting symbolic state.

The Z3 context is borrowed (not owned) so a single context can be reused across property checks; run is a pure input -> state mapping — the program to execute (goal) is consumed here and is never stored in the returned VmState.