Struct vstd :: raw_ptr :: PointsTo Copy item path

impl<T> PointsTo<T>

pub open spec fn ptr(&self) -> *mut T

{ self.view().ptr }

pub open spec fn opt_value(&self) -> MemContents<T>

{ self.view().opt_value }

pub open spec fn is_init(&self) -> bool

{ self.opt_value().is_init() }

pub open spec fn is_uninit(&self) -> bool

{ self.opt_value().is_uninit() }

pub open spec fn value(&self) -> T

{ self.opt_value().value() }

pub proof fn is_nonnull(tracked &self)

requires

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

ensures

self@.ptr@.addr != 0,

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

pub proof fn leak_contents(tracked &mut self)

ensures

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.

pub proof fn is_disjoint<S>(&mut self, other: &PointsTo<S>)

ensures

*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,

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

impl<V> PointsTo<V>

pub proof fn into_raw(tracked self) -> tracked points_to_raw : PointsToRaw

requires

self.is_uninit(),

ensures

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

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

is_sized::<V>(),

Trait Implementations§

impl<T> View for PointsTo<T>

spec fn view(&self) -> Self::V

type V = PointsToData<T>

Auto Trait Implementations§

impl<T> UnwindSafe for PointsTo<T>
where T: UnwindSafe,

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, U> Into for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

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

impl<T, U> TryFrom for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

Performs the conversion.

impl<T, U> TryInto for T
where U: TryFrom<T>,

type Error = >::Error

The type returned in the event of a conversion error.