Struct Provenance 

pub(crate) struct Provenance<'z3> {
    pub alloc_id: AllocId,
    pub offset: Int<'z3>,
    pub offset_kind: Option<OffsetKind<'z3>>,
}

Pointer provenance: which allocation, at what byte offset, and (when known) what structure that offset has.

Fields

alloc_id: AllocId

The allocation this pointer derives from.

offset: Int<'z3>

Byte offset from the allocation base (always present). A freshly created pointer to the base of an allocation has offset = 0.

offset_kind: Option<OffsetKind<'z3>>

The offset’s structure. None means the pointer sits at the base (offset == 0) with no further structure; Some(..) records whether the offset is a compile-time field offset (Field), an element index from element-strided arithmetic (Element), or a byte-strided offset (Byte).

Trait Implementations

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

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

Formats the value using the given formatter.