This document provides a brief overview of the various tools in the CProver project. The goal is as to provide a lightweight reference with links to detailed documentation on each of the tools.
The tools in the CProver project are as follows:
- cbmc
- goto-analyzer
- goto-cc (goto-gcc, goto-ld)
- goto-diff
- goto-harness
- goto-instrument
- janalyzer
- jbmc
- jdiff
- memory-analyzer
- smt2_solver
- symtab2gb
- Developer Utilities
The rest of this document provides a section on each of these tools in alphabetical order. Most links in this document are to the CProver online documentation.
The C Bounded Model Checker (cbmc) is the main tool used in the CProver suite.
cbmc does the entire analysis from the source code through to the result,
including generating traces. This includes invoking various sub-tools and
modules.
For details on usage of the cbmc tool see the following documentation
- Developer Tutorial
includes a very brief tutorial on many aspects of
cbmcand other tools.
For details on the architecture of the cbmc tool and how the analysis is performed
see the following documents:
- CBMC Architecture
gives a high level overview of the
cbmcarchitecture and data flow. - Background Concepts
overviews all the key concepts used in the
cbmcanalysis.
For details on compiling, testing, contributing, and documentation related to development see:
The goto-analyzer is a wrapper program around the
abstract interpretation
implementations. (For more detail on these implementations see
here.)
It is possible to configure which abstractions are used and what
is done with the chosen abstractions (verification, display,
simplification, etc.). See the man
page for details.
This is a compiler designed to be able to be dropped in to an existing
build process to replace the existing compiler. goto-cc is able to do
normal compilation, but is designed to output goto programs (optionally
in addition to the normal compiled program). Note that goto-cc is both
the compiler and linker (goto-gcc and goto-ld are symbolic links to
goto-cc, where the file name is used to ensure the program behaves
according to the name, e.g. if called from goto-gcc then goto-cc
will behave like gcc). The additional object code is used as the internal
representation for cbmc and related tools. These can also be extracted and
used themselves.
Further information on goto-cc can be found at:
- Developer Tutorial with some very simple examples and notes.
- goto-cc information
on the
goto-cccompilers - goto Programs for information on goto programs and how they are used.
Note that goto-cc can emulate GCC, Visual Studio, and CodeWarrior
compilers.
Provides a variety of difference checks between two goto programs
produced by goto-cc (essentially a diff tool for goto programs).
This invokes some of the cbmc tools to convert the goto
program and then determine which functions are added/removed/changed.
Details of all the options can be seen by running
goto-diff --help
this includes both options for the difference, and options for the goto program instrumentation.
This is a tool for creating a harness around a (part of a) goto program that can then be analysed (using the harness). Harnesses can be either function call environments, or memory snapshots.
Documentation on goto-harness can be found
in it's man page
including details and examples.
This is a collection of tools for analysing and modifying goto programs (programs created with #goto-cc). Generally these take a goto program and output another goto program.
Further examples and documentation can be found at:
- goto-instrument
has an overview of
goto-instrumentand a small tutorial example. - Developer Tutorial has high
level overview and some example commands for
goto-instrument.
This provides a way to access and invoke various forms of analysis on Java programs. This is a fork of goto-analyzer with a Java Virtual Machine front end.
Documentation useful for this tool can be found:
Details of all the options can be seen by running
janalyzer --help
This is the main analysis engine the performs the analysis
of Java files using bounded model checking. This is a
version of the cbmc tool that checks Java programs
(more documentation for cbmc is available and much of
it applies to jbmc since they use many of the same back
end utilities).
Note that the jbmc tool follows java conventions so that
programs can be analyzed in the same way you would run them
using the java executable. There also many additional
options to support nondeterministic initialisation of variable
size arrays, data structures and strings, control how to assert
on exceptions etc.
For some light information on usage of the jbmc tool see the following documentation
- JBMC homepage includes some simple examples and information.
For details on how analysis is performed in the cbmc and
jbmc tools see see the following documents:
- CBMC Architecture
gives a high level overview of the
cbmcarchitecture and data flow that should also apply tojbmc. - Background Concepts
overviews all the key concepts used in the
jbmcanalysis.
For details on compiling, testing, contributing, and documentation related to development see:
Provides a variety of difference checks between two goto programs (produced
by goto-cc). This invokes some of the cbmc/jbmc tools to convert the goto
program and then determine which functions are added/removed/changed.
This is a clone of goto-diff for Java programs and is essentially
a diff for goto programs generated from Java code.
Details of all the options can be seen by running
jdiff --help
this includes both options for the difference, and options for the goto program instrumentation.
This is a wrapper program that provides a front end to gdb that adds some
useful features related to the other goto utilities. In particular
memory-analyzer can run a compiled binary using gdb and then (at the
right point) create a harness from the current program state for use with
goto-harness.
Note that to use memory-analyzer the program must be compiled with
goto-cc. To make best use of memory-analyzer and gdb you should
compile with the -g option.
For further documentation and examples see here.
This is an (Satisfiability Modulo Theories) SMT solver that parses SMT-LIB 2 format files and uses CProver's internal bit-blasting solver (see solvers) to resolve queries.
This utility is to compile a cbmc symbols table (in JSON format) into a goto binary. This is to support integration of external language frontends (e.g. Ada using GNAT2GOTO). For usage run
symtab2gb --help
The utilities below are designed for developer use.
Runs Java unit tests. For more details use
java-unit --help
Default behaviour is to only show failed test cases.
Runs C unit tests. For more details use
unit --help
Default behaviour is to only show failed test cases.