Add a multi-crate test for #3061 (#3076)

This is a follow-up on #3063 that adds a test with multiple crates to
make sure this scenario is correctly handled and that Kani reports the
bug.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

tests/cargo-kani/storage-markers/Cargo.toml

@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[workspace]
+members = ["crate-with-bug", "crate-with-harness"]
+resolver = "2"

tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml

@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "crate-with-bug"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This function contains a use-after-free bug.
+
+pub fn fn_with_bug() -> i32 {
+    let raw_ptr = {
+        let var = 10;
+        &var as *const i32
+    };
+    unsafe { *raw_ptr }
+}

tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml

@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "crate-with-harness"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+crate-with-bug = { path = "../crate-with-bug" }

tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected

@@ -0,0 +1,3 @@
+Status: FAILURE\
+Description: "dereference failure: dead object"\
+in function crate_with_bug::fn_with_bug

tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that Kani captures the case of a use-after-free issue as
+// described in https://github.com/model-checking/kani/issues/3061 even across
+// crates. The test calls a function from another crate that has the bug.
+
+#[kani::proof]
+pub fn call_fn_with_bug() {
+    let _x = crate_with_bug::fn_with_bug();
+}