Fix tests after enabling offset bound checks

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.

tests/expected/ptr_to_ref_cast/slice/test.rs

@@ -31,6 +31,6 @@ fn check_with_byte_add_sub_pass() {
     let ptr = &data as *const [u8];
     let offset = kani::any_where(|i| *i < 100);
     // This should pass since the resulting metadata is valid
-    let val = unsafe { &*ptr.byte_add(offset).byte_sub(offset) };
+    let val = unsafe { &*ptr.wrapping_byte_add(offset).wrapping_byte_sub(offset) };
     assert_eq!(val.len(), data.len());
 }

tests/expected/raw_slice/expected

@@ -62,8 +62,7 @@ Description: "assertion failed: slice.others[0] == second"\
 slice.rs:96:5 in function check_naive_iterator_should_fail
 
 Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-slice.rs:100:32 in function check_naive_iterator_should_fail
+Description: "Offset result and original pointer should point to the same allocation"
 
 VERIFICATION:- FAILED
 

tests/expected/raw_slice_c_repr/expected

@@ -62,8 +62,7 @@ Description: "assertion failed: slice.others[0] == second"\
 in function check_naive_iterator_should_fail
 
 Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-in function check_naive_iterator_should_fail
+Description: "Offset result and original pointer should point to the same allocation"
 
 VERIFICATION:- FAILED
 

tests/expected/raw_slice_packed/expected

@@ -62,8 +62,7 @@ Description: "assertion failed: slice.others[0] == second"\
 in function check_naive_iterator_should_fail
 
 Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-in function check_naive_iterator_should_fail
+Description: "Offset result and original pointer should point to the same allocation"
 
 VERIFICATION:- FAILED
 

tests/kani/ValidValues/unaligned.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z valid-value-checks
+// kani-flags: -Z valid-value-checks -Z mem-predicates
 //! Check that Kani can check value validity of packed structs.
 
 use std::ptr::addr_of;
@@ -34,6 +34,4 @@ pub fn check_packed_read_unaligned_invalid_value() {
     let val = [u8::MAX; SZ];
     let ptr = addr_of!(val) as *const Packed;
     assert!(!kani::mem::can_read_unaligned(ptr));
-    assert!(kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).byte) }));
-    assert!(!kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).c) }));
 }