Pointer sub() operation is giving spurious overflow check error #1082
Description
I tried this code:
#[kani::proof]
fn check_thin_ptr() {
let array = [0, 1, 2, 3, 4, 5, 6];
let second_ptr: *const i32 = &array[3];
unsafe {
let before = second_ptr.sub(1);
assert_eq!(*before, 2);
}
}using the following command line invocation:
kani <test_file>
with Kani version:
I expected to see this happen: Verification succeed.
Instead, this happened: It fails with the following message:
SUMMARY:
** 1 of 9 failed
Failed Checks: attempt to compute offset which would overflow
File: "rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 295, in std::ptr::const_ptr::<impl *const T>::offset
VERIFICATION:- FAILED