Enum OffsetKind 

pub(crate) enum OffsetKind<'z3> {
    Field,
    Element(Int<'z3>),
    Byte,
}

The structure of a pointer’s byte offset, when it has one.

Each variant lets the verifier use a cheaper, more precise proof: Field carries the “field in-bounds” guarantee (offset + size_of(field) <= size_of(container), e.g. Option::as_slice), and Element(k) tracks the element index so InBound checks k + count <= slice_len linearly instead of the non-linear byte form (k+count)·S <= len·S (undecidable in Z3 NIA for a generic S).

Variants

Field

Compile-time field offset (offset_of!), including a first field at 0.

Element(Int<'z3>)

Element index from element-strided arithmetic (ptr.add(k)); the byte offset is element · S.

Byte

A byte-strided or otherwise unclassifiable offset (byte_add).

Trait Implementations

impl<'z3> Clone for OffsetKind<'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 OffsetKind<'z3>

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

Formats the value using the given formatter.