Struct creusot_contracts::ptr_own::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 GhostBox<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.

Implementations

impl<T: ?Sized> PtrOwn<T>

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

The raw pointer whose ownership is tracked by this PtrOwn

logic

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

The value currently stored at address self.ptr()

logic

impl<T> PtrOwn<T>

pub fn new(v: T) -> (RawPtr<T>, GhostBox<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>, GhostBox<PtrOwn<T>>)

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

ensures

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

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

Immutably borrows the underlying T.

requires

ptr == own.ptr()

ensures

*result == *own.val()

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

Mutably borrows the underlying T.

requires

ptr == own.ptr()

ensures

*result == *own.val()

ensures

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

ensures

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

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

Transfers ownership of own back into a Box.

requires

ptr == own.ptr()

ensures

*result == *own.val()

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

Deallocates the memory pointed by ptr.

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(prophetic)

pearlite! { !self.ptr().is_null_logic() && inv(self.val()) }