Spurious failure in pointer offset #3582
Description
I tried this code:
#[kani::proof]
fn check_foo() {
let x: u8 = 0;
let ptr: *const u8 = &x as *const u8;
let count = isize::MAX - 800;
let _ = ptr.wrapping_offset(count);
}using the following command line invocation:
kani lib.rs
with Kani version: fe17fdc
I expected to see this happen: Verification successful.
Instead, this happened: Verification failed:
RESULTS:
Check 1: std::ptr::const_ptr::<impl *const u8>::wrapping_offset.arithmetic_overflow.1
- Status: SUCCESS
- Description: "arith_offset: attempt to compute number in bytes which would overflow"
- Location: ../../../.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:481:18 in function std::ptr::const_ptr::<impl *const u8>::wrapping_offset
Check 2: std::ptr::const_ptr::<impl *const u8>::wrapping_offset.arithmetic_overflow.2
- Status: FAILURE
- Description: "attempt to compute offset which would overflow"
- Location: ../../../.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:481:18 in function std::ptr::const_ptr::<impl *const u8>::wrapping_offset
Check 3: check_foo.assertion.1
- Status: SUCCESS
- Description: "attempt to subtract with overflow"
- Location: lib.rs:5:17 in function check_foo
SUMMARY:
** 1 of 3 failed
Failed Checks: attempt to compute offset which would overflow
File: "/home/ubuntu/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 481, in std::ptr::const_ptr::<impl *const u8>::wrapping_offset
VERIFICATION:- FAILED