Skip to content

Kani should fail due to invalid access of a dead local variable via raw pointer #3061

@celinval

Description

@celinval

I tried this code:

#[kani::proof]
pub fn check_invalid_ptr() {
    let raw_ptr = {
        let var = 10;
        &var as *const _
    };
    // This should fail since it is de-referencing a dead object.
    assert_eq !(unsafe {*raw_ptr}, 10);
}

using the following command line invocation:

kani invalid_ptr.rs

with Kani version: 0.47

I expected to see this happen: Verification should fail since the de-referenced pointer is pointing to a dead object.
Instead, this happened: Verification succeeds

Metadata

Metadata

Assignees

Labels

T-High PriorityTag issues that have high priority[C] BugThis is a bug. Something isn't working.[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