Module vm 

Symbolic MIR Virtual Machine.

This module replaces the pattern-matching ForwardVerifier with a semantic MIR executor. Instead of deriving ad-hoc StateFacts from MIR patterns, the VM executes retained MIR items and directly builds symbolic state (VmState) with Z3 terms for every value.

Modules

alias 🔒

VM-specific alias origin tracing.

alias_hazard 🔒

MIR-level alias hazard scanning for the symbolic VM backend.

alias_tree 🔒

Per-function alias derivation forest, used only for field-path resolution.

call 🔒

Call handling for the symbolic VM.

display 🔒

Debug and diagnostic display for the symbolic VM.

exec 🔒

MIR statement and terminator executors for the symbolic VM.

memory 🔒

Symbolic memory model for the VM.

region 🔒

Region (lifetime) helpers shared by the VM and the property checker.

state 🔒

Symbolic VM state types.

Structs

SymbolicVm 🔒

Entry point for symbolic MIR execution.