Struct PermCell 

pub struct PermCell<T: ?Sized>(/* private fields */);

Cell with ghost permissions

When writing/reading the cell, you need to explicitly pass a PermCellOwn object.

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 PermCellOwn object created by PermCell::new, ensuring safety in a manner similar to ghost_cell.

Implementations

impl<T> PermCell<T>

pub fn new(value: T) -> (Self, Ghost<PermCellOwn<T>>)

Creates a new PermCell containing the given value.

terminates

ensures

result.0.id() == result.1.id()

ensures

(*result.1)@ == value

pub unsafe fn set(&self, perm: Ghost<&mut PermCellOwn<T>>, val: T)

Sets the contained value.

Safety

You must ensure that no other borrows to the inner value of self exists when calling this function.

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

terminates

requires

self.id() == perm.id()

ensures

val == (^perm)@

ensures

resolve(perm@)

ensures

self.id() == (^perm).id()

pub unsafe fn replace(&self, perm: Ghost<&mut PermCellOwn<T>>, val: T) -> T

Replaces the contained value with val, and returns the old contained value.

Safety

You must ensure that no other borrows to the inner value of self exists when calling this function.

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

terminates

requires

self.id() == perm.id()

ensures

val == (^perm)@

ensures

result == perm@

ensures

self.id() == (^perm).id()

pub fn into_inner(self, perm: Ghost<PermCellOwn<T>>) -> T

Unwraps the value, consuming the cell.

terminates

requires

self.id() == perm.id()

ensures

result == perm@

pub unsafe fn borrow<'a>(&'a self, perm: Ghost<&'a PermCellOwn<T>>) -> &'a T

Immutably borrows the wrapped value.

The permission also acts as a guard, preventing writes to the underlying value while it is borrowed.

Safety

You must ensure that no mutable borrow to the inner value of self exists when calling this function.

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

terminates

requires

self.id() == perm.id()

ensures

*result == perm@

pub unsafe fn borrow_mut<'a>( &'a self, perm: Ghost<&'a mut PermCellOwn<T>>, ) -> &'a mut T

Mutably borrows the wrapped value.

The permission also acts as a guard, preventing accesses to the underlying value while it is borrowed.

Safety

You must ensure that no other borrows to the inner value of self exists when calling this function.

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

terminates

requires

self.id() == perm.id()

ensures

self.id() == (^perm).id()

ensures

*result == perm@

ensures

^result == (^perm)@

impl<T: Copy> PermCell<T>

pub unsafe fn get(&self, perm: Ghost<&PermCellOwn<T>>) -> T

Returns a copy of the contained value.

Safety

You must ensure that no mutable borrow to the inner value of self exists when calling this function.

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

terminates

requires

self.id() == perm.id()

ensures

result == (**perm)@

impl<T> PermCell<T>

pub fn id(self) -> Id

Returns the logical identity of the cell.

This is used to guarantee that a PermCellOwn is always used with the right PermCell.

(opaque)

pub fn id_ghost(&self) -> Ghost<Id>

terminates

ghost

ensures

*result == self.id()

pub fn as_ptr(&self) -> *mut T

Returns a raw pointer to the underlying data in this cell.

ensures

true

pub fn from_mut(t: &mut T) -> (&PermCell<T>, Ghost<&mut PermCellOwn<T>>)

Returns a &PermCell<T> from a &mut T

terminates

ensures

result.0.id() == result.1.id()

ensures

^t == (^result.1)@

ensures

*t == result.1@

impl<T: Default> PermCell<T>

pub unsafe fn take(&self, perm: Ghost<&mut PermCellOwn<T>>) -> T

Takes the value of the cell, leaving Default::default() in its place.

Safety

You must ensure that no other borrows to the inner value of self exists when calling this function.

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

requires

self.id() == perm.id()

ensures

self.id() == (^perm).id()

ensures

result == perm@

ensures

T::default.postcondition((), (^perm)@)