Added tests with GlobalAlloc / promoted

Author: dkcumming

kmir/src/tests/integration/data/prove-rs/ptr-metadata-array-fail.rs

@@ -0,0 +1,6 @@
+fn main() {
+    let len = [1; 2].len();
+    let len2 = [4; 3].len();
+    assert!(len == 2);
+    assert!(len2 == 3);
+}

kmir/src/tests/integration/data/prove-rs/ptr-metadata-slice-fail.rs

@@ -0,0 +1,4 @@
+fn main() {
+    let t = [1; 2];
+    assert!(&t[..] == t);
+}

kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-array-fail.expected

@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "ptr_metadata_array_fail" ) globalAllocEntry ( 0 , Memory ( all
+│   function: main
+│   span: 51
+│
+│  (27 steps)
+└─ 3 (stuck, leaf)
+    #applyUnOp ( unOpPtrMetadata , typedValue ( thunk ( #cast ( typedValue ( RefAllo
+    function: main
+    span: 53
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-slice-fail.expected

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "ptr_metadata_slice_fail" ) globalAllocEntry ( 1 , Memory ( all
+│   function: main
+│   span: 127
+│
+│  (156 steps)
+└─ 3 (stuck, leaf)
+    #applyUnOp ( unOpPtrMetadata , typedValue ( thunk ( #cast ( typedValue ( RefStac
+    span: 58
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+

kmir/src/tests/integration/test_integration.py

@@ -435,6 +435,8 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None:
     'interior-mut3-fail',
     'assert_eq_exp-fail',
     'bitwise-not-shift-fail',
+    'ptr-metadata-array-fail',
+    'ptr-metadata-slice-fail',
 ]