RFC: Output - Harness listing/enumeration #2573
Assignees
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
T-RFC
Label RFC PRs and Issues
Comments
adpaco-aws
added
[C] Feature / Enhancement
|
I think this is related to #1612. I think we should add a list option / subcommand. I would also suggest that we list all the contracts in Kani |
github-merge-queue bot
pushed a commit
that referenced
this issue
Sep 3, 2024
RFC for the `kani list` subcommand. I saw the comment [in the template](https://github.com/model-checking/kani/blob/main/rfc/src/template.md#software-design) to leave the Software Design section empty, but I was looking at the raw MD file and made the mistake of thinking it referred to all sections below the comment. In other words, I thought when it said "We recommend you to leave this empty for the first version of your RFC" it meant that everything below the comment should be empty (so Rationale, Open Questions, and Future Work) and not Software Design. I realized my mistake when I was making this PR, but I figured I may as well leave it since I already wrote it. I [opened a PR](#3462) to update the comment. Resolves [#2573](#2573), [#1612](##1612). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Requested feature: A section of our output dedicated to enumerating or listing harnesses found in a project, how many will run for verification, etc. This is likely a requirement for #2563 , which will be an attempt to represent multi-harness progress.
Use case: Multi-harness verification - Nowadays users don't get any feedback about which harnesses are run or in which order.
Link to relevant documentation (Rust reference, Nomicon, RFC): #2563
The text was updated successfully, but these errors were encountered: