Struct AllocFacts 

pub(crate) struct AllocFacts<'z3, 'tcx> {
    pub dead: bool,
    pub liveness: Option<Region<'tcx>>,
    pub for_each: ForEachFacts<'z3, 'tcx>,
}

Per-allocation lifecycle facts (dead/liveness/for_each), kept apart from the allocation’s shape metadata and parent edge so identity/layout and facts are separated at the type level. The content facts (readability, C-string/UTF-8 trust) live on ContentFacts instead.

Fields

dead: bool

Whether the allocation has been freed (StorageDead / Drop).

liveness: Option<Region<'tcx>>

The region this external allocation is assumed alive for, via an Alive(p, 'a) contract/invariant (or 'static for ValidCStr/Allocated params/'static data). Only consulted for external allocations, whose memory is owned by the caller (so dead carries no liveness guarantee): the checker rejects a use that demands a longer region than this. None means no assumption — an external allocation then fails Alive unless grounded in a live reference; a VM-owned allocation is alive while !dead and never sets this.

for_each: ForEachFacts<'z3, 'tcx>

Uniform facts about this allocation’s pointer elements, established by x.iter() for_each invariants (Typed/Align/Allocated).

Trait Implementations

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

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

Formats the value using the given formatter.

impl<'z3, 'tcx> Default for AllocFacts<'z3, 'tcx>

fn default() -> Self

Returns the “default value” for a type.