Struct PtrLive 

pub struct PtrLive<'a, T>(/* private fields */);

Evidence that a range of memory is alive.

This evidence enables taking pointer offsets (see PtrAddExt) without ownership of that range of memory (i.e., not using Perm).

Its lifetime is bounded by some &Perm<*const [T]> (via Perm::live or Perm::live_mut) so it can’t outlive the associated allocation.

Implementations

impl<T> PtrLive<'_, T>

pub fn ward(self) -> *const T

Base pointer, start of the range

logic(opaque)

pub fn len(self) -> usize

The number of elements (of type T) in the range.

The length in bytes is thus self.len()@ * size_of_logic::<T>().

logic(opaque)

pub fn contains_range(self, ptr: *const T, len: Int) -> bool

Range inclusion.

The live range self.ward()..=(self.ward() + self.len()) contains the range ptr..=(ptr + len).

Note that the out-of-bounds pointer self.ward() + self.len() is included. The provenance of ptr must be the same as self.ward().

logic(open, inline)

let offset = ptr.sub_logic(self.ward());
// This checks that the provenance is the same.
ptr == self.ward().offset_logic(offset)
&& 0 <= offset && offset <= self.len()@
&& 0 <= offset + len && offset + len <= self.len()@

Trait Implementations

impl<T> Clone for PtrLive<'_, T>

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

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

Performs copy-assignment from source.

impl<T> Invariant for PtrLive<'_, T>

fn invariant(self) -> bool

logic(open, prophetic)

/* Macro-generated */

impl<T> Copy for PtrLive<'_, T>