SYNOPSIS

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.

DESCRIPTION

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 source-code directly, or a goto-binary generated by goto-cc. Java programs are given as class 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 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 distinguishes between compiling and linking phases, just as gcc does. cbmc expects a goto-binary for which linking has been completed.

goto-instrument 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.

OPTIONS

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)

--smt1

Output subgoals in SMT1 syntax (experimental)

--smt2

Output subgoals in SMT2 syntax (experimental)

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

COPYRIGHT

2001-2014, Daniel Kroening, Edmund Clarke