cbmc - Man Page

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.

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.