CBMC viewer

CBMC is a model checker for C. This means that CBMC will explore all possible paths through your code on all possible inputs, and will check that all assertions in your code are true. CBMC can also check for the possibility of memory safety errors (like buffer overflow) and for instances of undefined behavior (like signed integer overflow). CBMC is a bounded model checker, however, which means that using CBMC may require restricting this set of all possible inputs to inputs of some bounded size.

CBMC Viewer is a tool that scans the output of CBMC and produces a browsable summary of its findings.

Installation

Brew installation

On MacOS, we recommend installing with brew. Install with

  brew tap aws/tap
  brew install cbmc-viewer universal-ctags

and upgrade to the latest version with

  brew upgrade cbmc-viewer

The brew home page gives instructions for installing brew. The command brew tap aws/tap taps the AWS repository that contains the brew package. Installing ctags is optional, see below.

Pip installation

On all machines, you can install with pip. Install with

  python3 -m pip install cbmc-viewer
  brew install universal-ctags

  python3 -m pip install cbmc-viewer
  apt install universal-ctags

and upgrade to the latest version with

  python3 -m pip install --upgrade cbmc-viewer

The python download page gives instructions for installing python and pip. Installing ctags is optional, see below.

Developers

Developers can install the package in "editable mode" which makes it possible to modify the code in the source tree and then run the command from the command line as usual to test the changes. First, optionally install ctags as described above. Then

Clone the repository with

git clone https://github.com/model-checking/cbmc-viewer cbmc-viewer

Install into a virtual environment with
```
cd cbmc-viewer
make develop
```
At this point you can either activate the virtual environment with
```
source /tmp/cbmc-viewer/bin/activate
```
or simply add the virtual environment to your path with
```
export PATH=$PATH:/tmp/cbmc-viewer/bin
```
Uninstall with
```
cd cbmc-viewer
make undevelop
```

Installation notes

If you have difficulty installing these tools, please let us know by submitting a GitHub issue.

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 resplaced by exhuberant ctags which was replaced by universal ctags. They all claim to be backwards compatible. We recommend universal ctags.

Tutorial

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 <stdlib.h>

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.

Reference manual

CBMC Viewer produces a browsable summary of CBMC results.

This report includes a summary of CBMC's property checking results. The summary lists each property CBMC was able to violate along with a error trace demonstrating the program execution CBMC discovered that violates the property. Each step of the error trace is linked back to the line of source code that generated the step, making it easier to follow the error trace through the source code and debug the issue raised by CBMC.

This report also includes a summary of the code coverage CBMC attained during property checking. In the process of considering all possible executions through the code on all possible inputs, CBMC is able to exercise some lines of code and not other others. The code coverage summary computes the fraction of statically reachable code that CBMC was able to exercise. The source code itself is annotated in the style of gcov with reachable lines colored green and unreachable lines colored red.

By default, this report is written to report/html.

Here is the reference manual for cbmc-viewer:

cbmc-viewer

CBMC Viewer also produces summaries that will be of no interested to most users, but they summarize the analysis that CBMC Viewer does to produce the main report in the form of json files. By default, these summaries are written to report/json. For example, the file report/json/viewer-coverage.json lists each line of statically-reachable source code and whether that line was hit or missed by CBMC. It also lists for each statically-reachable function the fraction of lines hit. CBMC Viewer provides a collection of subcommands that provide command-line interfaces to these analyses. For example, the subcommand cbmc-viewer coverage will generate the the json describing code coverage that cbmc-viewer itself would write to report/json/viewer-coverage.json.

Here are the reference manuals for cbmc-viewer subcommands:

cbmc-viewer coverage: Summarize coverage checking results
cbmc-viewer loop: List loops found in the goto binary
cbmc-viewer property: List properties checked for during property checking
cbmc-viewer reachable: List reachable functions in the goto binary
cbmc-viewer result: Summarize property checking results
cbmc-viewer source: List source files used to build the goto binary
cbmc-viewer symbol: List symbols found in the goto binary
cbmc-viewer trace: List error traces generated for issues found during property checking

Reference manual

Name

cbmc-viewer - Generate a browsable summary of CBMC results

Synopsis

cbmc-viewer [-h] [--result FILE [FILE ...]]
                 [--coverage FILE [FILE ...]] [--property FILE [FILE ...]]
                 [--srcdir SRCDIR] [--exclude EXCLUDE] [--extensions REGEXP]
                 [--source-method MHD] [--wkdir WKDIR] [--goto GOTO]
                 [--reportdir REPORTDIR] [--json-summary JSON]
                 [--viewer-coverage JSON [JSON ...]]
                 [--viewer-loop JSON [JSON ...]]
                 [--viewer-property JSON [JSON ...]]
                 [--viewer-reachable JSON [JSON ...]]
                 [--viewer-result JSON [JSON ...]]
                 [--viewer-source JSON [JSON ...]]
                 [--viewer-symbol JSON [JSON ...]]
                 [--viewer-trace JSON [JSON ...]] [--verbose] [--debug]
                 [--config JSON] [--version] [--block BLOCK]
                 [--htmldir HTMLDIR] [--srcexclude EXCLUDE]
                 [--blddir BLDDIR] [--storm STORM]

Description

CBMC Viewer generates a browsable summary of CBMC results that makes it easy to root cause issues found by CBMC.

Options

CBMC output

This is the output of cbmc that is summarized by cbmc-viewer.

The output of cbmc can be text, xml, or json. cbmc outputs text by default, but cbmc --xml-ui and cbmc --json-ui will output xml and json instead. cbmc-viewer can generally accept output in any form, but xml is strongly preferred.

The output of cbmc-viewer can be a summary of multiple invocations of cbmc. For example, after testing one function with cbmc in multiple configurations, invoking cbmc-viewer with the results of all of these tests in all of these configurations will generate a single report summarizing the union of these results.

--result FILE [FILE ...]

The property checking results. A text, xml, or json file containing the output of cbmc.

--coverage FILE [FILE ...]

The coverage checking results. An xml or json file containing the output of cbmc --cover locations.

--property FILE [FILE ...]

The properties checked during property checking. An xml or json file containing the output of cbmc --show-properties.

Source files

--srcdir SRCDIR

The root of the source tree. This is typically the root of the code repository itself. For best results, the source tree should include both the project code and the proof code written to facilitate verification (for example, stubs for functionality not being tested). The final report will not link to files outside the source tree or to symbols defined in files outside the source tree.

--exclude EXCLUDE

A regular expression for the paths relative to SRCDIR to exclude from the list of source files. This is rarely used. It is a Python regular expression matched against the result of os.path.normpath(). The match is case insensitive.

--extensions REGEXP

A regular expression for the file extensions of files to include in the list of source files. This is rarely used. It is a Python regular expression matched against the result of os.path.splitext(). The match is case insensitive. (Default: ^\.(c|h|inl)$)

--source-method MHD

The method to use to enumerate the list of source files. This is rarely used. The default method is generally to use the files mentioned in the symbol table of the goto binary. The full set of methods available is
- find: use the Linux find command in SRCDIR,
- walk: use the Python walk method in SRCDIR,
- make: use the make command in the WKDIR to build the goto binary with the preprocessor and use the files under SRCDIR mentioned in the preprocessor output, and
- goto: use the files under SRCDIR mentioned in the symbol table of the goto binary.
The default method is goto if SRCDIR and WKDIR and GOTO are specified, make if SRCDIR and WKDIR are specified, walk on Windows, and find otherwise.

Goto binaries

--wkdir WKDIR

The working directory. This is generally the directory in which goto-cc was invoked to build the goto binary. It is the working directory that is mentioned in the source locations in the goto binary. It is used to resolve relative paths appearing in source locations into absolute paths to source files. Relative paths appear in source locations only when goto-cc is invoked with relative paths. If goto-cc is invoked with absolute paths, paths in source locations are absolute paths, and this working directory is not needed.

--goto GOTO

The goto binary itself.

Viewer output

--reportdir REPORTDIR

The report directory. Write the final report to this directory. (Default: report)

--json-summary JSON

Write summary of key metrics to this json file.

Viewer input

JSON files produced by the various make-* scripts.

--viewer-coverage JSON [JSON ...]

Load coverage data from the JSON output of make-coverage. If multiple files are given, merge multiple data sets into one.

--viewer-loop JSON [JSON ...]

Load loops from the JSON output of make-loop. If multiple files are given, merge multiple data sets into one.

--viewer-property JSON [JSON ...]

Load properties from the JSON output of make-property. If multiple files are given, merge multiple data sets into one.

--viewer-reachable JSON [JSON ...]

Load reachable functions from the JSON output of make-reachable. If multiple files are given, merge multiple data sets into one.

--viewer-result JSON [JSON ...]

Load results from the JSON output of make-result. If multiple files are given, merge multiple data sets into one.

--viewer-source JSON [JSON ...]

Load sources from the JSON output of make-source. If multiple files are given, merge multiple data sets into one.

--viewer-symbol JSON [JSON ...]

Load symbols from the JSON output of make-symbol. If multiple files are given, merge multiple data sets into one.

--viewer-trace JSON [JSON ...]

Load traces from the JSON output of make-trace. If multiple files are given, merge multiple data sets into one.

Other

--help, -h

--verbose

Verbose output.

--debug

Debugging output.

--config JSON

JSON configuration file. (Default: cbmc-viewer.json)

--version

Display version number and exit.

Deprecated:

Options from prior versions now deprecated.

--block BLOCK

Use --coverage instead.

--htmldir HTMLDIR

Use --reportdir instead.

--srcexclude EXCLUDE

Use --exclude instead.

--blddir BLDDIR

Ignored.

--storm STORM

Ignored.

Reference manual

Name

cbmc-viewer coverage - Summarize coverage checking results

Synopsis

cbmc-viewer coverage [-h] [--coverage FILE [FILE ...]]
                          [--srcdir SRCDIR]
                          [--viewer-coverage JSON [JSON ...]] [--verbose]
                          [--debug] [--version]

Description

Summarize coverage checking results

Options

CBMC output

This is the output of CBMC that is summarized by cbmc-viewer. Output can be text, xml, or json, but xml is strongly preferred.

--coverage FILE [FILE ...]

CBMC coverage checking results. The output of "cbmc --cover locations".

Source files

--srcdir SRCDIR

The root of the source tree, typically the root of the code repository.

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

--viewer-coverage JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer coverage" giving CBMC coverage checking results.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

Reference manual

Name

cbmc-viewer loop - List loops found in the goto binary

Synopsis

cbmc-viewer loop [-h] [--srcdir SRCDIR] [--goto GOTO]
                      [--viewer-loop JSON [JSON ...]] [--verbose] [--debug]
                      [--version]

Description

List loops found in the goto binary

Options

Source files

--srcdir SRCDIR

The root of the source tree, typically the root of the code repository.

GOTO binaries

--goto GOTO

The goto binary itself.

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

`--viewer-loop JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer loop" listing the loops found in the goto binary.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

Reference manual

Name

cbmc-viewer property - List properties checked for during property checking

Synopsis

cbmc-viewer property [-h] [--property FILE [FILE ...]]
                          [--srcdir SRCDIR]
                          [--viewer-property JSON [JSON ...]] [--verbose]
                          [--debug] [--version]

Description

List properties checked for during property checking

Options

CBMC output

This is the output of CBMC that is summarized by cbmc-viewer. Output can be text, xml, or json, but xml is strongly preferred.

--property FILE [FILE ...]

CBMC properties checked during property checking. The output of "cbmc --show-properties".

Source files

--srcdir SRCDIR

The root of the source tree, typically the root of the code repository.

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

--viewer-property JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer property" listing the properties checked during CBMC property checking.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

Reference manual

Name

cbmc-viewer reachable - List reachable functions in the goto binary

Synopsis

cbmc-viewer reachable [-h] [--srcdir SRCDIR] [--goto GOTO]
                           [--viewer-reachable JSON [JSON ...]] [--verbose]
                           [--debug] [--version]

Description

List reachable functions in the goto binary

Options

Source files

--srcdir SRCDIR

The root of the source tree, typically the root of the code repository.

GOTO binaries

--goto GOTO

The goto binary itself.

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

--viewer-reachable JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer property" listing the reachable functions in the goto binary.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

Reference manual

Name

cbmc-viewer result - Summarize CBMC property checking results

Synopsis

cbmc-viewer result [-h] [--result FILE [FILE ...]]
                        [--viewer-result JSON [JSON ...]] [--verbose]
                        [--debug] [--version]

Description

Summarize CBMC property checking results

Options

CBMC output

This is the output of CBMC that is summarized by cbmc-viewer. Output can be text, xml, or json, but xml is strongly preferred.

--result FILE [FILE ...]

CBMC property checking the results. The output of "cbmc".

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

--viewer-result JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer result" giving the CBMC property checking results.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

Reference manual

Name

cbmc-viewer source - List source files used to build the goto binary

Synopsis

cbmc-viewer source [-h] [--srcdir SRCDIR] [--exclude EXCLUDE]
                        [--extensions REGEXP] [--source-method MHD]
                        [--wkdir WKDIR] [--goto GOTO]
                        [--viewer-source JSON [JSON ...]] [--verbose]
                        [--debug] [--version]

Description

List source files used to build the goto binary

Options

Source files

--srcdir SRCDIR

The root of the source tree, typically the root of the code repository.

--exclude EXCLUDE

A regular expression for the paths relative to SRCDIR to exclude from the list of source files. This is rarely used.

--extensions REGEXP

A regular expression for the file extensions of files to include in the list of source files. This is rarely used. (Default: ^.(c|h|inl)$)

--source-method MHD

The method to use to enumerate the list of source files. This is rarely used. The default method 'goto' is generally to use the files mentioned in the symbol table of the goto binary. The full set of methods available is
- 'find': use the Linux 'find' command in SRCDIR,
- 'walk': use the Python 'walk' method in SRCDIR,
- 'make': use the 'make' command in the WKDIR to build the goto binary with the preprocessor and use the files under SRCDIR mentioned in the preprocessor output, and
- 'goto': use the files under SRCDIR mentioned in the symbol table of the goto binary.

GOTO binaries

--wkdir WKDIR

The working directory. This is generally the directory in which goto-cc was invoked to build the goto binary. It is the working directory that is mentioned in the source locations in the goto binary.

--goto GOTO

The goto binary itself.

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

--viewer-source JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer source" listing the source files used to build the goto binary.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

Reference manual

Name

cbmc-viewer symbol - List symbols found in the goto binary

Synopsis

cbmc-viewer symbol [-h] [--srcdir SRCDIR] [--wkdir WKDIR] [--goto GOTO]
                        [--viewer-source JSON [JSON ...]]
                        [--viewer-symbol JSON [JSON ...]] [--verbose]
                        [--debug] [--version]

Description

List symbols found in the goto binary

Options

Source files

--srcdir SRCDIR

The root of the source tree, typically the root of the code repository.

GOTO binaries

--wkdir WKDIR

The working directory. This is generally the directory in which goto-cc was invoked to build the goto binary. It is the working directory that is mentioned in the source locations in the goto binary.

--goto GOTO

The goto binary itself.

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

--viewer-source JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer source" listing the source files used to build the goto binary.

--viewer-symbol JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer symbol" listing the symbols in the goto binary.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

Reference manual

Name

cbmc-viewer trace - List error traces generated for issues found during property checking

Synopsis

cbmc-viewer trace [-h] [--result FILE [FILE ...]] [--srcdir SRCDIR]
                       [--wkdir WKDIR] [--viewer-trace JSON [JSON ...]]
                       [--verbose] [--debug] [--version]

Description

List error traces generated for issues found during property checking

Options

CBMC output

This is the output of CBMC that is summarized by cbmc-viewer. Output can be text, xml, or json, but xml is strongly preferred.

--result FILE [FILE ...]

CBMC property checking the results. The output of "cbmc".

Source files

--srcdir SRCDIR

The root of the source tree, typically the root of the code repository.

GOTO binaries

--wkdir WKDIR

The working directory. This is generally the directory in which goto-cc was invoked to build the goto binary. It is the working directory that is mentioned in the source locations in the goto binary.

Viewer input

Load json output of cbmc-viewer like "viewer-coverage.json" or the output of cbmc-viewer subcommands like "cbmc-viewer coverage".

--viewer-trace JSON [JSON ...]

Load the output of "cbmc-viewer" or "cbmc-viewer trace" giving the error traces generated by CBMC for the issues found during property checking.

Other

--help

--verbose

Verbose output.

--debug

Debugging output.

--version

Display version number and exit.

CBMC viewer resources

CBMC viewer GitHub repository
CBMC GitHub repository

Contributing

This material is a work in progress. If you have suggestions, corrections, or questions, contact us by submitting a GitHub issue. If you have some examples of your own that you would like to contribute, submit your contributions as a GitHub pull request.