Struct Guarded 

#[repr(transparent)]
pub struct Guarded<T> {
    pub borrow: T,
    /* private fields */
}

A borrow guarded by an invariant.

This is used to define GuardedBorrow. This can also be used to define the equivalent of GuardedBorrow with smart pointers, like RefMut.

Fields

borrow: T

Borrow contained in this guard.

The T type parameter is meant to be a mutable borrow type (like &mut T, or RefMut<T>).

Implementations

impl<T> Guarded<T>

pub fn guard(self) -> Mapping<T, bool>

The guard associated with this borrow.

The type invariant of the Guarded ensures that the current value of borrow satisfies this guard.

logic(open, inline)

*self._guard

impl<'a, T: ?Sized> Guarded<&'a mut T>

pub fn new(borrow: &'a mut T, guard: Snapshot<Mapping<T, bool>>) -> Self

Create a new guarded borrow.

The borrow contained in the result is guaranteed to satisfy the guard at the end of its lifetime.

Note that the borrow field cannot have its final value changed, ensuring that it will not get swapped for another borrow.

ensures

result.borrow == borrow

ensures

forall<bor: &mut T> result.guard()[bor] == (guard[*bor] && ^bor == ^borrow)

ensures

guard[^borrow]

ghost

pub fn into_shared(self) -> &'a T

Get a shared borrow out of this guarded borrow.

It is not possible to break the guard anymore, since the returned borrow is immutable.

ensures

*result == *self.borrow

ensures

*self.borrow == ^self.borrow

ghost

Trait Implementations

impl<T> Deref for Guarded<T>

fn deref(&self) -> &Self::Target

ensures

*result == self.borrow

ghost

type Target = T

The resulting type after dereferencing.

impl<T> Drop for Guarded<T>

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.