diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml index a1496a0c81a7..f6e1645c3a39 100644 --- 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 index 0276f285807f..1484c83901fc 100644 --- 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 index a5ef62af8036..43d3bd6baf60 100644 --- 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.