Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133#![allow(unused_imports)]use super::super::prelude::*;use core::sync::atomic::*;
// Supports the core::sync::atomic functions// This provides NO support for reasoning about the values inside the atomics.// If you need to do that, see `vstd::atomic` or `vstd::atomic_ghost` instead.#[verifier::external_type_specification]#[verifier::external_body]#[verifier::reject_recursive_types(T)]pub struct ExAtomic<T: AtomicPrimitive>(Atomic<T>);
#[verifier::external_trait_specification]pub trait ExAtomicPrimitive: Sized + Copy { type ExternalTraitSpecificationFor: AtomicPrimitive;}
#[verifier::external_type_specification]pub struct ExOrdering(Ordering);
macro_rules! atomic_specs_common { ($at:ty, $ty:ty) => { verus!{
// Panic preconditions per the std docs: load rejects Release/AcqRel, store rejects // Acquire/AcqRel, and compare_exchange(_weak) rejects Release/AcqRel as `failure`. pub assume_specification [ <$at>::new ](v: $ty) -> $at no_unwind;
pub assume_specification [ <$at>::compare_exchange ]( atomic: &$at, current: $ty, new: $ty, success: Ordering, failure: Ordering, ) -> Result<$ty, $ty> requires failure != Ordering::Release, failure != Ordering::AcqRel, no_unwind;
pub assume_specification [ <$at>::compare_exchange_weak ]( atomic: &$at, current: $ty, new: $ty, success: Ordering, failure: Ordering, ) -> Result<$ty, $ty> requires failure != Ordering::Release, failure != Ordering::AcqRel, no_unwind;
pub assume_specification [ <$at>::fetch_and ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
pub assume_specification [ <$at>::fetch_nand ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
pub assume_specification [ <$at>::fetch_or ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
pub assume_specification [ <$at>::fetch_xor ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
pub assume_specification [ <$at>::load ](atomic: &$at, order: Ordering) -> $ty requires order != Ordering::Release, order != Ordering::AcqRel, no_unwind;
pub assume_specification [ <$at>::store ](atomic: &$at, val: $ty, order: Ordering) requires order != Ordering::Acquire, order != Ordering::AcqRel, no_unwind;
pub assume_specification [ <$at>::swap ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
} };}
macro_rules! atomic_specs_int_specific { ($at:ty, $ty:ty) => { verus!{
pub assume_specification [ <$at>::fetch_add ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
pub assume_specification [ <$at>::fetch_sub ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
pub assume_specification [ <$at>::fetch_min ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
pub assume_specification [ <$at>::fetch_max ](atomic: &$at, val: $ty, order: Ordering) -> $ty no_unwind;
} };}
macro_rules! atomic_specs_int { ($at:ty, $ty:ty) => { atomic_specs_common!($at, $ty); atomic_specs_int_specific!($at, $ty); };}
macro_rules! atomic_specs_bool { ($at:ty, $ty:ty) => { atomic_specs_common!($at, $ty); };}
atomic_specs_int!(AtomicU8, u8);atomic_specs_int!(AtomicU16, u16);atomic_specs_int!(AtomicU32, u32);#[cfg(target_has_atomic = "64")]atomic_specs_int!(AtomicU64, u64);atomic_specs_int!(AtomicUsize, usize);
atomic_specs_int!(AtomicI8, i8);atomic_specs_int!(AtomicI16, i16);atomic_specs_int!(AtomicI32, i32);#[cfg(target_has_atomic = "64")]atomic_specs_int!(AtomicI64, i64);atomic_specs_int!(AtomicIsize, isize);
atomic_specs_bool!(AtomicBool, bool);