update tests to reflect fix

carolynzech · Aug 5, 2024 · 61515b6 · 61515b6
1 parent 66a40c9
commit 61515b6
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 11 deletions.
diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected
@@ -1,7 +1,3 @@
 Checking harness mem::verify::check_swap_unit...
 
-Failed Checks: ptr NULL or writable up to size
-
-Summary:
-Verification failed for - mem::verify::check_swap_unit
-Complete - 6 successfully verified harnesses, 1 failures, 7 total.
+Complete - 7 successfully verified harnesses, 0 failures, 7 total.
diff --git a/tests/std-checks/core/ptr.expected b/tests/std-checks/core/ptr.expected
@@ -1,4 +1,3 @@
 Summary:
-Verification failed for - ptr::verify::check_replace_unit
 Verification failed for - ptr::verify::check_as_ref_dangling
-Complete - 4 successfully verified harnesses, 2 failures, 6 total.
+Complete - 5 successfully verified harnesses, 1 failures, 6 total.
diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs
@@ -48,8 +48,6 @@ mod verify {
         contracts::swap(&mut x, &mut y)
     }
 
-    /// FIX-ME: Modifies clause fail with pointer to ZST.
-    /// <https://github.com/model-checking/kani/issues/3181>
     #[kani::proof_for_contract(contracts::swap)]
     pub fn check_swap_unit() {
         let mut x: () = kani::any();

diff --git a/tests/std-checks/core/src/ptr.rs b/tests/std-checks/core/src/ptr.rs
@@ -89,8 +89,6 @@ mod verify {
         let _rf = unsafe { contracts::as_ref(&non_null) };
     }
 
-    /// FIX-ME: Modifies clause fail with pointer to ZST.
-    /// <https://github.com/model-checking/kani/issues/3181>
     #[kani::proof_for_contract(contracts::replace)]
     pub fn check_replace_unit() {
         check_replace_impl::<()>();