cbmc-viewer icon indicating copy to clipboard operation
cbmc-viewer copied to clipboard

Produce stub and missing function reports

Open markrtuttle opened this issue 3 years ago • 2 comments

  • 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.

markrtuttle avatar Oct 20 '21 22:10 markrtuttle

Could also include expected coverage.

markrtuttle avatar Oct 20 '21 22:10 markrtuttle

A preliminary implementation now appears in the summary directory. This needs to be cleaned up and merged into viewer iteself.

markrtuttle avatar Dec 07 '21 15:12 markrtuttle