184 lines
6.2 KiB
Groff
184 lines
6.2 KiB
Groff
.\" Process this file with
|
|
.\" groff -man -Tascii cbmc.1
|
|
.\"
|
|
.TH CBMC 1 "JUNE 2014" "cbmc-4.7" "User Manual"
|
|
.SH NAME
|
|
cbmc \- Bounded Model Checker for C/C++ and Java programs
|
|
.SH SYNOPSIS
|
|
.B cbmc [--property \fIproperty-id\fB] \fIfile.c\fB ...
|
|
|
|
.B cbmc [--show-properties] \fIfile.c\fB ...
|
|
|
|
.B cbmc [--all-properties] \fIfile.c\fB ...
|
|
|
|
.B goto-cc [-I \fIinclude-path\fB] [-c] \fIfile.c\fB [-o \fIoutfile.o\fB]
|
|
|
|
.B goto-instrument \fIinfile\fB \fIoutfile\fR
|
|
|
|
.PP
|
|
Only the most useful options are listed here; see below for the remainder.
|
|
.SH DESCRIPTION
|
|
\fBcbmc\fR 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.
|
|
|
|
\fBgoto-cc\fR reads source code, and generates a goto-binary. Its
|
|
command-line interface is designed to mimic that of
|
|
.BR gcc (1).
|
|
Note in particular that \fBgoto-cc\fR distinguishes between compiling
|
|
and linking phases, just as gcc does. \fBcbmc\fR expects a goto-binary
|
|
for which linking has been completed.
|
|
|
|
\fBgoto-instrument\fR 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.
|
|
.SH OPTIONS
|
|
.SS "FRONTEND OPTIONS (cbmc and goto-cc)"
|
|
.IP "-I path"
|
|
Set include path (C/C++)
|
|
.IP "-D macro"
|
|
Define preprocessor macro (C/C++)
|
|
.IP --preprocess
|
|
Stop after preprocessing
|
|
.IP --show-symbol-table
|
|
Show symbol table
|
|
.IP --show-goto-functions
|
|
Show goto program
|
|
|
|
.SS "ARCHITECTURAL OPTIONS (cbmc and goto-cc)"
|
|
\fBcbmc\fR by default uses architectural settings that match those of the
|
|
machine \fBcbmc\fR 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. \fBgoto-cc\fR generates a goto-binary for a particular architecture,
|
|
i.e., the architecture cannot be changed after the goto-binary is generated.
|
|
.IP "--16, --32, --64"
|
|
Set width of int
|
|
.IP "--LP64, --ILP64, --LLP64, --ILP32, --LP32"
|
|
Set width of int, long and pointers
|
|
.IP --little-endian
|
|
Allow little-endian word-byte conversions
|
|
.IP --big-endian
|
|
Allow big-endian word-byte conversions
|
|
.IP --unsigned-char
|
|
Make "char" unsigned by default
|
|
.IP --arch
|
|
Set target architecture
|
|
.IP --os
|
|
Set target operating system
|
|
.IP --no-arch
|
|
Don't set up an architecture
|
|
.IP --no-library
|
|
Disable built-in abstract C library
|
|
.IP "--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
|
|
.BR fesetround (3).
|
|
.SS "PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)"
|
|
Both \fBcbmc\fR and \fBgoto-instrument\fR can generate assertions that
|
|
catch specific common errors, as listed below.
|
|
.IP --bounds-check
|
|
Enable array bounds checks
|
|
.IP --div-by-zero-check
|
|
Enable division by zero checks
|
|
.IP --pointer-check
|
|
Enable pointer checks
|
|
.IP --signed-overflow-check
|
|
Enable arithmetic over- and underflow checks for signed integer arithmetic
|
|
.IP --unsigned-overflow-check
|
|
Enable arithmetic over- and underflow checks for unsigned integer arithmetic
|
|
.IP --nan-check
|
|
Check floating-point computations for NaN
|
|
.IP --no-assertions
|
|
Ignore user-provided assertions
|
|
.IP --no-assumptions
|
|
Ignore user-provided assumptions
|
|
.IP "--error-label label"
|
|
Check that the given label is unreachable
|
|
.SS "PROGRAM INSTRUMENTATION OPTIONS (goto-instrument only)"
|
|
\fBgoto-instrument\fR supports further, more complex, program
|
|
transformations.
|
|
.IP --nondet-volatile
|
|
Makes reads from volatile variables non-deterministic
|
|
.IP "--isr function"
|
|
Instruments an interrupt service routine with the given name
|
|
.IP --mmio
|
|
Instruments memory-mapped I/O
|
|
.IP --nondet-static
|
|
Variables with static lifetime are initialized non-deretministically
|
|
.IP --dump-c
|
|
Output ANSI-C source code instead of a goto binary.
|
|
.SS "BMC OPTIONS (cbmc)"
|
|
.IP --all-properties
|
|
Report status of all properties
|
|
.IP --show-properties
|
|
Only show properties
|
|
.IP --show-loops
|
|
Show the loops in the program
|
|
.IP --cover-assertions
|
|
Check which assertions are reachable
|
|
.IP "--function name"
|
|
Set main function name
|
|
.IP "--property id"
|
|
Only check specific property with given identifier
|
|
.IP --program-only
|
|
Only show program expression
|
|
.IP "--depth nr "
|
|
Limit search depth
|
|
.IP "--unwind nr "
|
|
Unwind loops nr times
|
|
.IP "--unwindset L:B,..."
|
|
Unwind loop L with a bound of B (use \-\-show\-loops to get the loop IDs)
|
|
.IP --show-vcc
|
|
Show the verification conditions
|
|
.IP --slice-formula
|
|
Remove assignments unrelated to property
|
|
.IP --no-unwinding-assertions
|
|
Do not generate unwinding assertions
|
|
.IP --no-pretty-names
|
|
Do not simplify identifiers
|
|
.SS "BACKEND OPTIONS (cbmc)"
|
|
.IP --dimacs
|
|
Generate CNF in DIMACS format for use by external SAT solvers
|
|
.IP --beautify-greedy
|
|
Beautify the counterexample (greedy heuristic)
|
|
.IP --smt1
|
|
Output subgoals in SMT1 syntax (experimental)
|
|
.IP --smt2
|
|
Output subgoals in SMT2 syntax (experimental)
|
|
.IP --boolector
|
|
Use Boolector (experimental)
|
|
.IP --mathsat
|
|
Use MathSAT (experimental)
|
|
.IP --cvc
|
|
Use CVC3 (experimental)
|
|
.IP --yices
|
|
Use Yices (experimental)
|
|
.IP --z3
|
|
Use Z3 (experimental)
|
|
.IP --refine
|
|
Use refinement procedure (experimental)
|
|
.IP "--outfile filename"
|
|
Output formula to given file
|
|
.IP --arrays-uf-never
|
|
Never turn arrays into uninterpreted functions
|
|
.IP --arrays-uf-always
|
|
Always turn arrays into uninterpreted functions
|
|
.SH 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.
|
|
.SH COPYRIGHT
|
|
2001-2014, Daniel Kroening, Edmund Clarke
|