Repository navigation
RFC: Output - Other tool versions #2572
Description
Requested feature: Kani uses a bunch of other tools (engines, solvers, etc.) to do its job. At present, the only version being reported is CBMC's (and maybe some SAT solver through CBMC's output?), but it'd nicer to have versions for all the artifacts to be used printed after collecting harness metadata. What I'm considering now is something like this:
Versions:
- engine: cbmc 5.89.0
- solvers: minisat X.Y.Z, kissat A.B.C
- viewer: ...
This would allow users to check all versions (except for Kani's version, unless we added it here) in a single place. However, we could also hide this information by default and enable it through --verbose.
Use case: Geared towards multi-harness verification in particular.
Activity
[-]RFC: Other tool versions[/-][+]RFC: Output - Other tool versions[/+]JustusAdam commentedon Jun 27, 2023
I like this idea.
Given that we'll probably end up printing the Kani version by default guarding this one behind
--versionmakes sense to me.Also I'd include the supported Rust(c) version
celinval commentedon Jun 28, 2023
Or even under
--version --verbose. BTW, I also don't think this change is worth an RFC.Export the version of every tool the run uses
Add `--export-json` for structured verification results (model-checki…
Restore tool versions and add a stable harness selector
RFC: Structured verification results (export-json) (model-checking#4727)