Module exec 

MIR statement and terminator executors for the symbolic VM.

Each executor is a transfer function that updates VmState based on the semantics of a MIR construct. The VM walks retained MIR items in forward path order, calling these executors.

Functions

chosen_successor 🔒

Return the next MIR block after block in a finite verification path.

resolve_u64_from_place_key 🔒

Try to resolve a u64 constant from a PlaceKey’s source in the VM state.