Struct PointsToCopy item path

{ self.view().ptr }

The pointer that this permission is associated with.

{ self.view().opt_value }

The (possibly uninitialized) memory that this permission gives access to.

{ self.opt_value().is_init() }

Returns true if the permission’s associated memory is initialized.

{ self.opt_value().is_uninit() }

Returns true if the permission’s associated memory is uninitialized.

self.is_init(),

{ self.opt_value().value() }

If the permission’s associated memory is initialized, returns the value that the pointer points to. Otherwise, the result is meaningless.

size_of::<T>() != 0,

self@.ptr@.addr != 0,

Guarantee that the PointsTo for any non-zero-sized type points to a non-null address.

self.ptr() == old(self).ptr(),

self.is_uninit(),

“Forgets” about the value stored behind the pointer. Updates the PointsTo value to MemContents::Uninit. Note that this is a proof function, i.e., it is operationally a no-op in executable code, even on the Rust Abstract Machine. Only the proof-code representation changes.

*old(self) == *self,

self.ptr() as int + size_of::<T>() <= other.ptr() as int
    || other.ptr() as int + size_of::<S>() <= self.ptr() as int,

Guarantees that the memory ranges associated with two permissions will not overlap, since you cannot have two permissions to the same memory.

Note: If both S and T are non-zero-sized, then this implies the pointers have distinct addresses.

self.is_uninit(),

points_to_raw.is_range(self.ptr().addr() as int, size_of::<V>() as int),

points_to_raw.provenance() == self.ptr()@.provenance,

Creates a PointsToRaw from a PointsTo<V> with the same provenance and a range corresponding to the address of the PointsTo<V> and size of V, provided that the memory tracked by the PointsTo<V>is uninitialized.

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.