diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 2ae5081a90d3..f156f5396c24 100644 --- 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, 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) }