Struct Allocation 

pub struct Allocation<'ctx, 'tcx> {
    pub base: Int<'ctx>,
    pub size: Int<'ctx>,
    pub align: u64,
    pub element_ty: Option<Ty<'tcx>>,
    pub is_external: bool,
    pub dead: bool,
    pub initialized: bool,
    pub alive_assumed: bool,
    pub nul_terminated: bool,
    pub parent: Option<AllocId>,
    pub slice_data: Option<AllocId>,
}

A memory allocation (stack or heap).

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

Fields

base: Int<'ctx>

Base address (fresh Z3 constant).

size: Int<'ctx>

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

align: u64

Alignment in bytes.

element_ty: Option<Ty<'tcx>>

Element type for bounds checking.

is_external: bool

True if this allocation models an external raw-pointer parameter whose exact size and nullability are unknown.

dead: bool

Allocations that have been freed (StorageDead, Drop).

initialized: bool

Allocations that have been written to (initialized via write/MaybeUninit).

alive_assumed: bool

Allocations assumed alive via contract (e.g. #[rapx::requires(Alive(ptr))]).

nul_terminated: bool

Allocations known to be a null-terminated byte buffer (a valid C string), asserted via a ValidCStr contract fact or struct invariant.

parent: Option<AllocId>

Parent allocation for sub-allocations created by split_at / from_raw_parts.

slice_data: Option<AllocId>

Slice data allocation: for a &[T] reference’s stack allocation, the symbolic data allocation created for the slice contents.

Trait Implementations

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

fn clone(&self) -> Allocation<'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 Allocation<'ctx, 'tcx>

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

Formats the value using the given formatter.