Rollback changes in std-checks

model-checking · Jul 10, 2024 · 630f6c3 · 630f6c3
1 parent d094aaf
commit 630f6c3
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 42 deletions.
diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml
@@ -7,7 +7,7 @@ edition = "2021"
 description = "This crate contains contracts and harnesses for core library"
 
 [package.metadata.kani]
-unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true, uninit-checks = true }
+unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true }
 
 [package.metadata.kani.flags]
 output-format = "terse"
diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected
@@ -1,32 +1,7 @@
-Checking harness mem::verify::check_swap_large_adt_no_drop...
-
-Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
-
-VERIFICATION:- FAILED
-
-Checking harness mem::verify::check_swap_adt_no_drop...
-
-Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
-
-VERIFICATION:- FAILED
-
 Checking harness mem::verify::check_swap_unit...
 
-Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
-
 Failed Checks: ptr NULL or writable up to size
 
-VERIFICATION:- FAILED
-
-Checking harness mem::verify::check_swap_primitive...
-
-Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
-
-VERIFICATION:- FAILED
-
 Summary:
-Verification failed for - mem::verify::check_swap_large_adt_no_drop
-Verification failed for - mem::verify::check_swap_adt_no_drop
 Verification failed for - mem::verify::check_swap_unit
-Verification failed for - mem::verify::check_swap_primitive
-Complete - 3 successfully verified harnesses, 4 failures, 7 total.
+Complete - 6 successfully verified harnesses, 1 failures, 7 total.
diff --git a/tests/std-checks/core/ptr.expected b/tests/std-checks/core/ptr.expected
@@ -1,18 +1,4 @@
-Checking harness ptr::verify::check_new_unchecked...
-
-Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
-
-VERIFICATION:- FAILED
-
-Checking harness ptr::verify::check_new...
-
-Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.
-
-VERIFICATION:- FAILED
-
 Summary:
 Verification failed for - ptr::verify::check_replace_unit
 Verification failed for - ptr::verify::check_as_ref_dangling
-Verification failed for - ptr::verify::check_new_unchecked
-Verification failed for - ptr::verify::check_new
-Complete - 2 successfully verified harnesses, 4 failures, 6 total.
+Complete - 4 successfully verified harnesses, 2 failures, 6 total.