From b6e4972b303b21fdbbd92af522409de4e10a628f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 11 Jun 2024 19:28:07 +0200 Subject: [PATCH] Pointers-out-of-scope test no longer is "fixme" (#3252) We handle these adequately as of 0cc4b2463828. Resolves: #77 --- .../dead-invalid-access-via-raw/{expected => main.expected} | 0 tests/expected/dead-invalid-access-via-raw/value.expected | 2 ++ .../dead-invalid-access-via-raw/value.rs} | 1 - 3 files changed, 2 insertions(+), 1 deletion(-) rename tests/expected/dead-invalid-access-via-raw/{expected => main.expected} (100%) create mode 100644 tests/expected/dead-invalid-access-via-raw/value.expected rename tests/{kani/Pointers_OutOfScopeFail/fixme_main.rs => expected/dead-invalid-access-via-raw/value.rs} (96%) diff --git a/tests/expected/dead-invalid-access-via-raw/expected b/tests/expected/dead-invalid-access-via-raw/main.expected similarity index 100% rename from tests/expected/dead-invalid-access-via-raw/expected rename to tests/expected/dead-invalid-access-via-raw/main.expected diff --git a/tests/expected/dead-invalid-access-via-raw/value.expected b/tests/expected/dead-invalid-access-via-raw/value.expected new file mode 100644 index 000000000000..858d44d54ea4 --- /dev/null +++ b/tests/expected/dead-invalid-access-via-raw/value.expected @@ -0,0 +1,2 @@ +Failed Checks: assertion failed: *p_subscoped == 7 +Failed Checks: dereference failure: dead object diff --git a/tests/kani/Pointers_OutOfScopeFail/fixme_main.rs b/tests/expected/dead-invalid-access-via-raw/value.rs similarity index 96% rename from tests/kani/Pointers_OutOfScopeFail/fixme_main.rs rename to tests/expected/dead-invalid-access-via-raw/value.rs index 5bbcb93930bb..6160325174b7 100644 --- a/tests/kani/Pointers_OutOfScopeFail/fixme_main.rs +++ b/tests/expected/dead-invalid-access-via-raw/value.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-verify-fail #[kani::proof] fn main() {