Fix tests after enabling offset bound checks

Author: celinval

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

@@ -7,10 +7,10 @@ fn test_copy_nonoverlapping_invalid() {
     let arr: [i32; 3] = [0, 1, 0];
     let src: *const i32 = arr.as_ptr();
 
+    // Get an invalid pointer with a negative offset
+    let src_invalid = src.wrapping_sub(1) as *const i32;
+    let dst = src.wrapping_add(1) as *mut i32;
     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_nonoverlapping(src_invalid, dst, 1);
     }
 }

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

@@ -7,10 +7,10 @@ fn test_copy_invalid() {
     let arr: [i32; 3] = [0, 1, 0];
     let src: *const i32 = arr.as_ptr();
 
+    // Get an invalid pointer with a negative offset
+    let src_invalid = src.wrapping_sub(1) as *const i32;
+    let dst = src.wrapping_add(1) as *mut i32;
     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/offset-bounds-check/out_of_bounds_ub_check.expected

@@ -1,4 +1,4 @@
-Failed Checks: Offset result is out of bounds of initial allocation
+Failed Checks: Offset result and original pointer should point to the same allocation
 Verification failed for - check_ptr_oob
 
 Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/offset-bounds-check/start_from_oob.expected

@@ -1,4 +1,4 @@
-Failed Checks: Offset result is out of bounds of initial allocation
+Failed Checks: Offset result and original pointer should point to the same allocation
 Verification failed for - check_add_to_oob
 
 Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/offset-bytes-overflow/expected

@@ -1,2 +1,4 @@
-FAILURE\
-offset: attempt to compute number in bytes which would overflow
+Failed Checks: Offset in bytes overflow isize
+Verification failed for - check_wrap_offset
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/offset-from-bytes-overflow/expected

@@ -1,2 +1,4 @@
-FAILURE\
-attempt to compute number in bytes which would overflow
+Failed Checks: Offset in bytes overflow isize
+Verification failed for - main
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/offset-overflow/expected

@@ -1,2 +1,4 @@
-FAILURE\
-attempt to compute offset which would overflow
+Failed Checks: Offset result and original pointer should point to the same allocation
+Verification failed for - test_offset_overflow
+
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/pointer-overflow/expected

@@ -1,2 +1 @@
-Status: FAILURE\
-offset: attempt to compute number in bytes which would overflow
+Failed Checks: Offset in bytes overflow isize

tests/expected/pointer-overflow/main.rs

@@ -1,7 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --extra-pointer-checks
 // Checks that overflows for pointer arithmetic are reported
 
 #[kani::proof]

tests/expected/ptr-offset-overflow-bytes/expected

@@ -1,5 +1,3 @@
-std::ptr::const_ptr::<impl *const Foo>::offset.arithmetic_overflow\
-Status: FAILURE\
-Description: "offset: attempt to compute number in bytes which would overflow"
-
-VERIFICATION:- FAILED
+Failed Checks: Offset in bytes overflow isize
+Verification failed for - main
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.