Skip to content

Do not show "Generate concrete test" for unsupported cases #91

@celinval

Description

@celinval

Screenshot or description of the issue:

I ran the verification for the code:

unsafe fn use_after_drop(ptr: *mut String) {
    std::ptr::drop_in_place(ptr);
    let _ = *ptr;
}

#[cfg(kani)]
mod harnesses {
    use super::*;
    #[kani::proof]
    fn check_mem_error() {
        let mut string = "hi".to_string();
        unsafe { use_after_drop(&mut string) };
    }
}

I got a bunch of UB and memory safety checks failure. I tried to generate a concrete playback test.

I expected to see this happen: I think there are few possible behaviors:

  1. The command should generate a test. This is ideal but it's a Kani issue (captured here: Concrete playback should support all kind of property failures kani#2163)
  2. The extension shouldn't suggest that this was possible.
  3. The extension should have a pop-up error saying that the property is not supported.

Instead, this happened: Nothing visible happens

Link to PR / commit where the action failed: ed948a5

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions