diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 3e8ac4cf02fb..813e07d06723 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -271,7 +271,7 @@ impl GotocCtx<'_> { ) } // For all other assert kind we can get the static message. - AssertMessage::NullPointerDereference { .. } => { + AssertMessage::NullPointerDereference => { (msg.description().unwrap(), PropertyClass::SafetyCheck) } AssertMessage::Overflow { .. } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 2ead8328e67b..6f7b59041d12 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -205,7 +205,7 @@ impl MutableBody { Operand::Copy(Place::from(self.new_local(assert_fn.ty(), span, Mutability::Not))); let kind = TerminatorKind::Call { func: assert_op, - args: args, + args, destination: Place { local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not), projection: vec![],