Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
jaisnan opened this issue Feb 23, 2023 · 3 comments
Assignees
Labels
bug Something isn't working

Comments

@jaisnan
Copy link
Contributor

jaisnan commented Feb 23, 2023

The changes to model-checking/kani#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 jaisnan added the bug Something isn't working label Feb 23, 2023
@jaisnan jaisnan changed the title Querying kani with exact function breaks output parsing Querying kani with --harness breaks output parsing Feb 23, 2023
@jaisnan
Copy link
Contributor Author

jaisnan commented Feb 23, 2023

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
Copy link
Contributor

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

@jaisnan
Copy link
Contributor Author

jaisnan commented May 11, 2023

#56 is related to this issue.

@jaisnan jaisnan changed the title Querying kani with --harness breaks output parsing Harnesses with overlapping substrings result in multiple harness being run Jun 9, 2023
@jaisnan jaisnan self-assigned this Jun 20, 2023
@jaisnan jaisnan moved this to In Progress in Kani 2023-07-10 Jun 20, 2023
@adpaco-aws adpaco-aws moved this from In Progress to Done in Kani 2023-07-10 Jul 10, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
No open projects
Status: Done
Development

No branches or pull requests

2 participants