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.

Sign up for GitHub

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

Jump to bottom

Create a command to play a counter example #2440

Closed
celinval opened this issue May 12, 2023 · 0 comments · Fixed by #2464
Closed

Create a command to play a counter example #2440

celinval opened this issue May 12, 2023 · 0 comments · Fixed by #2464
Assignees
@celinval
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@celinval
Copy link
Contributor

Requested feature: User should be able to run a unit test generated by Kani with one command which would incorporate stubs / kani library and other steps that today don't work or require extra configuration.
Use case: Running concrete playback without this extra setup step: https://model-checking.github.io/kani/debugging-verification-failures.html#setup
Link to relevant documentation (Rust reference, Nomicon, RFC):

Notes: We should accept a similar arguments as cargo test and accept a runner.
@celinval celinval added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label May 12, 2023
@celinval celinval mentioned this issue May 12, 2023
Closed
@celinval celinval self-assigned this May 16, 2023
@celinval celinval mentioned this issue May 17, 2023
Merged
4 tasks
celinval added a commit that referenced this issue May 20, 2023
@celinval
Move common arguments to their own structure (#2449)
ef1358d 
This is a pre-work needed for implementing #2440 as a subcommand. Today, the only other subcommand we have is assess and the way it takes arguments is rather broken as explained in #1831.

For the playback sub-command, I expect that we will need at least CargoArgs and CommonArgs to control the build process and to control the process verbosity.
@celinval celinval mentioned this issue May 23, 2023
Merged
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
No open projects
Kani 2023-05-29
Status: In Progress
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Create a playback command to make it easier to run Kani generated tests celinval/kani-dev
1 participant
@celinval