Change generate_unchecked_neg_harness macro

model-checking · Oct 3, 2024 · a3bf6d1 · a3bf6d1
1 parent 715e940
commit a3bf6d1
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
@@ -1620,13 +1620,13 @@ mod verify {
     }
 
     macro_rules! generate_unchecked_neg_harness {
-        ($type:ty, $method:ident, $harness_name:ident) => {
-            #[kani::proof_for_contract($type::$method)]
+        ($type:ty, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::unchecked_neg)]
             pub fn $harness_name() {
                 let num1: $type = kani::any::<$type>();
 
                 unsafe {
-                    num1.$method();
+                    num1.unchecked_neg();
                 }
             }
         }