references to open_atomic_invariant! should refer vstd, not the clien…

…t crate
verus-lang · Feb 2, 2024 · ee42363 · ee42363
1 parent 2fe7508
commit ee42363
Showing 1 changed file with 7 additions and 7 deletions.
diff --git a/source/pervasive/atomic_ghost.rs b/source/pervasive/atomic_ghost.rs
@@ -319,7 +319,7 @@ macro_rules! atomic_with_ghost_store {
     ($e:expr, $operand:expr, $prev:pat, $next:pat, $res:pat, $g:ident, $b:block) => {
         ::builtin_macros::verus_exec_expr!{ {
             let atomic = &($e);
-            crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
+            $crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
                 #[allow(unused_mut)]
                 let tracked (mut perm, mut $g) = pair;
                 let ghost $prev = perm.view().value;
@@ -343,7 +343,7 @@ macro_rules! atomic_with_ghost_load {
         ::builtin_macros::verus_exec_expr!{ {
             let result;
             let atomic = &($e);
-            crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
+            $crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
                 #[allow(unused_mut)]
                 let tracked (perm, mut $g) = pair;
                 result = atomic.patomic.load(Tracked(&perm));
@@ -368,7 +368,7 @@ macro_rules! atomic_with_ghost_no_op {
     ($e:expr, $prev:pat, $next: pat, $res: pat, $g:ident, $b:block) => {
         ::builtin_macros::verus_exec_expr!{ {
             let atomic = &($e);
-            crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
+            $crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
                 #[allow(unused_mut)]
                 let tracked (perm, mut $g) = pair;
                 let ghost $res = result;
@@ -393,7 +393,7 @@ macro_rules! atomic_with_ghost_update_with_1_operand {
             let result;
             let atomic = &($e);
             let operand = $operand;
-            crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
+            $crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
                 #[allow(unused_mut)]
                 let tracked (mut perm, mut $g) = pair;
                 let ghost $prev = perm.view().value;
@@ -421,7 +421,7 @@ macro_rules! atomic_with_ghost_update_with_2_operand {
             let atomic = &($e);
             let operand1 = $operand1;
             let operand2 = $operand2;
-            crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
+            $crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
                 #[allow(unused_mut)]
                 let tracked (mut perm, mut $g) = pair;
                 let ghost $prev = perm.view().value;
@@ -448,7 +448,7 @@ macro_rules! atomic_with_ghost_update_fetch_add {
             let result;
             let atomic = &($e);
             let operand = $operand;
-            crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
+            $crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
                 #[allow(unused_mut)]
                 let tracked (mut perm, mut $g) = pair;
 
@@ -479,7 +479,7 @@ macro_rules! atomic_with_ghost_update_fetch_sub {
             let result;
             let atomic = &($e);
             let operand = $operand;
-            crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
+            $crate::open_atomic_invariant!(atomic.atomic_inv.borrow() => pair => {
                 #[allow(unused_mut)]
                 let tracked (mut perm, mut $g) = pair;