Struct PtrOwn

pub struct PtrOwn<T: ?Sized> { /* private fields */ }

Token that represents the ownership of a memory cell. A PtrOwn value only exists in the ghost world, but can be used in combination with a corresponding RawPtr to access and modify memory.

A warning regarding memory leaks: dropping a Ghost<PtrOwn<T>> (we only ever handle ghost PtrOwn values) cannot deallocate the memory corresponding to the pointer because it is a ghost value. One must thus remember to explicitly call drop in order to free the memory tracked by a PtrOwn token.

Safety

When using Creusot to verify the code, all methods should be safe to call. Indeed, Creusot ensures that every operation on the inner value uses the right PtrOwn object created by PtrOwn::new, ensuring safety in a manner similar to ghost_cell.

Implementations

impl<T: ?Sized> PtrOwn<T>

pub fn ptr(&self) -> RawPtr<T>

The raw pointer whose ownership is tracked by this PtrOwn

logic

self.ptr

pub fn val(&self) -> SizedW<T>

The value currently stored at address self.ptr()

logic

self.val

impl<T> PtrOwn<T>

pub fn new(v: T) -> (RawPtr<T>, Ghost<PtrOwn<T>>)

Creates a new PtrOwn and associated RawPtr by allocating a new memory cell initialized with v.

ensures

result.1.ptr() == result.0 && *result.1.val() == v

impl<T: ?Sized> PtrOwn<T>

pub fn from_box(val: Box<T>) -> (RawPtr<T>, Ghost<PtrOwn<T>>)

Creates a ghost PtrOwn and associated RawPtr from an existing Box.

ensures

result.1.ptr() == result.0 && *result.1.val() == *val

pub unsafe fn as_ref(ptr: RawPtr<T>, own: Ghost<&PtrOwn<T>>) -> &T

Immutably borrows the underlying T.

Safety

Safety requirements are the same as a direct dereference: &*ptr.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

requires

ptr == own.ptr()

ensures

*result == *own.val()

pub unsafe fn as_mut(ptr: RawPtr<T>, own: Ghost<&mut PtrOwn<T>>) -> &mut T

Mutably borrows the underlying T.

Safety

Safety requirements are the same as a direct dereference: &mut *ptr.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

requires

ptr == own.ptr()

ensures

*result == *own.val()

ensures

(^own.inner_logic()).ptr() == own.ptr()

ensures

*(^own.inner_logic()).val() == ^result

pub unsafe fn to_box(ptr: RawPtr<T>, own: Ghost<PtrOwn<T>>) -> Box<T>

Transfers ownership of own back into a Box.

Safety

Safety requirements are the same as Box::from_raw.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

requires

ptr == own.ptr()

ensures

*result == *own.val()

pub unsafe fn drop(ptr: RawPtr<T>, own: Ghost<PtrOwn<T>>)

Deallocates the memory pointed by ptr.

Safety

Safety requirements are the same as Box::from_raw.

Creusot will check that all calls to this function are indeed safe: see the type documentation.

requires

ptr == own.ptr()

pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &PtrOwn<T>)

If one owns two PtrOwns in ghost code, then they are for different pointers.

pure

ensures

own1.ptr().addr_logic() != own2.ptr().addr_logic()

ensures

*own1 == ^own1

Trait Implementations

impl<T: ?Sized> Invariant for PtrOwn<T>

fn invariant(self) -> bool

logic

!self.ptr().is_null_logic()