Struct VmValue 

pub struct VmValue<'ctx, 'tcx> {
    pub term: Int<'ctx>,
    pub ty: Ty<'tcx>,
    pub provenance: Option<Provenance<'ctx>>,
    pub invariants: ValueInvariants,
}

A symbolic value tracked by the VM.

Semantics of term

• For pointer/reference types (&T, *const T, *mut T, Box<T>, etc.): term represents the address in the VM’s logical address space.
• For scalar types (integers, bool, char): term represents the value.
• For aggregate types (struct, tuple, enum): term is the base address of the stack allocation backing the aggregate.

When provenance is Some, the following relationship holds and is asserted into the solver at check time: term == alloc[provenance.alloc_id].base + provenance.offset

Fields

term: Int<'ctx>

The Z3 integer term (address or scalar value, see struct docs).

ty: Ty<'tcx>

Rust type, for layout queries.

provenance: Option<Provenance<'ctx>>

Which allocation this pointer derives from and at what offset.

invariants: ValueInvariants

Known constraints on this value.

Implementations

impl<'ctx, 'tcx> VmValue<'ctx, 'tcx>

fn describe(&self) -> String

A compact one-line description of a symbolic value.

impl<'ctx, 'tcx> VmValue<'ctx, 'tcx>

pub fn new(term: Int<'ctx>, ty: Ty<'tcx>) -> Self

pub fn provenance_alloc_id(&self) -> Option<AllocId>

Convenience: extract the AllocId from provenance, if any.

Trait Implementations

impl<'ctx, 'tcx> Clone for VmValue<'ctx, 'tcx>

fn clone(&self) -> VmValue<'ctx, 'tcx>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'ctx, 'tcx> Debug for VmValue<'ctx, 'tcx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.