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(1) 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(1) distinguishes between compiling and linking phases, just as gcc does. cbmc expects a GOTO binary for which linking has been completed.

goto-instrument(1) 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.


Analysis options


show the properties, but don't run analysis

--symex-coverage-report f

generate a Cobertura XML coverage report in f

--property id

only check one specific property


give a counterexample trace for failed properties


stop analysis once a failed property is detected (implies --trace)


localize faults (experimental)

C/C++ frontend options


stop after preprocessing


stop after preprocessing, discard output

-I path

set include path (C/C++)

--include file

set include file (C/C++)

-D macro

define preprocessor macro (C/C++)

--c89,  --c99,  --c11

set C language standard (default: c11)

--cpp98,  --cpp03,  --cpp11

set C++ language standard (default: cpp98)


make "char" unsigned by default

--round-to-nearest,  --round-to-even

rounding towards nearest even (default)


rounding towards plus infinity


rounding towards minus infinity


rounding towards zero


disable built-in abstract C library

--max-nondet-tree-depth N

limit size of nondet (e.g. input) object tree; at level N pointers are set to null

--min-null-tree-depth N

minimum level at which a pointer can first be NULL in a recursively nondet initialized struct

--function name

set main function name

Platform options

--arch arch

Set analysis architecture, which defaults to the host architecture. Use one of: alpha, arm, arm64, armel, armhf, hppa, i386, ia64, mips, mips64, mips64el, mipsel, mipsn32, mipsn32el, powerpc, ppc64, ppc64le, riscv64, s390, s390x, sh4, sparc, sparc64, v850, x32, x86_64, or none.

--os os

Set analysis operating system, which defaults to the host operating system. Use one of: freebsd, linux, macos, solaris, or windows.

--i386-linux,  --i386-win32,  --i386-macos,  --ppc-macos,  --win32,  --winx64

Set analysis architecture and operating system.

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

Set width of int, long and pointers, but don't override default architecture and operating system.

--16,  --32,  --64

Equivalent to --LP32, --ILP32, --LP64 (on Windows: --LLP64).


allow little-endian word-byte conversions


allow big-endian word-byte conversions


use GCC as preprocessor

Program representations


show parse tree


show loaded symbol table


show loaded goto program


list loaded goto functions


enable additional well-formedness checks on the goto program


enable additional well-formedness checks on the SSA representation

Program instrumentation options


enable array bounds checks


enable pointer checks


enable memory leak checks


Enable memory cleanup checks: assert that all dynamically allocated memory is explicitly freed before terminating the program.


enable division by zero checks


enable signed arithmetic over- and underflow checks


enable arithmetic over- and underflow checks


enable pointer arithmetic over- and underflow checks


check whether values can be represented after type cast


check shift greater than bit-width


check floating-point for +/-Inf


check floating-point for NaN


checks that all enum type expressions have values in the enum range


checks that all pointers in pointer primitives are valid or null


include checks that are trivially true

--error-label label

check that label is unreachable


ignore assertions in built-in library


ignore user assertions


ignore user assumptions


convert user assertions to assumptions

--cover CC

create test-suite with coverage criterion CC, where CC is one of assertion[s], assume[s], branch[es], condition[s], cover, decision[s], location[s], or mcdc


do not stop coverage checking at failed assertions (this is the default for --cover assertions)


print test suite for coverage criterion (requires --cover)

--mm MM

memory consistency model for concurrent programs (default: sc)


allow malloc calls to return a null pointer


set malloc failure mode to assert-then-assume


set malloc failure mode to return null


track C string lengths and zero-termination


remove instructions that cannot appear on a trace from entry point to a property


remove instructions that cannot appear on a trace from entry point through a property


run full slicer (experimental)


drop functions trivially unreachable from main function


for any function that has no body, assign non-deterministic values to any parameters passed as non-const pointers and the return value

Semantic transformations


add nondeterministic initialization of variables with static lifetime

BMC options

--paths [strategy]

explore paths one at a time


list strategies for use with --paths


show which steps symex travels, includes diagnostic information


show points-to sets for pointer dereference. Requires --json-ui.


only show program expression


show all byte extracts and updates

--depth nr

limit search depth

--max-field-sensitivity-array-size M

maximum size M of arrays for which field sensitivity will be applied to array, the default is 64


deactivate field sensitivity for arrays, this is equivalent to setting the maximum field sensitivity size for arrays to 0


show the loops in the program

--unwind nr

unwind 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)

--incremental-loop L

check properties after each unwinding of loop L (use --show-loops to get the loop IDs)

--unwind-min nr

start incremental-loop after nr unwindings but before solving that iteration. If for example it is 1, then the loop will be unwound once, and immediately checked. Note: this means for min-unwind 1 or 0 all properties are checked.

--unwind-max nr

stop incremental-loop after nr unwindings


do not check properties before unwind-min when using incremental-loop


show the verification conditions


remove assignments unrelated to property


generate unwinding assertions (cannot be used with --cover)


permit paths with partial loops


do not simplify while(1){} to assume(0)

--symex-complexity-limit N

how complex (N) a path can become before symex abandons it. Currently uses guard size to calculate complexity.

--symex-complexity-failed-child-loops-limit N

how many child branches (N) in an iteration are allowed to fail due to complexity violations before the loop gets blacklisted

--graphml-witness filename

write the witness in GraphML format to filename


enable caching of repeated dereferences

Backend options

--object-bits n

number of bits used for object addresses

--sat-solver solver

use specified SAT solver

--external-sat-solver cmd

command to invoke SAT solver process


disable the SAT solver's simplifier


generate CNF in DIMACS format


beautify the counterexample (greedy heuristic)


use default SMT1 solver (obsolete)


use default SMT2 solver (Z3)


use Bitwuzla


use Boolector


use CPROVER SMT2 solver


use CVC3


use CVC4


use CVC5


use MathSAT


use Yices


use Z3


use theory of floating-point arithmetic


use refinement procedure (experimental)


use refinement for arrays only


refinement of arithmetic expressions only


maximum refinement iterations for arithmetic expressions

--incremental-smt2-solver cmd

Use the incremental SMT backend where cmd is the command to invoke the SMT solver of choice.
Example invocations:
 --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
 --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' (use the CVC5 solver).

Note that:
The solver name must be in the "PATH" or be an executable with full path.
The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
The SMT solver should support the QF_AUFBV logic.

--outfile filename

output formula to given file

--dump-smt-formula filename

output smt incremental formula to the given file

--write-solver-stats-to json-file

collect the solver query complexity


use string refinement (experimental)


restrict to printable strings (experimental)


never turn arrays into uninterpreted functions


always turn arrays into uninterpreted functions


show array theory constraints added during post processing. Requires --json-ui.

User-interface options


use XML-formatted output


bi-directional XML interface


use JSON-formatted output


bi-directional JSON interface


add rawLhs property to trace


show function calls in plain trace


show original code in plain trace


represent plain trace values in hex


give a compact trace


give a stack trace only


flush every line of output

--export-symex-ready-goto filename

export the symex ready version of the goto-model into the given filename

--verbosity #

verbosity level

--timestamp [monotonic|wall]

Print microsecond-precision timestamps.  monotonic: stamps increase monotonically.  wall: ISO-8601 wall clock timestamps.


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.


If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues

See Also

goto-cc(1), goto-instrument(1)

Referenced By

goto-analyzer(1), goto-cc(1), goto-diff(1), goto-harness(1), goto-instrument(1), goto-synthesizer(1), memory-analyzer(1), symtab2gb(1).

June 2022 cbmc-5.59.0