Module state 

Symbolic VM state types.

Core data structures that represent the symbolic execution state: VmValue (symbolic value with invariants), Allocation (memory object), and VmState (the full execution state at a program point).

Structs

AllocId

Unique identifier for a heap or stack allocation.

Allocation

A memory allocation (stack or heap).

ByteInfo 🔒

Per-byte symbolic state at a concrete offset in an allocation.

ContractFlags 🔒

One-shot execution/contract flags accumulated while stepping a path.

InlineFrame 🔒

A saved caller context pushed during cross-function inline. Nested inlining (a callee that itself inlines another callee) pushes multiple frames; a single Option slot would clobber the outer caller’s context on the inner exit, so a stack is required.

Provenance

Pointer provenance: which allocation and at what byte offset.

ValueInvariants

Known invariants about a symbolic value.

VmState

The full symbolic execution state at a program point.

VmValue

A symbolic value tracked by the VM.