cbmc-viewer
cbmc-viewer copied to clipboard
Produce stub and missing function reports
- Create a "proof assumptions" section in report that lists all expected stubs and expected undefined functions. The definition of expected comes from the cbmc-viewer.json proof configuration file.
- Report unexpected stubs and unexpected undefined functions as errors and alarm on them.
- Summarize this information across all proofs on the litani report with histograms.
Could also include expected coverage.
A preliminary implementation now appears in the summary directory. This needs to be cleaned up and merged into viewer iteself.