Requested feature: Users should have a mechanism allowing them to easily specify a subset of harnesses to run under Kani.
Use case: There are multiple possible use cases.
- Slow vs fast proofs: users may wish to run slow proofs nightly, but fast proofs on every commit
- Feature gates: users may wish to verify feature-gated code. Their harness should respect the same feature gate
- Polymorphic proofs: users may wish to run with a single instance in a quick test set, then run with a wider set of types in a complete set
- Proofs under development: users may wish to check in proofs under development, but only have them run when ready.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Potential mechanisms:
- Feature gates: Put the proof harnesses under standard rust feature gates.
- Tags: allow users to annotate proofs with tags, and then
cargo-kani only runs a select set of tagged proofs
- Regular expressions/globs:
cargo-kani could take a regexp argument, and only run proofs that match the regexp.
Test case: File with multiple harnesses, different kani runs that only execute some of them.
Requested feature: Users should have a mechanism allowing them to easily specify a subset of harnesses to run under Kani.
Use case: There are multiple possible use cases.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Potential mechanisms:
cargo-kanionly runs a select set of tagged proofscargo-kanicould take a regexp argument, and only run proofs that match the regexp.Test case: File with multiple harnesses, different kani runs that only execute some of them.