Skip to content

Commit 8fe6559

Browse files
authored
Remove warning for volatile_store (rust-lang#1118)
* Remove warning for `volatile_store` * Removes `loc` clones
1 parent 12b5a85 commit 8fe6559

File tree

1 file changed

+3
-5
lines changed

1 file changed

+3
-5
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -621,7 +621,7 @@ impl<'tcx> GotocCtx<'tcx> {
621621
}
622622
"volatile_store" => {
623623
assert!(self.place_ty(p).is_unit());
624-
self.codegen_volatile_store(instance, intrinsic, fargs, loc)
624+
self.codegen_volatile_store(instance, fargs, loc)
625625
}
626626
"wrapping_add" => codegen_wrapping_op!(plus),
627627
"wrapping_mul" => codegen_wrapping_op!(mul),
@@ -1181,11 +1181,9 @@ impl<'tcx> GotocCtx<'tcx> {
11811181
fn codegen_volatile_store(
11821182
&mut self,
11831183
instance: Instance<'tcx>,
1184-
intrinsic: &str,
11851184
mut fargs: Vec<Expr>,
11861185
loc: Location,
11871186
) -> Stmt {
1188-
emit_concurrency_warning!(intrinsic, loc);
11891187
let dst = fargs.remove(0);
11901188
let src = fargs.remove(0);
11911189
let typ = instance.substs.type_at(0);
@@ -1194,9 +1192,9 @@ impl<'tcx> GotocCtx<'tcx> {
11941192
align,
11951193
PropertyClass::DefaultAssertion,
11961194
"`dst` is properly aligned",
1197-
loc.clone(),
1195+
loc,
11981196
);
1199-
let expr = dst.dereference().assign(src, loc.clone());
1197+
let expr = dst.dereference().assign(src, loc);
12001198
Stmt::block(vec![align_check, expr], loc)
12011199
}
12021200

0 commit comments

Comments
 (0)