cbmc - Man Page

Bounded Model Checker for C/C++ and Java programs


cbmc [--property property-id] file.c ...

cbmc [--show-properties] file.c ...

cbmc [--all-properties] file.c ...

goto-cc [-I include-path] [-c] file.c [-o outfile.o]

goto-instrument infile outfile

Only the most useful options are listed here; see below for the remainder.


cbmc generates traces that demonstrate how an assertion can be violated, or proves that the assertion cannot be violated within a given number of loop iterations.  CBMC can read C/C++ source-code directly, or a goto-binary generated by goto-cc.  Java programs are given as class or JAR files.  Without any further options, cbmc checks all properties (automatically generated or user-specified) found in the program.  If any of the properties can be violated, a counterexample is printed and the analysis is aborted.  The analysis can be restricted to a particular property with the --property option.  The verification result for all properties can be obtained by means of the --all-properties option.

goto-cc reads source code, and generates a goto-binary. Its command-line interface is designed to mimic that of gcc(1). Note in particular that goto-cc distinguishes between compiling and linking phases, just as gcc does. cbmc expects a goto-binary for which linking has been completed.

goto-instrument reads a goto-binary, performs a given program transformation, and then writes the resulting program as goto-binary on disc.

The usual flow is to (1) translate source into a goto-binary using goto-cc, then (2) perform instrumentation with goto-instrument, and finally (3) perform the analysis with cbmc.


FRONTEND OPTIONS (cbmc and goto-cc)

-I path

Set include path (C/C++)

-D macro

Define preprocessor macro (C/C++)


Stop after preprocessing


Show symbol table


Show goto program

ARCHITECTURAL OPTIONS (cbmc and goto-cc)

cbmc by default uses architectural settings that match those of the machine cbmc is executed on, i.e., the settings below are only needed when verifying software that is meant to run on a different architecture or OS. goto-cc generates a goto-binary for a particular architecture, i.e., the architecture cannot be changed after the goto-binary is generated.

--16,  --32,  --64

Set width of int

--LP64,  --ILP64,  --LLP64,  --ILP32,  --LP32

Set width of int, long and pointers


Allow little-endian word-byte conversions


Allow big-endian word-byte conversions


Make "char" unsigned by default


Set target architecture


Set target operating system


Don't set up an architecture


Disable built-in abstract C library

--round-to-nearest,  --round-to-plus-inf,  --round-to-minus-inf,  --round-to-zero

IEEE floating point rounding mode to use when the program begins (default is round to nearest). The program under verification can override this setting, e.g., with fesetround(3).

PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)

Both cbmc and goto-instrument can generate assertions that catch specific common errors, as listed below.


Enable array bounds checks


Enable division by zero checks


Enable pointer checks


Enable arithmetic over- and underflow checks for signed integer arithmetic


Enable arithmetic over- and underflow checks for unsigned integer arithmetic


Check floating-point computations for NaN


Ignore user-provided assertions


Ignore user-provided assumptions

--error-label label

Check that the given label is unreachable


goto-instrument supports further, more complex, program transformations.


Makes reads from volatile variables non-deterministic

--isr function

Instruments an interrupt service routine with the given name


Instruments memory-mapped I/O


Variables with static lifetime are initialized non-deterministically


Output ANSI-C source code instead of a goto binary.



Report status of all properties


Only show properties


Show the loops in the program


Check which assertions are reachable

--function name

Set main function name

--property id

Only check specific property with given identifier


Only show program expression

--depth nr

Limit search depth

--unwind nr

Unwind loops nr times

--unwindset [T:]L:B,...

Unwind loop L with a bound of B, optionally restricted to thread T. Use --show-loops to get the loop IDs. Thread numbers are set as follows: The initial thread has index 0, and threads are consecutively numbered in program order of threads being spawned.  The`--unwindset` option can be given multiple times.


Show the verification conditions


Remove assignments unrelated to property


Do not generate unwinding assertions


Do not simplify identifiers



Generate CNF in DIMACS format for use by external SAT solvers


Beautify the counterexample (greedy heuristic)


Output subgoals in SMT2 syntax


Use Boolector (experimental)


Use MathSAT (experimental)


Use CVC3 (experimental)


Use CVC4 (experimental)


Use Yices (experimental)


Use Z3 (experimental)


Use refinement procedure (experimental)

--outfile filename

Output formula to given file


Never turn arrays into uninterpreted functions


Always turn arrays into uninterpreted functions


All tools honor the TMPDIR environment variable when generating temporary files and directories. Furthermore note that the preprocessor used by CBMC will use environment variables to locate header files. GOTO-CC aims to accept all environment variables that GCC does.

Referenced By

The man pages goto-analyzer(1), goto-cc(1), goto-diff(1), goto-gcc(1), goto-harness(1), goto-instrument(1) and goto-ld(1) are aliases of cbmc(1).

JUNE 2014 cbmc-4.7 User Manual