Type Alias GuardedBorrow 

pub type GuardedBorrow<'a, T> = Guarded<&'a mut T>;

A mutable borrow, that asserts an invariant called the guard.

The guard can be broken locally, by accessing the borrow directly. However, it must be restored by the end of the GuardedBorrow’s lifetime.

Example

use creusot_std::prelude::*;
use creusot_std::invariant::GuardedBorrow;

#[ensures(^b == 0i32)]
fn breaks_inv(b: &mut i32) { *b = 0; }

let mut x = 1;
let guarded = GuardedBorrow::new(&mut x, snapshot!(|x: i32| x == 1i32));
// break the guard...
breaks_inv(&mut *guarded.borrow);
// but restore it before we are done
*guarded.borrow = 1;

Aliased Type

#[repr(transparent)]
pub struct GuardedBorrow<'a, T> {
    pub borrow: &'a mut T,
    /* private fields */
}

Fields

borrow: &'a mut 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<'a, T: ?Sized> GuardedBorrow<'a, 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<'a, T: ?Sized> Invariant for GuardedBorrow<'a, T>

fn invariant(self) -> bool

logic(open, prophetic)

self.guard()[self.borrow]