From 630f6c3d142d1869da4a5deb718a05ae71b1d4b2 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 10 Jul 2024 13:43:12 -0700 Subject: [PATCH] Rollback changes in `std-checks` --- tests/std-checks/core/Cargo.toml | 2 +- tests/std-checks/core/mem.expected | 27 +-------------------------- tests/std-checks/core/ptr.expected | 16 +--------------- 3 files changed, 3 insertions(+), 42 deletions(-) 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.