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.

model-checking, updated 🕥 2023-01-18 22:55:26

CBMC Viewer

CBMC is a Bounded Model Checker for C. It can prove that (for computations of bounded depth) a C program exhibits no memory safe errors (no buffer overflows, no invalid pointers, etc), no undefined behaviors, and no failures of assertions in the code. CBMC Viewer is a tool that scans the output of CBMC and produces a browsable summary of its findings.

Example

Here is a simple example of using cbmc-viewer. Running this example requires installing CBMC. Installation on MacOS is just brew install cbmc. Installation on other operation systems is described on the CBMC release page.

Create a source file main.c containing ```

include

static int global;

int main() { int *ptr = malloc(sizeof(int));

assert(global > 0); assert(*ptr > 0);

return 0; } and run the commands goto-cc -o main.goto main.c cbmc main.goto --trace --xml-ui > result.xml cbmc main.goto --cover location --xml-ui > coverage.xml cbmc main.goto --show-properties --xml-ui > property.xml cbmc-viewer --goto main.goto --result result.xml --coverage coverage.xml --property property.xml --srcdir . and open the report created by cbmc-viewer in a web browser with open report/html/index.html ```

What you will see is

A coverage report summarizing what lines of source code were exercised by cbmc. In this case, coverage is 100%. Clicking on main, you can see the source code for main annotated with coverage data (all lines are green because all lines were hit).
A bug report summarizing what issues cbmc found with the code. In this case, the bugs are violations of the assertions because, for example, it is possible that the uninitialized integer allocated on the heap contains a negative value. For each bug, there is a link to
- The line of code where the bug occurred.
- An error trace showing the steps of the program leading to the bug. For each step, there a link to the line of code that generated the step, making it easy to follow the error trace and root cause the bug.

Documentation

The cbmc-viewer documentation includes a reference manual and a user guide. These documents are currently works in progress and will improve over time.

Installation

Most people should just follow the instructions on the release page.

Developers can install the package in Python "development mode" as follows.

Clone the repository and install dependencies with git clone https://github.com/awslabs/aws-viewer-for-cbmc.git cbmc-viewer apt install python3-pip python3-venv python3-jinja2 python3-voluptuous universal-ctags Installing ctags is optional. See the ctags discussion at the end of the release page.
Install development mode with cd cbmc-viewer make develop export PATH=/tmp/cbmc-viewer/bin:$PATH
Uninstall development mode with cd cbmc-viewer make undevelop

Security

See CONTRIBUTING for more information.

License

This project is licensed under the Apache-2.0 License.

Issues

[IGNORE] TEMP

opened on 2023-01-18 22:55:26 by ronakfof

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.

[IGNORE] TEMP

opened on 2023-01-18 20:47:07 by ronakfof

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.

Viewer Crashes when selected coverage is different from `location` e.g `mcdc` or `branch`

opened on 2022-12-15 15:26:50 by FlorianBarrau

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 of coverage : branch, decision etc...

CBMC Viewer Version : 3.6 CBMC Version : 5.72.2 Ubuntu 18.04 GCC 7.5

How to reproduce

Take the example from the README
Replace coverage by mcdc for example goto-cc -o main.goto main.c cbmc main.goto --trace --xml-ui > result.xml cbmc main.goto --cover mcdc --xml-ui > coverage.xml cbmc main.goto --show-properties --xml-ui > property.xml cbmc-viewer --goto main.goto --result result.xml --coverage coverage.xml --property property.xml --srcdir .
CBMC Viewer trace ```bash Traceback (most recent call last): File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 506, in parse_description basic_block = re.match(r'block [0-9]+ (lines (.*))', description).group(1) AttributeError: 'NoneType' object has no attribute 'group'

The above exception was the direct cause of the following exception:

Traceback (most recent call last): File "/data/home/fb/.local/bin/cbmc-viewer", line 11, in sys.exit(main()) File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/cbmc_viewer.py", line 13, in main args.func(args) File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/viewer.py", line 98, in viewer coverage = coveraget.make_and_save_coverage(args, jsondir / 'viewer-coverage.json') File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 616, in make_and_save_coverage obj = make_coverage(args) File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 605, in make_coverage return CoverageFromCbmcXml(cbmc_coverage, srcdir) File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in init [load_cbmc_xml(xml_file, root) for xml_file in xml_files] File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 390, in [load_cbmc_xml(xml_file, root) for xml_file in xml_files] File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 403, in load_cbmc_xml parse_description(goal.get("description"))) File "/data/home/fb/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 525, in parse_description raise UserWarning(f'Unexpected coverage goal description: "{description}"') from error UserWarning: Unexpected coverage goal description: "decision/condition 'global > 0' false" ```

Other traces for different kind of coverage

Decision ```bash Traceback (most recent call last): File "/data/home/f00494530/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 506, in parse_description basic_block = re.match(r'block [0-9]+ (lines (.*))', description).group(1) AttributeError: 'NoneType' object has no attribute 'group'

The above exception was the direct cause of the following exception:

```

Branch ```bash Traceback (most recent call last): File "/data/home/f00494530/.local/lib/python3.6/site-packages/cbmc_viewer/coveraget.py", line 506, in parse_description basic_block = re.match(r'block [0-9]+ (lines (.*))', description).group(1) AttributeError: 'NoneType' object has no attribute 'group'

The above exception was the direct cause of the following exception:

```

Test `config.py` crashes with commands that have no arguments

opened on 2022-12-12 21:48:25 by karkhaz

The config.py script used as a test in the CBMC starter kit crashes when the starter kit includes a Litani job whose command has no arguments.

The crash is on line 80 of config.py: cmd, args = job['command'].strip().split(maxsplit=1) A job's command is not guaranteed to have arguments, so the split can fail.

Suppress unhelpful warnings for better user experience

opened on 2022-11-23 17:25:27 by feliperodri

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. Then, navigate to the proof located at coreJSON/verification/cbmc/proofs/skipString/. Finally, run the proof using make veryclean; time make. What behaviour did you expect: No warnings. What happened instead: I keep getting the following warnings without any source location.

``` WARNING: Skipping redefinition of symbol name: JSON_Iterate

WARNING: Old symbol JSON_Iterate: file verification/cbmc/proofs/skipString/core_json.c, line 1774

WARNING: New symbol JSON_Iterate: file source/include/core_json.h, line 326

WARNING: Skipping redefinition of symbol name: JSON_Validate

WARNING: Old symbol JSON_Validate: file verification/cbmc/proofs/skipString/core_json.c, line 1129

WARNING: New symbol JSON_Validate: file source/include/core_json.h, line 91

WARNING: Skipping redefinition of symbol name: skipAnyScalar

WARNING: Old symbol skipAnyScalar: file verification/cbmc/include/core_json_annex.h, line 120

WARNING: New symbol skipAnyScalar: file verification/cbmc/proofs/skipString/core_json.c, line 848

WARNING: Skipping redefinition of symbol name: skipCollection

WARNING: Old symbol skipCollection: file verification/cbmc/include/core_json_annex.h, line 95

WARNING: New symbol skipCollection: file verification/cbmc/proofs/skipString/core_json.c, line 1049

WARNING: Skipping redefinition of symbol name: skipScalars

WARNING: Old symbol skipScalars: file verification/cbmc/include/core_json_annex.h, line 106

WARNING: New symbol skipScalars: file verification/cbmc/proofs/skipString/core_json.c, line 1012

WARNING: Skipping redefinition of symbol name: skipSpace

WARNING: Old symbol skipSpace: file verification/cbmc/include/core_json_annex.h, line 132

WARNING: New symbol skipSpace: file verification/cbmc/proofs/skipString/core_json.c, line 72

WARNING: Skipping redefinition of symbol name: skipString

WARNING: Old symbol skipString: file verification/cbmc/include/core_json_annex.h, line 143

WARNING: New symbol skipString: file verification/cbmc/proofs/skipString/core_json.c, line 509

WARNING: Skipping redefinition of symbol name: skipString

WARNING: Old symbol skipString: file verification/cbmc/include/core_json_annex.h, line 143

WARNING: New symbol skipString: file MISSING, line 0

WARNING: Skipping source file annotation: wrapped functions for code contracts ``` Also, what does these warnings mean?

If this doesn't compromise the coverage report, then it should only be INFO instead of warnings.

How to report coverage for function contracts replacement?

opened on 2022-11-04 18:10:21 by feliperodri None

Releases

viewer-3.8 2022-12-16 17:52:07

This is CBMC Viewer version 3.8.

On MacOS, you can install with brew: brew install aws/tap/cbmc-viewer The prefix aws/tap refers to the AWS repository with the brew package.

On all machines, you can install with pip: python3 -m pip install cbmc-viewer

For best results, install universal ctags or exuberant ctags with

MacOS: brew install universal-ctags or brew install ctags
Ubuntu: sudo apt install universal-ctags or sudo apt install ctags
Windows: Follow the installation instructions in the universal-ctags or exuberant ctags repository.

The installation of ctags is optional, but without ctags, cbmc-viewer will fail to link some symbols appearing in error traces to their definitions in the source code. The ctags tool has a long history. The original ctags was replaced by exhuberant ctags which was replaced by universal ctags. They all claim to be backwards compatible. We recommend universal ctags.

viewer-3.7 2022-12-16 17:08:25

This is CBMC Viewer version 3.7.

On MacOS, you can install with brew: brew install aws/tap/cbmc-viewer The prefix aws/tap refers to the AWS repository with the brew package.

On all machines, you can install with pip: python3 -m pip install cbmc-viewer

For best results, install universal ctags or exuberant ctags with

MacOS: brew install universal-ctags or brew install ctags
Ubuntu: sudo apt install universal-ctags or sudo apt install ctags
Windows: Follow the installation instructions in the universal-ctags or exuberant ctags repository.

viewer-3.6 2022-07-12 16:00:19

This is CBMC Viewer version 3.6.

On MacOS, you can install with brew: brew install aws/tap/cbmc-viewer The prefix aws/tap refers to the AWS repository with the brew package.

On all machines, you can install with pip: python3 -m pip install cbmc-viewer

For best results, install universal ctags or exuberant ctags with

MacOS: brew install universal-ctags or brew install ctags
Ubuntu: sudo apt install universal-ctags or sudo apt install ctags
Windows: Follow the installation instructions in the universal-ctags or exuberant ctags repository.

viewer-3.5 2022-06-10 20:06:20

This is CBMC Viewer version 3.5.

On MacOS, you can install with brew: brew install aws/tap/cbmc-viewer The prefix aws/tap refers to the AWS repository with the brew package.

On all machines, you can install with pip: python3 -m pip install cbmc-viewer

For best results, install universal ctags or exuberant ctags with

MacOS: brew install universal-ctags or brew install ctags
Ubuntu: sudo apt install universal-ctags or sudo apt install ctags
Windows: Follow the installation instructions in the universal-ctags or exuberant ctags repository.

viewer-3.4 2022-05-25 21:16:05

This is CBMC Viewer version 3.4.

On MacOS, you can install with brew: brew install aws/tap/cbmc-viewer The prefix aws/tap refers to the AWS repository with the brew package.

On all machines, you can install with pip: python3 -m pip install cbmc-viewer

For best results, install universal ctags or exuberant ctags with

MacOS: brew install universal-ctags or brew install ctags
Ubuntu: sudo apt install universal-ctags or sudo apt install ctags
Windows: Follow the installation instructions in the universal-ctags or exuberant ctags repository.

viewer-3.3 2022-05-20 18:43:58

This is CBMC Viewer version 3.3.

On MacOS, you can install with brew: brew install aws/tap/cbmc-viewer The prefix aws/tap refers to the AWS repository with the brew package.

On all machines, you can install with pip: python3 -m pip install cbmc-viewer

For best results, install universal ctags or exuberant ctags with

MacOS: brew install universal-ctags or brew install ctags
Ubuntu: sudo apt install universal-ctags or sudo apt install ctags
Windows: Follow the installation instructions in the universal-ctags or exuberant ctags repository.

model-checking

GitHub Repository Homepage