NAME¶
cbmc - Bounded Model Checker for C/C++ and Java programs
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-specificed) 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-deretministically
- --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
ENVIRONMENT¶
CBMC does not regognize any environment variables. Note, however, that the
preprocessor used by CBMC will use environment variables to locate header
files. GOTO-CC aims to accept all environment variables that GCC does.
COPYRIGHT¶
2001-2014, Daniel Kroening, Edmund Clarke