Struct Allocation 

pub(crate) struct Allocation<'z3, 'tcx> {
    pub base: Int<'z3>,
    pub size: Int<'z3>,
    pub align: Int<'z3>,
    pub element_ty: ElementTy<'tcx>,
    pub kind: AllocKind<'z3>,
    pub facts: AllocFacts<'z3, 'tcx>,
    pub parent: Option<AllocId>,
}

A memory allocation: a stack local, a heap object (Box/Vec), or an external raw-pointer placeholder.

The allocation is stored in a MemoryUnit at index AllocId.0 (an AllocId is a monotonic counter that doubles as the vector index).

Fields

base: Int<'z3>

Base address (fresh Z3 constant).

size: Int<'z3>

Size in bytes (Z3 term, may be symbolic).

align: Int<'z3>

Alignment in bytes (Z3 term, may be symbolic for a generic element type).

element_ty: ElementTy<'tcx>

Type of the allocation’s contents (concrete Ty or symbolic Generic).

kind: AllocKind<'z3>

The allocation shape (object vs slice vs external).

facts: AllocFacts<'z3, 'tcx>

Cross-cutting per-allocation facts (dead/liveness/for_each), kept apart from the shape metadata above.

parent: Option<AllocId>

The allocation a sub-view was derived from: a slice view created by s[i..j] / s.get(range), split_at / align_to / as_chunks, or from_raw_parts. Each view is a fresh AllocId but a window onto the same memory as its source, so root_alloc follows this edge to group aliasing views. The address linkage back to the source lives in the pointer term (parent_term + offset) and provenance offset, not in base arithmetic.

Implementations

impl<'z3, 'tcx> Allocation<'z3, 'tcx>

pub(crate) fn new( base: Int<'z3>, size: Int<'z3>, align: Int<'z3>, element_ty: Option<Ty<'tcx>>, kind: AllocKind<'z3>, ) -> Self

Construct a fresh allocation with all live/dead/invariant flags in their initial state.

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

Whether this allocation models an external raw-pointer parameter.

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

The slice/array element count, if this allocation is slice data.

Invariant: size == len * sizeof(element_ty) is maintained by the callers that call Self::set_slice_len (they compute size from the same len and push the equality as a path condition); it is not enforced here. slice_len_from_value falls back to size / elem_size when the length was never materialized.

pub(crate) fn set_slice_len(&mut self, len: Int<'z3>)

Mark this allocation as slice data with the given element count. Callers must keep size == len * sizeof(element_ty) consistent.

Trait Implementations

impl<'z3, 'tcx> Clone for Allocation<'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 Allocation<'z3, 'tcx>

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

Formats the value using the given formatter.