Enum AllocKind 

pub(crate) enum AllocKind<'z3> {
    Object,
    Slice {
        len: Int<'z3>,
    },
    External,
}

The shape of an allocation: a single object, a slice/array buffer, or an external raw-pointer parameter. element_ty (typed vs untyped) and the parent sub-view edge stay separate fields.

Variants

Object

A single object: a Box<T> heap object, a struct, a scalar, or an untyped raw buffer.

Slice

A slice/array buffer with a known element count.

Fields

len: Int<'z3>

External

An external raw-pointer parameter. size is an unconstrained symbolic term (the caller may pass any allocation); nullability is not stored here — it is tracked via the pointer term (term == 0) path conditions.

Trait Implementations

impl<'z3> Clone for AllocKind<'z3>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'z3> Debug for AllocKind<'z3>

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

Formats the value using the given formatter.