vstd/std_specs/
atomic.rs

Help
1#![allow(unused_imports)]
2use super::super::prelude::*;
3use core::sync::atomic::*;
4
5// Supports the core::sync::atomic functions
6// This provides NO support for reasoning about the values inside the atomics.
7// If you need to do that, see `vstd::atomic` or `vstd::atomic_ghost` instead.
8
9#[verifier::external_type_specification]
10pub struct ExOrdering(Ordering);
11
12macro_rules! atomic_specs_common {
13    ($at:ty, $ty:ty) => {
14        #[verifier::external_type_specification]
15        #[verifier::external_body]
16        pub struct ExAtomic($at);
17
18        verus!{
19
20        pub assume_specification [ <$at>::new ](v: $ty) -> $at;
21
22        pub assume_specification [ <$at>::compare_exchange ](
23            atomic: &$at,
24            current: $ty,
25            new: $ty,
26            success: Ordering,
27            failure: Ordering,
28        ) -> Result<$ty, $ty>;
29
30        pub assume_specification [ <$at>::compare_exchange_weak ](
31            atomic: &$at,
32            current: $ty,
33            new: $ty,
34            success: Ordering,
35            failure: Ordering,
36        ) -> Result<$ty, $ty>;
37
38        pub assume_specification [ <$at>::fetch_and ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
39
40        pub assume_specification [ <$at>::fetch_nand ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
41
42        pub assume_specification [ <$at>::fetch_or ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
43
44        pub assume_specification [ <$at>::fetch_xor ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
45
46        pub assume_specification [ <$at>::load ](atomic: &$at, order: Ordering) -> $ty;
47
48        pub assume_specification [ <$at>::store ](atomic: &$at, val: $ty, order: Ordering);
49
50        pub assume_specification [ <$at>::swap ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
51
52        }
53    };
54}
55
56macro_rules! atomic_specs_int_specific {
57    ($at:ty, $ty:ty) => {
58        verus!{
59
60        pub assume_specification [ <$at>::fetch_add ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
61
62        pub assume_specification [ <$at>::fetch_sub ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
63
64        pub assume_specification [ <$at>::fetch_min ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
65
66        pub assume_specification [ <$at>::fetch_max ](atomic: &$at, val: $ty, order: Ordering) -> $ty;
67
68        }
69    };
70}
71
72macro_rules! atomic_specs_int {
73    ($modname:ident, $at:ty, $ty:ty) => {
74        mod $modname {
75            use super::*;
76            atomic_specs_common!($at, $ty);
77            atomic_specs_int_specific!($at, $ty);
78        }
79    };
80}
81
82macro_rules! atomic_specs_bool {
83    ($modname:ident, $at:ty, $ty:ty) => {
84        mod $modname {
85            use super::*;
86            atomic_specs_common!($at, $ty);
87        }
88    };
89}
90
91atomic_specs_int!(atomic_specs_u8, AtomicU8, u8);
92atomic_specs_int!(atomic_specs_u16, AtomicU16, u16);
93atomic_specs_int!(atomic_specs_u32, AtomicU32, u32);
94atomic_specs_int!(atomic_specs_u64, AtomicU64, u64);
95atomic_specs_int!(atomic_specs_usize, AtomicUsize, usize);
96
97atomic_specs_int!(atomic_specs_i8, AtomicI8, i8);
98atomic_specs_int!(atomic_specs_i16, AtomicI16, i16);
99atomic_specs_int!(atomic_specs_i32, AtomicI32, i32);
100atomic_specs_int!(atomic_specs_i64, AtomicI64, i64);
101atomic_specs_int!(atomic_specs_isize, AtomicIsize, isize);
102
103atomic_specs_bool!(atomic_specs_bool, AtomicBool, bool);
vstd/std_specs/atomic.rs

vstd/std_specs/
atomic.rs
