Skip to content

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

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

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions