Struct vstd::ptr::Dealloc

source ·

pub struct Dealloc<V> { /* 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<V> Dealloc<V>

source

pub spec fn view(self) -> DeallocData

👎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 §

impl<V> Dealloc<V>

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_raw(tracked self) -> DeallocRaw

👎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

dealloc_raw@.pptr === self@.pptr,

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

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

is_sized::<V>(),

source

pub proof fn borrow_raw(tracked &self) -> tracked &DeallocRaw

👎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