PR comments

model-checking · Jun 28, 2021 · 86118f8 · 86118f8
1 parent b5deaa0
commit 86118f8
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 17 deletions.
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
@@ -280,11 +280,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "atomic_xadd_acqrel" => codegen_atomic_binop!(plus),
             "atomic_xadd_rel" => codegen_atomic_binop!(plus),
             "atomic_xadd_relaxed" => codegen_atomic_binop!(plus),
-            "atomic_xchg"
-            | "atomic_xchg_acq"
-            | "atomic_xchg_acqrel"
-            | "atomic_xchg_rel"
-            | "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_acq" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_xor" => codegen_atomic_binop!(bitxor),
             "atomic_xor_acq" => codegen_atomic_binop!(bitxor),
             "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor),

diff --git a/src/test/cbmc/Atomics/Stable/Exchange/main.rs b/src/test/cbmc/Atomics/Stable/Exchange/main.rs
@@ -3,18 +3,6 @@
 use std::sync::atomic::{AtomicBool, Ordering};
 
 fn main() {
-    // pub fn compare_exchange(
-    //     &self,
-    //     current: bool,
-    //     new: bool,
-    //     success: Ordering,
-    //     failure: Ordering
-    // ) -> Result<bool, bool>
-    // Stores a value into the bool if the current value is the same
-    // as the current value.
-    // The return value is a result indicating whether the new value
-    // was written and containing the previous value. On success this
-    // value is guaranteed to be equal to current.
     let a1 = AtomicBool::new(true);
     let a2 = AtomicBool::new(true);
     let a3 = AtomicBool::new(true);