Struct vstd::raw_ptr::PointsToRaw

source · 
pub struct PointsToRaw { /* private fields */ }
Expand description

PointsToRaw Variable-sized uninitialized memory.

Permission is for an arbitrary set of addresses, not necessarily contiguous, and with a given provenance.

Implementations§

source§

impl PointsToRaw

source

pub open spec fn provenance(self) -> Provenance

{}
source

pub open spec fn dom(self) -> Set<int>

{}
source

pub open spec fn is_range(self, start: int, len: int) -> bool

{ super::set_lib::set_int_range(start, start + len) =~= self.dom() }
source

pub open spec fn contains_range(self, start: int, len: int) -> bool

{ super::set_lib::set_int_range(start, start + len) <= self.dom() }
source

pub proof fn empty(provenance: Provenance) -> tracked Self

ensures
points_to_raw.dom() == Set::<int>::empty(),
points_to_raw.provenance() == provenance,
source

pub proof fn split(tracked self, range: Set<int>) -> (Self, Self)

requires
range.subset_of(self.dom()),
ensures
res.0.provenance() == self.provenance(),
res.1.provenance() == self.provenance(),
res.0.dom() == range,
res.1.dom() == self.dom().difference(range),
source

pub proof fn join(tracked self, tracked other: Self) -> tracked Self

requires
self.provenance() == other.provenance(),
ensures
joined.provenance() == self.provenance(),
joined.dom() == self.dom() + other.dom(),
source

pub proof fn into_typed<V>(tracked self, start: usize) -> PointsTo<V>

requires
is_sized::<V>(),
start as int % align_of::<V>() as int == 0,
self.is_range(start as int, size_of::<V>() as int),
ensures
points_to.ptr()
    == ptr_mut_from_data::<
        V,
    >(PtrData {
        addr: start,
        provenance: self.provenance(),
        metadata: Metadata::Thin,
    }),
points_to.is_uninit(),

Auto Trait Implementations§

Blanket Implementations§

source§

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

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

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

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

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

source§

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

Mutably borrows from an owned value. Read more
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

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

source§

fn into(self) -> U

Calls U::from(self).

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

source§

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

§

type Error = Infallible

The type returned in the event of a conversion error.
source§

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

Performs the conversion.
source§

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

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.