Add test to check that no pointer checks happen inside kani::mem_init

tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+use std::alloc::{alloc_zeroed, Layout};
+use std::slice::from_raw_parts;
+
+#[kani::proof]
+fn alloc_zeroed_to_slice() {
+    let layout = Layout::from_size_align(32, 8).unwrap();
+    unsafe {
+        // This returns initialized memory, so any further accesses are valid.
+        let ptr = alloc_zeroed(layout);
+        *ptr = 0x41;
+        *ptr.add(1) = 0x42;
+        *ptr.add(2) = 0x43;
+        *ptr.add(3) = 0x44;
+        *ptr.add(16) = 0x00;
+        let _slice1 = from_raw_parts(ptr, 16);
+        let _slice2 = from_raw_parts(ptr.add(16), 16);
+    }
+}

tests/script-based-pre/mem-init-reinstrumentation/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: mem-init-reinstrumentation.sh
+expected: mem-init-reinstrumentation.expected

tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected

@@ -0,0 +1 @@
+success: no pointer checks are detected in initialized memory instrumentaiton

tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -u
+
+KANI_OUTPUT=`kani -Z uninit-checks alloc-zeroed.rs`
+echo "$KANI_OUTPUT" | egrep -q "kani::mem_init::.*pointer_dereference"
+INSTRUMENTATION_DETECTED=$?
+
+if [[ $INSTRUMENTATION_DETECTED == 0 ]]; then
+    echo "failed: pointer checks are detected in initialized memory instrumentaiton"
+    exit 1
+elif [[ $INSTRUMENTATION_DETECTED == 1 ]]; then
+    echo "success: no pointer checks are detected in initialized memory instrumentaiton"
+    exit 0
+else 
+    echo "failed: error occured when runnning egrep"
+    exit 0
+fi