Struct VHeap 

pub struct VHeap<S: IShape> { /* private fields */ }

Verified heap that tracks state for Kani proofs.

This heap doesn’t do any real memory operations - it just tracks the abstract state of allocations and asserts that all transitions are valid.

Implementations

impl<S: IShape> VHeap<S>

pub fn new() -> Self

Create a new verified heap with no allocations.

Trait Implementations

impl<S: Debug + IShape> Debug for VHeap<S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<S: IShape> Default for VHeap<S>

fn default() -> Self

Returns the “default value” for a type.

impl<S: IShape> IHeap<S> for VHeap<S>

type Ptr = VPtr

Pointer type used by this heap.

unsafe fn alloc(&mut self, shape: S) -> VPtr

Allocate a region for a value of the given shape.

unsafe fn dealloc(&mut self, ptr: VPtr, shape: S)

Deallocate a region.

unsafe fn memcpy(&mut self, dst: VPtr, src: VPtr, len: usize)

Copy len bytes from src to dst.

unsafe fn drop_in_place(&mut self, ptr: VPtr, shape: S)

Drop the value at ptr and mark the range as uninitialized.

unsafe fn default_in_place(&mut self, ptr: VPtr, shape: S) -> bool

Default-initialize the value at ptr and mark the range as initialized.