Skip to content

Kani does not detect UB for ptr_offset_from and ptr_offset_from_unsigned #3756

@celinval

Description

@celinval
#[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

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.[E] Unsupported UBUndefined behavior that Kani does not detect[F] SoundnessKani failed to detect an issue

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions