Struct vstd::ptr::DeallocRaw

source ·

pub struct DeallocRaw { /* 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)

Implementations§

source §

impl DeallocRaw

source

pub spec fn view(self) -> DeallocRawData

👎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 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@.pptr != 0,

source

pub proof fn into_typed<V>(tracked self) -> tracked dealloc : Dealloc<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>(),

self@.size === size_of::<V>(),

self@.align === align_of::<V>(),

ensures

dealloc@.pptr === self@.pptr,

source

pub proof fn borrow_typed<V>(tracked &self) -> tracked dealloc : &Dealloc<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