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.