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/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_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/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) }));
 }