Add a test that deallocates a stack variable (#2717)

tests/expected/dealloc/stack/expected

@@ -0,0 +1,4 @@
+Status: FAILURE\
+Description: "free argument must be dynamic object"
+
+VERIFICATION:- FAILED

tests/expected/dealloc/stack/test.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use std::alloc::{dealloc, Layout};
+
+// This test checks that Kani flags the deallocation of a stack-allocated
+// variable
+
+#[kani::proof]
+fn check_dealloc_stack() {
+    let mut x = 6;
+    let layout = Layout::new::<i32>();
+    let p = &mut x as *mut i32;
+    unsafe {
+        dealloc(p as *mut u8, layout);
+    }
+}