model-checking / kani-vscode-extension

Kani VSCode Extension
https://marketplace.visualstudio.com/items?itemName=model-checking.kani-vscode-extension
Apache License 2.0
15 stars 10 forks source link

Harnesses with overlapping substrings result in multiple harness being run #39

Open jaisnan opened 1 year ago

jaisnan commented 1 year ago

The changes to https://github.com/model-checking/kani/pull/2202 change how kani x.rs --harness "y" output looks like, and now it returns a fuzzy result, the extension needs to search for the exact harness.

For example,

if there are two functions


fn function_1() {
...
}

fn function_11() {
...
}

the extension queries the output from kani for both the harnesses with the command kani x.rs --harness function_1

jaisnan commented 1 year ago

If there's no way to run a single harness without ensuring that only that harness is run, maybe we could throw a warning to rename the harness to something unique (could modify the function ourselves before running the query).

celinval commented 1 year ago

That's a good point. Can you see how the rust vscode plugin handle that?

jaisnan commented 1 year ago

56 is related to this issue.