Remove warning for volatile_store (rust-lang#1118)

* Remove warning for `volatile_store` * Removes `loc` clones
celinval · Apr 28, 2022 · 8fe6559 · 8fe6559
1 parent 12b5a85
commit 8fe6559
Showing 1 changed file with 3 additions and 5 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -621,7 +621,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "volatile_store" => {
                 assert!(self.place_ty(p).is_unit());
-                self.codegen_volatile_store(instance, intrinsic, fargs, loc)
+                self.codegen_volatile_store(instance, fargs, loc)
             }
             "wrapping_add" => codegen_wrapping_op!(plus),
             "wrapping_mul" => codegen_wrapping_op!(mul),
@@ -1181,11 +1181,9 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_volatile_store(
         &mut self,
         instance: Instance<'tcx>,
-        intrinsic: &str,
         mut fargs: Vec<Expr>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning!(intrinsic, loc);
         let dst = fargs.remove(0);
         let src = fargs.remove(0);
         let typ = instance.substs.type_at(0);
@@ -1194,9 +1192,9 @@ impl<'tcx> GotocCtx<'tcx> {
             align,
             PropertyClass::DefaultAssertion,
             "`dst` is properly aligned",
-            loc.clone(),
+            loc,
         );
-        let expr = dst.dereference().assign(src, loc.clone());
+        let expr = dst.dereference().assign(src, loc);
         Stmt::block(vec![align_check, expr], loc)
     }