Struct vstd::ptr::PointsToRaw

source ·

pub struct PointsToRaw { /* private fields */ }

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

Expand description

Points to uninitialized memory.

Implementations§

source §

impl PointsToRaw

source

pub spec fn view(self) -> Map<int, u8>

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

source

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

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

{ set_int_range(start, start + len).subset_of(self@.dom()) }

source

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

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

{ set_int_range(start, start + len) =~= self@.dom() }

source

pub open spec fn spec_index(self, i: int) -> u8

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

{ self@[i] }

source

pub proof fn is_nonnull(tracked &self)

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

ensures

!self@.dom().contains(0),

source

pub proof fn is_in_bounds(tracked &self)

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

ensures

forall |i: int| self@.dom().contains(i) ==> 0 < i <= usize::MAX,

source

pub proof fn empty() -> tracked points_to_raw : Self

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

ensures

points_to_raw@ == Map::<int, u8>::empty(),

source

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

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

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@.pptr == start,

points_to@.value === None,

source

pub proof fn borrow_typed<V>(tracked &self, start: int) -> tracked points_to : &PointsTo<V>

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

requires

is_sized::<V>(),

start % align_of::<V>() as int == 0,

self.contains_range(start, size_of::<V>() as int),

ensures

points_to@.pptr === start,

points_to@.value === None,

source

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

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

ensures

self@.dom().disjoint(other@.dom()),

joined@ == self@.union_prefer_right(other@),

source

pub proof fn insert(tracked &mut self, tracked other: Self)

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

ensures

old(self)@.dom().disjoint(other@.dom()),

self@ == old(self)@.union_prefer_right(other@),

source

pub proof fn borrow_join<'a>(tracked &'a self, tracked other: &'a Self) -> tracked joined : &'a Self

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

ensures

(forall |i| {
    self@.dom().contains(i) && other@.dom().contains(i) ==> self@[i] == other@[i]
}),

joined@ == self@.union_prefer_right(other@),

source

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

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

requires

range.subset_of(self@.dom()),

ensures

res.0@ == self@.restrict(range),

res.1@ == self@.remove_keys(range),

source

pub proof fn take(tracked &mut self, range: Set<int>) -> tracked res : Self

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

requires

range.subset_of(old(self)@.dom()),

ensures

res@ == old(self)@.restrict(range),

self@ == old(self)@.remove_keys(range),

source

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

👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either: – PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations) – *mut T with vstd::raw_ptr (for more advanced use-cases)

requires