Struct Provenance 

pub struct Provenance<'ctx> {
    pub alloc_id: AllocId,
    pub offset: Int<'ctx>,
    pub is_field_offset: bool,
}

Pointer provenance: which allocation and at what byte offset.

Fields

alloc_id: AllocId

The allocation this pointer derives from.

offset: Int<'ctx>

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

is_field_offset: bool

Whether offset is a compile-time field offset (offset_of!). Such an offset always satisfies 0 <= offset and offset + size_of(field) <= size_of(container), which the verifier uses to discharge in-bounds checks for patterns like Option::as_slice.

Trait Implementations

impl<'ctx> Clone for Provenance<'ctx>

fn clone(&self) -> Provenance<'ctx>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'ctx> Debug for Provenance<'ctx>

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

Formats the value using the given formatter.