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.
*Issue #, if available:* *Description of changes:* Displays the type and count of array constraints being added during post processing. Often has a direct correlation to the post processing runtime....
*Issue #, if available:* *Description of changes:* Add memopt module to parse json formatted goto program (cbmc --show-goto-functions --json-ui) to record all calls to memory operations: memcpy, memcmp, memchr, memmove,...
*Issue #, if available:* *Description of changes:* Add metric-report module to read viewer json logs and generate a consolidated runtime analysis report across multiple proofs. By submitting this pull request,...
*Issue #, if available:* *Description of changes:* Provides mapping between clauses and program instructions. Highlights instructions that contribute to the UNSAT core and provides a list of program lines that...
*Issue #, if available:* *Description of changes:* Add module to generate byte op metric report using CBMC output produced by --show-byte-ops. Takes a json file as input and generates a...
In a view of a Trace reported by cbmc-viewer, I am unable to get the "Shift-Alt-Click" navigation action to work on macOS. I have also tried to modify the viewer.js...
*Description of changes:* Use GitHub's log masking to ensure even tokens that do not match GitHub's default filter are replaced by asterisks. By submitting this pull request, I confirm that...
*Description of changes:* Parsing CBMC's results in a memory consumption that is 100 times the size of the input file. Switching to cElementTree appears to halve the memory footprint, which...
upload-release-asset is long deprecated. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Description of changes:* The HTML rendering of property failures should not include (broken) links to counterexample traces the property status of which is "UNKNOWN". By submitting this pull request, I...
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.