CBMC(1) User Commands CBMC(1)

cbmc - 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.

show the properties, but don't run analysis
generate a Cobertura XML coverage report in f
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)

stop after preprocessing
stop after preprocessing, discard output
set include path (C/C++)
set include file (C/C++)
define preprocessor macro (C/C++)
set C language standard (default: c11)
set C++ language standard (default: cpp98)
make "char" unsigned by default
rounding towards nearest even (default)
rounding towards plus infinity
rounding towards minus infinity
rounding towards zero
disable built-in abstract C library
limit size of nondet (e.g. input) object tree; at level N pointers are set to null
minimum level at which a pointer can first be NULL in a recursively nondet initialized struct
set main function name

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.
Set analysis operating system, which defaults to the host operating system. Use one of: freebsd, linux, macos, solaris, or windows.
Set analysis architecture and operating system.
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

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

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
check that label is unreachable
ignore assertions in built-in library
ignore user assertions
ignore user assumptions
convert user assertions to assumptions
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)
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

add nondeterministic initialization of variables with static lifetime

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
limit search depth
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 times
unwind loop L with a bound of B (optionally restricted to thread T) (use --show-loops to get the loop IDs)
check properties after each unwinding of loop L (use --show-loops to get the loop IDs)
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.
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)
how complex (N) a path can become before symex abandons it. Currently uses guard size to calculate complexity.
how many child branches (N) in an iteration are allowed to fail due to complexity violations before the loop gets blacklisted
write the witness in GraphML format to filename
enable caching of repeated dereferences

number of bits used for object addresses
use specified SAT solver
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
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.

output formula to given file
output smt incremental formula to the given 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.

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 the symex ready version of the goto-model into the given filename
verbosity level
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

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

2001-2016, Daniel Kroening, Edmund Clarke

June 2022 cbmc-5.59.0