FRONTEND OPTIONS (cbmc and goto-cc)

-I path

Set include path (C/C++)

-D macro

Define preprocessor macro (C/C++)

--preprocess

Stop after preprocessing

--show-symbol-table

Show symbol table

--show-goto-functions

Show goto program

ARCHITECTURAL OPTIONS (cbmc and goto-cc)

cbmc by default uses architectural settings that match those of the machine cbmc is executed on, i.e., the settings below are only needed when verifying software that is meant to run on a different architecture or OS. goto-cc generates a goto-binary for a particular architecture, i.e., the architecture cannot be changed after the goto-binary is generated.

--16, --32, --64

Set width of int

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

Set width of int, long and pointers

--little-endian

Allow little-endian word-byte conversions

--big-endian

Allow big-endian word-byte conversions

--unsigned-char

Make "char" unsigned by default

--arch

Set target architecture

--os

Set target operating system

--no-arch

Don't set up an architecture

--no-library

Disable built-in abstract C library

--round-to-nearest, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero

IEEE floating point rounding mode to use when the program begins (default is round to nearest). The program under verification can override this setting, e.g., with fesetround(3).

PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)

Both cbmc and goto-instrument can generate assertions that catch specific common errors, as listed below.

--bounds-check

Enable array bounds checks

--div-by-zero-check

Enable division by zero checks

--pointer-check

Enable pointer checks

--signed-overflow-check

Enable arithmetic over- and underflow checks for signed integer arithmetic

--unsigned-overflow-check

Enable arithmetic over- and underflow checks for unsigned integer arithmetic

--nan-check

Check floating-point computations for NaN

--no-assertions

Ignore user-provided assertions

--no-assumptions

Ignore user-provided assumptions

--error-label label

Check that the given label is unreachable

PROGRAM INSTRUMENTATION OPTIONS (goto-instrument only)

goto-instrument supports further, more complex, program transformations.

--nondet-volatile

Makes reads from volatile variables non-deterministic

--isr function

Instruments an interrupt service routine with the given name

--mmio

Instruments memory-mapped I/O

--nondet-static

Variables with static lifetime are initialized non-deterministically

--dump-c

Output ANSI-C source code instead of a goto binary.

BMC OPTIONS (cbmc)

--all-properties

Report status of all properties

--show-properties

Only show properties

--show-loops

Show the loops in the program

--cover-assertions

Check which assertions are reachable

--function name

Set main function name

--property id

Only check specific property with given identifier

--program-only

Only show program expression

--depth nr

Limit search depth

--unwind nr

Unwind loops nr times

--unwindset L:B,...

Unwind loop L with a bound of B (use --show-loops to get the loop IDs)

--show-vcc

Show the verification conditions

--slice-formula

Remove assignments unrelated to property

--no-unwinding-assertions

Do not generate unwinding assertions

--no-pretty-names

Do not simplify identifiers

BACKEND OPTIONS (cbmc)

--dimacs

Generate CNF in DIMACS format for use by external SAT solvers

--beautify-greedy

Beautify the counterexample (greedy heuristic)

--smt2

Output subgoals in SMT2 syntax

--boolector

Use Boolector (experimental)

--mathsat

Use MathSAT (experimental)

--cvc

Use CVC3 (experimental)

--yices

Use Yices (experimental)

--z3

Use Z3 (experimental)

--refine

Use refinement procedure (experimental)

--outfile filename

Output formula to given file

--arrays-uf-never

Never turn arrays into uninterpreted functions

--arrays-uf-always

Always turn arrays into uninterpreted functions