cbmc-viewer
cbmc-viewer copied to clipboard
model-checking
CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
The `config.py` script used as a test in the [CBMC starter kit](https://github.com/model-checking/cbmc-starter-kit) crashes when the starter kit includes a Litani job whose command has no arguments. The crash is on...
The functions [link_text_to_file](https://github.com/awslabs/aws-viewer-for-cbmc/blob/aff75c57673da2dd092f98f9491a37a7f07250e7/cbmc_viewer/markup_link.py#L44) and [link_text_to_line](https://github.com/awslabs/aws-viewer-for-cbmc/blob/aff75c57673da2dd092f98f9491a37a7f07250e7/cbmc_viewer/markup_link.py#L54) should take an option "escape=True" argument and invoke html.escape on the text strings when escape is true. The invocation of html.escape in [format_srcloc](https://github.com/awslabs/aws-viewer-for-cbmc/blob/60c47b13b64265112d3b4b2fe2498049be524fcb/cbmc_viewer/markup_trace.py#L152) should be...
Replace os.path with pathlib.Path for readability and portability across operating systems.
Currently, when the `--property` flag is omitted, the errors are reported as "other errors" without line numbers or traces. All that is missing is the property description from the `--property`...
- 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...
We should restrict coverage to the reachable functions. Currently coverage checking reports coverage on all code, not just the statically reachable code. Prior attempts to restrict to reachable functions were...
See https://github.com/awslabs/aws-viewer-for-cbmc/blob/master/cbmc_viewer/coveraget.py.
*Issue #, if available:* *Description of changes:* Generate pointer alias analysis report using points-to set metric information from CBMC. Takes json output obtained from cbmc --show-points-to-sets and generates a html...
Metadata
Owner
Metadata
CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.