More expected tests (readable/writable)

tests/expected/intrinsics/copy/copy-unreadable-src/expected

@@ -0,0 +1,2 @@
+FAILURE\
+memmove source region readable

tests/expected/intrinsics/copy/copy-unreadable-src/main.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy` fails when `src` is not valid for reads.
+#[kani::proof]
+fn test_copy_invalid() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an invalid pointer with a negative offset
+        let src_invalid = unsafe { src.sub(1) as *const i32 };
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::copy(src_invalid, dst, 1);
+    }
+}

tests/expected/intrinsics/copy/copy-unwritable-dst/expected

@@ -0,0 +1,2 @@
+FAILURE\
+memmove destination region writeable

tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy` fails when `dst` is not valid for writes.
+#[kani::proof]
+fn test_copy_invalid() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an invalid pointer with an out-of-bounds offset
+        let dst_invalid = src.add(3) as *mut i32;
+        core::intrinsics::copy(src, dst_invalid, 1);
+    }
+}