Add test case from issue #3061

tests/expected/dead-invalid-access-via-raw/expected

@@ -0,0 +1,16 @@
+SUCCESS\
+address must be a multiple of its type's alignment
+FAILURE\
+unsafe { *raw_ptr } == 10
+SUCCESS\
+pointer NULL
+SUCCESS\
+pointer invalid
+SUCCESS\
+deallocated dynamic object
+FAILURE\
+dead object
+SUCCESS\
+pointer outside object bounds
+SUCCESS\
+invalid integer address

tests/expected/dead-invalid-access-via-raw/main.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+pub fn check_invalid_ptr() {
+    let raw_ptr = {
+        let var = 10;
+        &var as *const _
+    };
+    // This should fail since it is de-referencing a dead object.
+    assert_eq!(unsafe { *raw_ptr }, 10);
+}