Fix copy intrinsic test to reflect the semantic change

tests/expected/uninit/intrinsics/expected

@@ -46,6 +46,10 @@ VERIFICATION:- SUCCESSFUL
 
 Checking harness check_copy...
 
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_copy_read...
+
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 
 VERIFICATION:- FAILED
@@ -56,6 +60,10 @@ VERIFICATION:- SUCCESSFUL
 
 Checking harness check_copy_nonoverlapping...
 
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_copy_nonoverlapping_read...
+
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 
 VERIFICATION:- FAILED
@@ -65,6 +73,6 @@ Verification failed for - check_typed_swap_safe
 Verification failed for - check_typed_swap
 Verification failed for - check_volatile_load
 Verification failed for - check_compare_bytes
-Verification failed for - check_copy
-Verification failed for - check_copy_nonoverlapping
-Complete - 5 successfully verified harnesses, 6 failures, 11 total.
+Verification failed for - check_copy_read
+Verification failed for - check_copy_nonoverlapping_read
+Complete - 7 successfully verified harnesses, 6 failures, 13 total.

tests/expected/uninit/intrinsics/intrinsics.rs

@@ -14,7 +14,20 @@ fn check_copy_nonoverlapping() {
         let layout = Layout::from_size_align(16, 8).unwrap();
         let src: *mut u8 = alloc(layout);
         let dst: *mut u8 = alloc(layout);
-        copy_nonoverlapping(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized.
+        // This does not fail, since `copy_nonoverlapping` is untyped.
+        copy_nonoverlapping(src as *const u8, dst, 2);
+    }
+}
+
+#[kani::proof]
+fn check_copy_nonoverlapping_read() {
+    unsafe {
+        let layout = Layout::from_size_align(16, 8).unwrap();
+        let src: *mut u8 = alloc(layout);
+        let dst: *mut u8 = alloc_zeroed(layout);
+        copy_nonoverlapping(src as *const u8, dst, 2);
+        // ~ERROR: Accessing `dst` here, which became uninitialized after copy.
+        let uninit = std::ptr::read(dst);
     }
 }
 
@@ -35,7 +48,20 @@ fn check_copy() {
         let layout = Layout::from_size_align(16, 8).unwrap();
         let src: *mut u8 = alloc(layout);
         let dst: *mut u8 = alloc(layout);
-        copy(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized.
+        // This does not fail, since `copy` is untyped.
+        copy(src as *const u8, dst, 2);
+    }
+}
+
+#[kani::proof]
+fn check_copy_read() {
+    unsafe {
+        let layout = Layout::from_size_align(16, 8).unwrap();
+        let src: *mut u8 = alloc(layout);
+        let dst: *mut u8 = alloc_zeroed(layout);
+        copy(src as *const u8, dst, 2);
+        // ~ERROR: Accessing `dst` here, which became uninitialized after copy.
+        let uninit = std::ptr::read(dst);
     }
 }