cbmc.1

.TH CBMC "1" "June 2022" "cbmc-5.59.0" "User Commands"
.SH NAME
cbmc \- Bounded Model Checker for C/C++ and Java programs
.SH SYNOPSIS
.B cbmc [--property \fIproperty-id\fB] \fIfile.c\fB ...

.B cbmc [--show-properties] \fIfile.c\fB ...

.B cbmc [--all-properties] \fIfile.c\fB ...

.B cbmc [--no-standard-checks] \fIfile.c\fB ...

.B cbmc [--no-standard-checks] [--pointer-check] \fIfile.c\fB ...

.B cbmc [--no-bounds-check] \fIfile.c\fB ...

.B goto-cc [-I \fIinclude-path\fB] [-c] \fIfile.c\fB [-o \fIoutfile.o\fB]

.B goto-instrument \fIinfile\fB \fIoutfile\fR

.PP
Only the most useful options are listed here; see below for the remainder.
.SH DESCRIPTION
\fBcbmc\fR 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.

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

\fBgoto-instrument\fR(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.
.SH OPTIONS
.SS "Standard Checks"
From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
apply some checks to the program by default (called the "standard checks"), with the
aim to provide a better user experience for a non-expert user of the tool. These checks are:
.TP
\fB\-\-pointer\-check\fR
enable pointer checks
.TP
\fB\-\-bounds\-check\fR
enable array bounds checks
.TP
\fB\-\-undefined\-shift\-check\fR
check shift greater than bit\-width
.TP
\fB\-\-div\-by\-zero\-check\fR
enable division by zero checks
.TP
\fB\-\-pointer\-primitive\-check\fR
checks that all pointers in pointer primitives are valid or null
.TP
\fB\-\-signed\-overflow\-check\fR
enable signed arithmetic over\- and underflow checks
.TP
\fB\-\-malloc\-may\-fail\fR
allow malloc calls to return a null pointer
.TP
\fB\-\-malloc\-fail\-null\fR
set malloc failure mode to return null
.TP
\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
generate unwinding assertions (cannot be
used with \fB\-\-cover\fR)
.PP
These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag
like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like
so:
.TP
\fB\-\-no\-pointer\-check\fR
disable pointer checks
.TP
\fB\-\-no\-bounds\-check\fR
disable array bounds checks
.TP
\fB\-\-no\-undefined\-shift\-check\fR
do not perform check for shift greater than bit\-width
.TP
\fB\-\-no\-div\-by\-zero\-check\fR
disable division by zero checks
.TP
\fB\-\-no\-pointer\-primitive\-check\fR
do not check that all pointers in pointer primitives are valid or null
.TP
\fB\-\-no\-signed\-overflow\-check\fR
disable signed arithmetic over\- and underflow checks
.TP
\fB\-\-no\-malloc\-may\-fail\fR
do not allow malloc calls to fail by default
.TP
\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
do not generate unwinding assertions (cannot be
used with \fB\-\-cover\fR)
.PP
If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
when default checks are already on, the flag is simply ignored.
.SS "Analysis options:"
.TP
\fB\-\-no\-standard\-checks\fR
disable the standard (default) checks applied to a C/GOTO program
(see above for more information)
.TP
\fB\-\-show\-properties\fR
show the properties, but don't run analysis
.TP
\fB\-\-symex\-coverage\-report\fR f
generate a Cobertura XML coverage report in f
.TP
\fB\-\-property\fR id
only check one specific property
.TP
\fB\-\-trace\fR
give a counterexample trace for failed properties
.TP
\fB\-\-stop\-on\-fail\fR
stop analysis once a failed property is detected
(implies \fB\-\-trace\fR)
.TP
\fB\-\-localize\-faults\fR
localize faults (experimental)
.SS "C/C++ frontend options:"
.TP
\fB\-\-preprocess\fR
stop after preprocessing
.TP
\fB\-\-test\-preprocessor\fR
stop after preprocessing, discard output
.TP
\fB\-I\fR path
set include path (C/C++)
.TP
\fB\-\-include\fR file
set include file (C/C++)
.TP
\fB\-D\fR macro
define preprocessor macro (C/C++)
.TP
\fB\-\-c89\fR, \fB\-\-c99\fR, \fB\-\-c11\fR
set C language standard (default: c11)
.TP
\fB\-\-cpp98\fR, \fB\-\-cpp03\fR, \fB\-\-cpp11\fR
set C++ language standard (default: cpp98)
.TP
\fB\-\-unsigned\-char\fR
make "char" unsigned by default
.TP
\fB\-\-round\-to\-nearest\fR, \fB\-\-round\-to\-even\fR
rounding towards nearest even (default)
.TP
\fB\-\-round\-to\-plus\-inf\fR
rounding towards plus infinity
.TP
\fB\-\-round\-to\-minus\-inf\fR
rounding towards minus infinity
.TP
\fB\-\-round\-to\-zero\fR
rounding towards zero
.TP
\fB\-\-no\-library\fR
disable built\-in abstract C library
.TP
\fB\-\-max\-nondet\-tree\-depth\fR N
limit size of nondet (e.g. input) object tree;
at level N pointers are set to null
.TP
\fB\-\-min\-null\-tree\-depth\fR N
minimum level at which a pointer can first be
NULL in a recursively nondet initialized struct
.TP
\fB\-\-function\fR name
set main function name
.SS "Platform options:"
.TP
\fB\-\-arch\fR \fIarch\fR
Set analysis architecture, which defaults to the host architecture. Use one of:
\fBalpha\fR, \fBarm\fR, \fBarm64\fR, \fBarmel\fR, \fBarmhf\fR, \fBhppa\fR, \fBi386\fR, \fBia64\fR,
\fBmips\fR, \fBmips64\fR, \fBmips64el\fR, \fBmipsel\fR, \fBmipsn32\fR,
\fBmipsn32el\fR, \fBpowerpc\fR, \fBppc64\fR, \fBppc64le\fR, \fBriscv64\fR, \fBs390\fR,
\fBs390x\fR, \fBsh4\fR, \fBsparc\fR, \fBsparc64\fR, \fBv850\fR, \fBx32\fR, \fBx86_64\fR, or
\fBnone\fR.
.TP
\fB\-\-os\fR \fIos\fR
Set analysis operating system, which defaults to the host operating system. Use
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
\fBwindows\fR.
.TP
\fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
Set analysis architecture and operating system.
.TP
\fB\-\-LP64\fR, \fB\-\-ILP64\fR, \fB\-\-LLP64\fR, \fB\-\-ILP32\fR, \fB\-\-LP32\fR
Set width of int, long and pointers, but don't override default architecture and
operating system.
.TP
\fB\-\-16\fR, \fB\-\-32\fR, \fB\-\-64\fR
Equivalent to \fB\-\-LP32\fR, \fB\-\-ILP32\fR, \fB\-\-LP64\fR (on Windows:
\fB\-\-LLP64\fR).
.TP
\fB\-\-little\-endian\fR
allow little\-endian word\-byte conversions
.TP
\fB\-\-big\-endian\fR
allow big\-endian word\-byte conversions
.TP
\fB\-\-gcc\fR
use GCC as preprocessor
.SS "Program representations:"
.TP
\fB\-\-show\-parse\-tree\fR
show parse tree
.TP
\fB\-\-show\-symbol\-table\fR
show loaded symbol table
.TP
\fB\-\-show\-goto\-functions\fR
show loaded goto program
.TP
\fB\-\-list\-goto\-functions\fR
list loaded goto functions
.TP
\fB\-\-validate\-goto\-model\fR
enable additional well\-formedness checks on the
goto program
.TP
\fB\-\-validate\-ssa\-equation\fR
enable additional well\-formedness checks on the
SSA representation
.SS "Program instrumentation options:"
.TP
\fB\-\-bounds\-check\fR
enable array bounds checks
.TP
\fB\-\-pointer\-check\fR
enable pointer checks
.TP
\fB\-\-memory\-leak\-check\fR
enable memory leak checks
.TP
\fB\-\-memory\-cleanup\-check\fR
Enable memory cleanup checks: assert that all dynamically allocated memory is
explicitly freed before terminating the program.
.TP
\fB\-\-div\-by\-zero\-check\fR
enable division by zero checks
.TP
\fB\-\-signed\-overflow\-check\fR
enable signed arithmetic over\- and underflow checks
.TP
\fB\-\-unsigned\-overflow\-check\fR
enable arithmetic over\- and underflow checks
.TP
\fB\-\-pointer\-overflow\-check\fR
enable pointer arithmetic over\- and underflow checks
.TP
\fB\-\-conversion\-check\fR
check whether values can be represented after type cast
.TP
\fB\-\-undefined\-shift\-check\fR
check shift greater than bit\-width
.TP
\fB\-\-float\-overflow\-check\fR
check floating\-point for +/\-Inf
.TP
\fB\-\-nan\-check\fR
check floating\-point for NaN
.TP
\fB\-\-enum\-range\-check\fR
checks that all enum type expressions have values in the enum range
.TP
\fB\-\-pointer\-primitive\-check\fR
checks that all pointers in pointer primitives are valid or null
.TP
\fB\-\-retain\-trivial\-checks\fR
include checks that are trivially true
.TP
\fB\-\-error\-label\fR label
check that label is unreachable
.TP
\fB\-\-no\-built\-in\-assertions\fR
ignore assertions in built\-in library
.TP
\fB\-\-no\-assertions\fR
ignore user assertions
.TP
\fB\-\-no\-assumptions\fR
ignore user assumptions
.TP
\fB\-\-assert\-to\-assume\fR
convert user assertions to assumptions
.TP
\fB\-\-cover\fR 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
.TP
\fB\-\-cover\-failed\-assertions\fR
do not stop coverage checking at failed assertions
(this is the default for \fB\-\-cover\fR assertions)
.TP
\fB\-\-show\-test\-suite\fR
print test suite for coverage criterion (requires \fB\-\-cover\fR)
.TP
\fB\-\-mm\fR MM
memory consistency model for concurrent programs (default: sc)
.TP
\fB\-\-malloc\-may\-fail\fR
allow malloc calls to return a null pointer
.TP
\fB\-\-malloc\-fail\-assert\fR
set malloc failure mode to assert\-then\-assume
.TP
\fB\-\-malloc\-fail\-null\fR
set malloc failure mode to return null
.TP
\fB\-\-string\-abstraction\fR
track C string lengths and zero\-termination
.TP
\fB\-\-reachability\-slice\fR
remove instructions that cannot appear on a trace
from entry point to a property
.TP
\fB\-\-reachability\-slice\-fb\fR
remove instructions that cannot appear on a trace
from entry point through a property
.TP
\fB\-\-full\-slice\fR
run full slicer (experimental)
.TP
\fB\-\-drop\-unused\-functions\fR
drop functions trivially unreachable from main function
.TP
\fB\-\-havoc\-undefined\-functions\fR
for any function that has no body, assign non\-deterministic values to
any parameters passed as non\-const pointers and the return value
.SS "Semantic transformations:"
.TP
\fB\-\-nondet\-static\fR
add nondeterministic initialization of variables with static lifetime
.SS "BMC options:"
.TP
\fB\-\-paths\fR [strategy]
explore paths one at a time
.TP
\fB\-\-show\-symex\-strategies\fR
list strategies for use with \fB\-\-paths\fR
.TP
\fB\-\-show\-goto\-symex\-steps\fR
show which steps symex travels, includes
diagnostic information
.TP
\fB\-\-show\-points\-to\-sets\fR
show points\-to sets for
pointer dereference. Requires \fB\-\-json\-ui\fR.
.TP
\fB\-\-program\-only\fR
only show program expression
.TP
\fB\-\-show\-byte\-ops\fR
show all byte extracts and updates
.TP
\fB\-\-depth\fR nr
limit search depth
.TP
\fB\-\-max\-field\-sensitivity\-array\-size\fR M
maximum size M of arrays for which field
sensitivity will be applied to array,
the default is 64
.TP
\fB\-\-no\-array\-field\-sensitivity\fR
deactivate field sensitivity for arrays, this is
equivalent to setting the maximum field
sensitivity size for arrays to 0
.TP
\fB\-\-show\-loops\fR
show the loops in the program
.TP
\fB\-\-unwind\fR nr
unwind nr times
.TP
\fB\-\-unwindset\fR [T:]L:B,...
unwind loop L with a bound of B
(optionally restricted to thread T)
(use \fB\-\-show\-loops\fR to get the loop IDs)
.TP
\fB\-\-incremental\-loop\fR L
check properties after each unwinding
of loop L
(use \fB\-\-show\-loops\fR to get the loop IDs)
.TP
\fB\-\-unwind\-min\fR 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.
.TP
\fB\-\-unwind\-max\fR nr
stop incremental\-loop after nr unwindings
.TP
\fB\-\-ignore\-properties\-before\-unwind\-min\fR
do not check properties before unwind\-min
when using incremental\-loop
.TP
\fB\-\-show\-vcc\fR
show the verification conditions
.TP
\fB\-\-slice\-formula\fR
remove assignments unrelated to property
.TP
\fB\-\-unwinding\-assertions\fR
generate unwinding assertions (cannot be
used with \fB\-\-cover\fR)
.TP
\fB\-\-partial\-loops\fR
permit paths with partial loops
.TP
\fB\-\-no\-self\-loops\-to\-assumptions\fR
do not simplify while(1){} to assume(0)
.TP
\fB\-\-symex\-complexity\-limit\fR N
how complex (N) a path can become before
symex abandons it. Currently uses guard
size to calculate complexity.
.TP
\fB\-\-symex\-complexity\-failed\-child\-loops\-limit\fR N
how many child branches (N) in an
iteration are allowed to fail due to
complexity violations before the loop
gets blacklisted
.TP
\fB\-\-graphml\-witness\fR filename
write the witness in GraphML format to filename
.TP
\fB\-\-symex\-cache\-dereferences\fR
enable caching of repeated dereferences
.SS "Backend options:"
.TP
\fB\-\-object\-bits\fR n
number of bits used for object addresses
.TP
\fB\-\-sat\-solver\fR solver
use specified SAT solver
.TP
\fB\-\-external\-sat\-solver\fR cmd
command to invoke SAT solver process
.TP
\fB\-\-no\-sat\-preprocessor\fR
disable the SAT solver's simplifier
.TP
\fB\-\-dimacs\fR
generate CNF in DIMACS format
.TP
\fB\-\-beautify\fR
beautify the counterexample
(greedy heuristic)
.TP
\fB\-\-smt1\fR
use default SMT1 solver (obsolete)
.TP
\fB\-\-smt2\fR
use default SMT2 solver (Z3)
.TP
\fB\-\-bitwuzla\fR
use Bitwuzla
.TP
\fB\-\-boolector\fR
use Boolector
.TP
\fB\-\-cprover\-smt2\fR
use CPROVER SMT2 solver
.TP
\fB\-\-cvc3\fR
use CVC3
.TP
\fB\-\-cvc4\fR
use CVC4
.TP
\fB\-\-cvc5\fR
use CVC5
.TP
\fB\-\-mathsat\fR
use MathSAT
.TP
\fB\-\-yices\fR
use Yices
.TP
\fB\-\-z3\fR
use Z3
.TP
\fB\-\-fpa\fR
use theory of floating\-point arithmetic
.TP
\fB\-\-refine\fR
use refinement procedure (experimental)
.TP
\fB\-\-refine\-arrays\fR
use refinement for arrays only
.TP
\fB\-\-refine\-arithmetic\fR
refinement of arithmetic expressions only
.TP
\fB\-\-max\-node\-refinement\fR
maximum refinement iterations for
arithmetic expressions
.TP
\fB\-\-incremental\-smt2\-solver\fR \fIcmd\fR
Use the incremental SMT backend where \fIcmd\fR is the command to invoke the SMT
solver of choice.
.br
Example invocations:
.br
  --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
.br
  --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' (use the CVC5 solver).
.sp
Note that:
.br
The solver name must be in the "PATH" or be an executable with full path.
.br
The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
.br
The SMT solver should support the QF_AUFBV logic.
.TP
\fB\-\-outfile\fR filename
output formula to given file
.TP
\fB\-\-dump\-smt\-formula\fR filename
output smt incremental formula to the given file
.TP
\fB\-\-write\-solver\-stats\-to\fR json\-file
collect the solver query complexity
.TP
\fB\-\-refine\-strings\fR
use string refinement (experimental)
.TP
\fB\-\-string\-printable\fR
restrict to printable strings (experimental)
.TP
\fB\-\-arrays\-uf\-never\fR
never turn arrays into uninterpreted functions
.TP
\fB\-\-arrays\-uf\-always\fR
always turn arrays into uninterpreted functions
.TP
\fB\-\-show\-array\-constraints\fR
show array theory constraints added
during post processing.
Requires \fB\-\-json\-ui\fR.
.SS "User-interface options:"
.TP
\fB\-\-xml\-ui\fR
use XML\-formatted output
.TP
\fB\-\-xml\-interface\fR
bi\-directional XML interface
.TP
\fB\-\-json\-ui\fR
use JSON\-formatted output
.TP
\fB\-\-json\-interface\fR
bi\-directional JSON interface
.TP
\fB\-\-trace\-json\-extended\fR
add rawLhs property to trace
.TP
\fB\-\-trace\-show\-function\-calls\fR
show function calls in plain trace
.TP
\fB\-\-trace\-show\-code\fR
show original code in plain trace
.TP
\fB\-\-trace\-hex\fR
represent plain trace values in hex
.TP
\fB\-\-compact\-trace\fR
give a compact trace
.TP
\fB\-\-stack\-trace\fR
give a stack trace only
.TP
\fB\-\-flush\fR
flush every line of output
.TP
\fB\-\-export\-symex\-ready\-goto\fR filename
export the symex ready version of the goto-model into the given filename
.TP
\fB\-\-verbosity\fR #
verbosity level
.TP
\fB\-\-timestamp\fR [\fBmonotonic\fR|\fBwall\fR]
Print microsecond\-precision timestamps.  \fBmonotonic\fR: stamps increase
monotonically.  \fBwall\fR: ISO\-8601 wall clock timestamps.
.SH ENVIRONMENT
All tools honor the TMPDIR environment variable when generating temporary
files and directories. Furthermore note that
the preprocessor used by \fBcbmc\fR will use environment variables to locate
header files.
.SH BUGS
If you encounter a problem please create an issue at
.B https://github.com/diffblue/cbmc/issues
.SH SEE ALSO
.BR goto-cc (1),
.BR goto-instrument (1)
.SH COPYRIGHT
2001-2016, Daniel Kroening, Edmund Clarke