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

Kani doesn't have an --exact flag to call for singular harnesses #2285

Closed
jaisnan opened this issue Mar 8, 2023 · 4 comments · Fixed by #2527
Closed

Kani doesn't have an --exact flag to call for singular harnesses #2285

jaisnan opened this issue Mar 8, 2023 · 4 comments · Fixed by #2527
Assignees
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@jaisnan
Copy link
Contributor

jaisnan commented Mar 8, 2023

Requested feature:

Like rust tests, kani needs an --exact flag that matches against a harness instead of the substring match that happens by default. substring match needs to be the default method, but users should be able to specify harnesses.

@jaisnan jaisnan added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Mar 8, 2023
@celinval
Copy link
Contributor

celinval commented Jun 2, 2023

@jaisnan I just wanted to double check if it's OK if we model it the same way as rust tests model --exact? I.e., it requires the fully qualified name for the test function to match the given name.

@jaisnan
Copy link
Contributor Author

jaisnan commented Jun 2, 2023

I have a PR out for the changes to use the fully qualified name, and so far it seems to be working fine.
I'm assuming it won't be necessitated and that the fuzzing search for harnesses that we do have, will work just the same. If so, I say that we add the --exact flag the way you're suggesting, and that the extension should use it by default but it will also use the fuzzing approach as a backup if that fails. Do you think that will work?

@celinval
Copy link
Contributor

celinval commented Jun 2, 2023

Yes. Once we have the list harness option, it will be easier to know for sure the qualified name too.

@jaisnan
Copy link
Contributor Author

jaisnan commented Jun 2, 2023

Makes sense to me to model it after cargo. Good for the long term as well.

@jaisnan jaisnan self-assigned this Jun 8, 2023
@jaisnan jaisnan mentioned this issue Jun 14, 2023
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants