Reduce CBMC verbosity to CBMC's default#3398
Reduce CBMC verbosity to CBMC's default#3398tautschnig wants to merge 2 commits intomodel-checking:mainfrom
Conversation
CBMC v6 included changes to hide timing information and loop unwinding status output at the default verbosity. To not impact Kani users, model-checking#2995 included changes to make Kani run CBMC with `--verbosity 9`. This change now makes Kani run CBMC with just the default verbosity, hiding timing information and loop unwinding status by default. If users still wish to see this information, they can invoke Kani with `--cbmc args --verbosity 9`.
There was a problem hiding this comment.
I would suggest packaging this in a Kani-level option (e.g. --verbose_solver). The user should not be required to use --cbmc-args except in very unusual cases, and I think it will be common for users to need this option to debug a run that is not terminating (e.g. to understand whether it's stuck in unwinding, symex, or solver stage).
We also need to highlight this change in the CHANGELOG.md.
Marking this PR as "Draft," which I actually meant to do from the start: we should really review the verbosity levels on the CBMC side as at least some of the information that's now hidden at the default verbosity (such as unwinding information) is practically very important. (Timing information, however, is probably not very important.) I suggest we revisit this PR once we have a better situation on the CBMC side, at which point it may well be possible to merge this one as-is. |
3 participants
CBMC v6 included changes to hide timing information and loop unwinding status output at the default verbosity. To not impact Kani users, #2995 included changes to make Kani run CBMC with
--verbosity 9. This change now makes Kani run CBMC with just the default verbosity, hiding timing information and loop unwinding status by default. If users still wish to see this information, they can invoke Kani with--cbmc args --verbosity 9.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.