Struct VmValue 

pub(crate) struct VmValue<'z3, 'tcx> {
    pub z3_term: Int<'z3>,
    pub ty: Ty<'tcx>,
    pub provenance: Option<Provenance<'z3>>,
    pub facts: ValueFacts<'z3>,
    pub source: ValueSource<'z3>,
}

A symbolic value tracked by the VM.

Semantics of z3_term

• For pointer/reference types (&T, *const T, *mut T, Box<T>, etc.): z3_term represents the address in the VM’s logical address space.
• For scalar types (integers, bool, char): z3_term represents the value.
• For aggregate types (struct, tuple, enum): z3_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: z3_term == alloc[provenance.alloc_id].base + provenance.offset

Fields

z3_term: Int<'z3>

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

ty: Ty<'tcx>

Rust type, for layout queries.

provenance: Option<Provenance<'z3>>

Which allocation this pointer derives from and at what offset.

facts: ValueFacts<'z3>

Known constraints on this value.

source: ValueSource<'z3>

Extra semantics (field offset, discriminant, comparison, or binary-op source); see ValueSource.

Implementations

impl<'z3, 'tcx> VmValue<'z3, 'tcx>

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

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

Convenience: extract the AllocId from provenance, if any.

pub(crate) fn discriminant(&self) -> Option<&Int<'z3>>

Symbolic enum discriminant, if known.

pub(crate) fn bool_cond(&self) -> Option<&Bool<'z3>>

Direct boolean condition of a comparison result, if any.

pub(crate) fn is_field_offset(&self) -> bool

Whether this scalar is a compile-time offset_of! field offset.

pub(crate) fn is_pointer(&self) -> bool

Whether this value is a pointer (carries provenance).

Trait Implementations

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

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

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

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

Formats the value using the given formatter.