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

contains_hazard 🔒

Whether any atom in this (possibly compound) property is a hazard (ContractKind::Hazard), which the caller explicitly opts into.

pow2_factor 🔒

Largest power-of-two factor of a non-negative constant (the alignment implied by multiplying by c): c itself if it is a power of two, otherwise 2^trailing_zeros(c).

rebind_expr_place 🔒

rebind_property_place 🔒

Rebind every self place in a struct invariant to the given MIR local, so an invariant parsed against the struct’s own self can be asserted on a freshly-created reference (&*NonNull<T> → &T).

resolve_u64_from_place_key 🔒

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