Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Kani does not detect UB for ptr_offset_from and ptr_offset_from_unsigned #3756

Open
celinval opened this issue Dec 5, 2024 · 0 comments · May be fixed by #3757
Open

Kani does not detect UB for ptr_offset_from and ptr_offset_from_unsigned #3756

celinval opened this issue Dec 5, 2024 · 0 comments · May be fixed by #3757
Labels
[C] Bug This is a bug. Something isn't working. [E] Unsupported UB Undefined behavior that Kani does not detect [F] Soundness Kani failed to detect an issue

Comments

@celinval
Copy link
Contributor

celinval commented Dec 5, 2024

#[kani::proof]
fn check_offset_from() {
    let val = 10u128;
    let ptr: *const u128 = &val;
    let ptr_oob: *const u128 = ptr.wrapping_add(10);
    // SAFETY: This is not safe!
    let _offset = unsafe { ptr_oob.offset_from(ptr) };
}

using the following command line invocation:

kani check_ub.rs

with Kani version: 0.56.0

I expected to see this happen: Verification fails due to UB detection

Instead, this happened: Verification succeeds

@celinval celinval added [C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue [E] Unsupported UB Undefined behavior that Kani does not detect labels Dec 5, 2024
@celinval celinval linked a pull request Dec 5, 2024 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [E] Unsupported UB Undefined behavior that Kani does not detect [F] Soundness Kani failed to detect an issue
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant