Expand description
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.
- 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.
- state
- Symbolic VM state types.
Structs§
- Symbolic
Vm - Entry point for symbolic MIR execution.