Pointers-out-of-scope test no longer is "fixme" (model-checking#3252)

We handle these adequately as of 0cc4b24. Resolves: model-checking#77
tautschnig · Jun 11, 2024 · b6e4972 · b6e4972
1 parent e922d73
commit b6e4972
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 1 deletion.
diff --git a/...cted/dead-invalid-access-via-raw/expected → ...dead-invalid-access-via-raw/main.expected b/...cted/dead-invalid-access-via-raw/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
@@ -0,0 +1,2 @@
+Failed Checks: assertion failed: *p_subscoped == 7
+Failed Checks: dereference failure: dead object
diff --git a/...ani/Pointers_OutOfScopeFail/fixme_main.rs → ...cted/dead-invalid-access-via-raw/value.rs b/...ani/Pointers_OutOfScopeFail/fixme_main.rs → ...cted/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() {
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		Failed Checks: assertion failed: *p_subscoped == 7
		Failed Checks: dereference failure: dead object