diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs index ff2d54e7ca6b..744528b9c32a 100644 --- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs +++ b/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); } } diff --git a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs index 2b0e71cc16f3..202900933e00 100644 --- a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs +++ b/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); } } diff --git a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected index 099cbdcd9f1c..62b518815bb0 100644 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected +++ b/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. diff --git a/tests/expected/offset-bounds-check/start_from_oob.expected b/tests/expected/offset-bounds-check/start_from_oob.expected index fc5fbdfb365a..fc766c277581 100644 --- a/tests/expected/offset-bounds-check/start_from_oob.expected +++ b/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. diff --git a/tests/expected/offset-bytes-overflow/expected b/tests/expected/offset-bytes-overflow/expected index 1f13adcc7776..8eae686f2142 100644 --- a/tests/expected/offset-bytes-overflow/expected +++ b/tests/expected/offset-bytes-overflow/expected @@ -1,2 +1,4 @@ -FAILURE\ -offset: attempt to compute number in bytes which would overflow \ No newline at end of file +Failed Checks: Offset in bytes overflow isize +Verification failed for - check_wrap_offset + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-from-bytes-overflow/expected b/tests/expected/offset-from-bytes-overflow/expected index bcf0242f9e9d..51f9bfb293a0 100644 --- a/tests/expected/offset-from-bytes-overflow/expected +++ b/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. diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected index 9613638bf8f9..ba7d1c2fe7df 100644 --- a/tests/expected/offset-overflow/expected +++ b/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. diff --git a/tests/expected/pointer-overflow/expected b/tests/expected/pointer-overflow/expected index 3701d77c8bfd..a6319eb7d1f1 100644 --- a/tests/expected/pointer-overflow/expected +++ b/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 diff --git a/tests/expected/pointer-overflow/main.rs b/tests/expected/pointer-overflow/main.rs index 9c8dc52bddf0..c78cf4027351 100644 --- a/tests/expected/pointer-overflow/main.rs +++ b/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] diff --git a/tests/expected/ptr-offset-overflow-bytes/expected b/tests/expected/ptr-offset-overflow-bytes/expected index ad33ce91dabb..a258cb026a1a 100644 --- a/tests/expected/ptr-offset-overflow-bytes/expected +++ b/tests/expected/ptr-offset-overflow-bytes/expected @@ -1,5 +1,3 @@ -std::ptr::const_ptr::::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. diff --git a/tests/expected/ptr_to_ref_cast/slice/test.rs b/tests/expected/ptr_to_ref_cast/slice/test.rs index 8526d0bf1c7f..b9e4d54546f6 100644 --- a/tests/expected/ptr_to_ref_cast/slice/test.rs +++ b/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()); } diff --git a/tests/expected/raw_slice/expected b/tests/expected/raw_slice/expected index 1b863417c02c..73a625248d51 100644 --- a/tests/expected/raw_slice/expected +++ b/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 diff --git a/tests/expected/raw_slice_c_repr/expected b/tests/expected/raw_slice_c_repr/expected index 9271825be7cd..eca589cdd260 100644 --- a/tests/expected/raw_slice_c_repr/expected +++ b/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 diff --git a/tests/expected/raw_slice_packed/expected b/tests/expected/raw_slice_packed/expected index 9271825be7cd..eca589cdd260 100644 --- a/tests/expected/raw_slice_packed/expected +++ b/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 diff --git a/tests/kani/ValidValues/unaligned.rs b/tests/kani/ValidValues/unaligned.rs index 695f74ebf1b4..dc1d3d897211 100644 --- a/tests/kani/ValidValues/unaligned.rs +++ b/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) })); }