search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.23k stars 90 forks source link

RFC: Output - Other tool versions #2572

Open adpaco-aws opened 1 year ago

adpaco-aws commented 1 year ago

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.

JustusAdam commented 1 year ago

I like this idea. Given that we'll probably end up printing the Kani version by default guarding this one behind --version makes sense to me.

Also I'd include the supported Rust(c) version

celinval commented 1 year ago

Or even under --version --verbose. BTW, I also don't think this change is worth an RFC.