Bounded model checker for c/c++ and java programs
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.
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.
Set include path (C/C++)
Define preprocessor macro (C/C++)
Stop after preprocessing
Show symbol table
Show goto program
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.
Set width of int
Set width of int, long and pointers
Allow little-endian word-byte conversions
Allow big-endian word-byte conversions
Make "char" unsigned by default
Set target architecture
Set target operating system
Don't set up an architecture
Disable built-in abstract C library
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).
Both cbmc and goto-instrument can generate assertions that catch specific common errors, as listed below.
Enable array bounds checks
Enable division by zero checks
Enable pointer checks
Enable arithmetic over- and underflow checks for signed integer arithmetic
Enable arithmetic over- and underflow checks for unsigned integer arithmetic
Check floating-point computations for NaN
Ignore user-provided assertions
Ignore user-provided assumptions
Check that the given label is unreachable
goto-instrument supports further, more complex, program transformations.
Makes reads from volatile variables non-deterministic
Instruments an interrupt service routine with the given name
Instruments memory-mapped I/O
Variables with static lifetime are initialized non-deretministically
Output ANSI-C source code instead of a goto binary.
Report status of all properties
Only show properties
Show the loops in the program
Check which assertions are reachable
Set main function name
Only check specific property with given identifier
Only show program expression
Limit search depth
Unwind loops nr times
Unwind loop L with a bound of B (use --show-loops to get the loop IDs)
Show the verification conditions
Remove assignments unrelated to property
Do not generate unwinding assertions
Do not simplify identifiers
Generate CNF in DIMACS format for use by external SAT solvers
Beautify the counterexample (greedy heuristic)
Output subgoals in SMT1 syntax (experimental)
Output subgoals in SMT2 syntax (experimental)
Use Boolector (experimental)
Use MathSAT (experimental)
Use CVC3 (experimental)
Use Yices (experimental)
Use Z3 (experimental)
Use refinement procedure (experimental)
Output formula to given file
Never turn arrays into uninterpreted functions
Always turn arrays into uninterpreted functions
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.
2001-2014, Daniel Kroening, Edmund Clarke