Standard Checks¶

From version 6.0 onwards, cbmc, goto-analyzer 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:

--pointer-check

enable pointer checks

--bounds-check

enable array bounds checks

--undefined-shift-check

check shift greater than bit-width

--div-by-zero-check

enable division by zero checks for integer division

--float-div-by-zero-check

enable division by zero checks for floating-point division

--pointer-primitive-check

checks that all pointers in pointer primitives are valid or null

--signed-overflow-check

enable signed arithmetic over- and underflow checks

--malloc-may-fail

allow malloc calls to return a null pointer

--malloc-fail-null

set malloc failure mode to return null

--unwinding-assertions

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

These checks can all be deactivated at once by using the --no-standard-checks flag like in the header example, or individually, by prepending a no- before the flag, like so:

--no-pointer-check

disable pointer checks

--no-bounds-check

disable array bounds checks

--no-undefined-shift-check

do not perform check for shift greater than bit-width

--no-div-by-zero-check

disable division by zero checks

--no-pointer-primitive-check

do not check that all pointers in pointer primitives are valid or null

--no-signed-overflow-check

disable signed arithmetic over- and underflow checks

--no-malloc-may-fail

do not allow malloc calls to fail by default

--no-unwinding-assertions

do not generate unwinding assertions

If an already set flag is re-set, like calling --pointer-check when default checks are already on, the flag is simply ignored.

Analysis options:¶

--no-standard-checks

disable the standard (default) checks applied to a C/GOTO program (see above for more information)

--show-properties

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

--trace

give a counterexample trace for failed properties

--stop-on-fail

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

--localize-faults

localize faults (experimental)

C/C++ frontend options:¶

--preprocess

stop after preprocessing

--test-preprocessor

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)

--unsigned-char

make "char" unsigned by default

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

rounding towards nearest even (default)

--round-to-plus-inf

rounding towards plus infinity

--round-to-minus-inf

rounding towards minus infinity

--round-to-zero

rounding towards zero

--no-library

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, netbsd, openbsd, solaris, hurd, 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).

--little-endian

allow little-endian word-byte conversions

--big-endian

allow big-endian word-byte conversions

--gcc

use GCC as preprocessor

Program representations:¶

--show-parse-tree

show parse tree

--show-symbol-table

show loaded symbol table

--show-goto-functions

show loaded goto program

--list-goto-functions

list loaded goto functions

--validate-goto-model

enable additional well-formedness checks on the goto program

--validate-ssa-equation

enable additional well-formedness checks on the SSA representation

Program instrumentation options:¶

--bounds-check

enable array bounds checks

--pointer-check

enable pointer checks

--memory-leak-check

enable memory leak checks

--memory-cleanup-check

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

--div-by-zero-check

enable division by zero checks

--signed-overflow-check

enable signed arithmetic over- and underflow checks

--unsigned-overflow-check

enable arithmetic over- and underflow checks

--pointer-overflow-check

enable pointer arithmetic over- and underflow checks

--conversion-check

check whether values can be represented after type cast

--undefined-shift-check

check shift greater than bit-width

--float-overflow-check

check floating-point for +/-Inf

--nan-check

check floating-point for NaN

--enum-range-check

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

--pointer-primitive-check

checks that all pointers in pointer primitives are valid or null

--retain-trivial-checks

include checks that are trivially true

--error-label label

check that label is unreachable

--no-built-in-assertions

ignore assertions in built-in library

--no-assertions

ignore user assertions

--no-assumptions

ignore user assumptions

--assert-to-assume

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

--cover-failed-assertions

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

--show-test-suite

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

--mm MM

memory consistency model for concurrent programs (default: sc)

--malloc-may-fail

allow malloc calls to return a null pointer

--malloc-fail-assert

set malloc failure mode to assert-then-assume

--malloc-fail-null

set malloc failure mode to return null

--string-abstraction

track C string lengths and zero-termination

--reachability-slice

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

--reachability-slice-fb

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

--full-slice

run full slicer (experimental)

--drop-unused-functions

drop functions trivially unreachable from main function

Semantic transformations:¶

--nondet-static

add nondeterministic initialization of variables with static lifetime

BMC options:¶

--paths [strategy]

explore paths one at a time

--show-symex-strategies

list strategies for use with --paths

--show-goto-symex-steps

show which steps symex travels, includes diagnostic information

--show-points-to-sets

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

--program-only

only show program expression

--show-byte-ops

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

--no-array-field-sensitivity

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

--show-loops

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

--ignore-properties-before-unwind-min

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

--show-vcc

show the verification conditions

--slice-formula

remove assignments unrelated to property

--unwinding-assertions

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

--partial-loops

permit paths with partial loops

--no-self-loops-to-assumptions

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

--symex-cache-dereferences

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

--no-sat-preprocessor

disable the SAT solver's simplifier

--dimacs

generate CNF in DIMACS format

--beautify

beautify the counterexample (greedy heuristic)

--smt1

use default SMT1 solver (obsolete)

--smt2

use default SMT2 solver (Z3)

--bitwuzla

use Bitwuzla

--boolector

use Boolector

--cprover-smt2

use CPROVER SMT2 solver

--cvc3

use CVC3

--cvc4

use CVC4

--cvc5

use CVC5

--mathsat

use MathSAT

--yices

use Yices

--z3

use Z3

--fpa

use theory of floating-point arithmetic

--refine

use refinement procedure (experimental)

--refine-arrays

use refinement for arrays only

--refine-arithmetic

refinement of arithmetic expressions only

--max-node-refinement

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

--refine-strings

use string refinement (experimental)

--string-printable

restrict to printable strings (experimental)

--arrays-uf-never

never turn arrays into uninterpreted functions

--arrays-uf-always

always turn arrays into uninterpreted functions

--show-array-constraints

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

User-interface options:¶

--xml-ui

use XML-formatted output

--xml-interface

bi-directional XML interface

--json-ui

use JSON-formatted output

--json-interface

bi-directional JSON interface

--trace-json-extended

add rawLhs property to trace

--trace-show-function-calls

show function calls in plain trace

--trace-show-code

show original code in plain trace

--trace-hex

represent plain trace values in hex

--compact-trace

give a compact trace

--stack-trace

give a stack trace only

--flush

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.