Struct AtomicI32 

pub struct AtomicI32(/* private fields */);

Creusot wrapper around std::sync::atomic::AtomicI32

Implementations

impl AtomicI32

pub fn new(val: i32) -> (Self, Ghost<Box<Perm<AtomicI32>>>)

ensures

*result.1.val() == val

ensures

*result.1.ward() == result.0

terminates

pub fn fetch_add<'a, A, F>(&'a self, val: i32, f: Ghost<F>) -> (i32, Ghost<A>)

where F: FnGhost + FnOnce(&'a mut Committer) -> A,

Wrapper for std::sync::atomic::AtomicI32::fetch_add.

The fetch and the store are always sequentially consistent.

requires

forall<c: &mut Committer> !c.shot() ==> c.ward() == *self ==> c.new_value() == val + c.old_value() ==>
        f.precondition((c,)) &&
        (forall<r> f.postcondition_once((c,), r) ==> (^c).shot())

ensures

exists<c: &mut Committer>
        !c.shot() && c.ward() == *self && c.new_value() == val + c.old_value() &&
        c.old_value() == result.0 &&
        f.postcondition_once((c,), *(result.1))

pub fn store<'a, A, F>(&'a self, val: i32, f: Ghost<F>) -> Ghost<A>

where F: FnGhost + FnOnce(&'a mut Committer) -> A,

Wrapper for std::sync::atomic::AtomicI32::store.

The store is always sequentially consistent.

requires

forall<c: &mut Committer> !c.shot() ==> c.ward() == *self ==> c.new_value() == val ==>
        f.precondition((c,)) &&
        (forall<r> f.postcondition_once((c,), r) ==> (^c).shot())

ensures

exists<c: &mut Committer>
        !c.shot() && c.ward() == *self && c.new_value() == val &&
        f.postcondition_once((c,), *result)

pub fn into_inner(self, own: Ghost<Box<Perm<AtomicI32>>>) -> i32

Wrapper for std::sync::atomic::AtomicI32::into_inner.

requires

self == *own.ward()

ensures

result == *own.val()

Trait Implementations

impl Container for AtomicI32

fn is_disjoint(&self, _: &Self::Value, other: &Self, _: &Self::Value) -> bool

(open, inline)

self != other

type Value = i32