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.