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.
Image a one have a number of GOTO binaries for every target function. For every GOTO binary, CBMC will generate a property, coverage and result reports (in JSON or XML...
The Static Analysis Results Interchange Format ([SARIF](https://sarifweb.azurewebsites.net/)) is an industry standard format for the output of static analysis tools. Github supports SARIF format and allows showing code annotations in a...
CBMC version 6 includes at least one breaking change which was noticeable when the CI system in the `s2n-tls` repo picked it up as a pre-release version in [this run](https://github.com/aws/s2n-tls/actions/runs/7215710149/job/19660493232#step:5:31)....
Required to satisfy the reqs of voluptuous 0.14.0 which now uses type annotations, a python 3.7+ feature. Fixes #146 Sets the minimum python version to 3.7. By submitting this pull...
cbmc-viewer depends on voluptuous which recently (Nov 2023) upgraded from 0.13.1 to 0.14.0. This new version uses `__future__.annotations` which silently require python 3.7 to work (https://github.com/alecthomas/voluptuous/issues/490). cbmc-viewer only lists python...
(moved over from https://github.com/diffblue/cbmc/issues/7865, reported by @ylevhariamzn) CBMC version: 5.87 Operating system: Rocky Linux Exact command line resulting in the issue: What behaviour did you expect: What happened instead: I...
*Issue #, if available:* *Description of changes:* By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Issue #, if available:* *Description of changes:* By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
# Description CBMC Viewer crashes if we generate mcdc, branch, or decision coverage. In this issue we detail the mcdc trace problem. But this can be reproduced with other kind...
CBMC version: `5.69.1 (cbmc-5.59.0-676-gb4a4122dee)` Viewer version: 2.9 Operating system: N/A Exact command line resulting in the issue: First, clone my fork for [coreJSON](https://github.com/feliperodri/coreJSON/tree/JSON_validate-proof). Then, navigate to the proof located at...
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.