1CBMC(1)                           User Manual                          CBMC(1)
2
3
4

NAME

6       cbmc - Bounded Model Checker for C/C++ and Java programs
7

SYNOPSIS

9       cbmc [--property property-id] file.c ...
10
11       cbmc [--show-properties] file.c ...
12
13       cbmc [--all-properties] file.c ...
14
15       goto-cc [-I include-path] [-c] file.c [-o outfile.o]
16
17       goto-instrument infile outfile
18
19
20       Only the most useful options are listed here; see below for the remain‐
21       der.
22

DESCRIPTION

24       cbmc generates traces that demonstrate how an  assertion  can  be  vio‐
25       lated,  or  proves that the assertion cannot be violated within a given
26       number of loop iterations.  CBMC can read C/C++  source-code  directly,
27       or  a  goto-binary  generated  by  goto-cc.  Java programs are given as
28       class or JAR files.  Without any further options, cbmc checks all prop‐
29       erties  (automatically  generated  or user-specified) found in the pro‐
30       gram.  If any of the properties can be violated,  a  counterexample  is
31       printed and the analysis is aborted.  The analysis can be restricted to
32       a particular property with the  --property  option.   The  verification
33       result for all properties can be obtained by means of the --all-proper‐
34       ties option.
35
36       goto-cc reads source code, and generates a  goto-binary.  Its  command-
37       line interface is designed to mimic that of gcc(1).  Note in particular
38       that goto-cc distinguishes between compiling and linking  phases,  just
39       as gcc does. cbmc expects a goto-binary for which linking has been com‐
40       pleted.
41
42       goto-instrument reads a goto-binary, performs a given program transfor‐
43       mation, and then writes the resulting program as goto-binary on disc.
44
45       The  usual  flow  is  to  (1) translate source into a goto-binary using
46       goto-cc, then (2) perform  instrumentation  with  goto-instrument,  and
47       finally (3) perform the analysis with cbmc.
48

OPTIONS

50   FRONTEND OPTIONS (cbmc and goto-cc)
51       -I path
52              Set include path (C/C++)
53
54       -D macro
55              Define preprocessor macro (C/C++)
56
57       --preprocess
58              Stop after preprocessing
59
60       --show-symbol-table
61              Show symbol table
62
63       --show-goto-functions
64              Show goto program
65
66
67   ARCHITECTURAL OPTIONS (cbmc and goto-cc)
68       cbmc  by  default  uses  architectural settings that match those of the
69       machine cbmc is executed on, i.e., the settings below are  only  needed
70       when  verifying  software that is meant to run on a different architec‐
71       ture or OS. goto-cc generates a goto-binary for a particular  architec‐
72       ture, i.e., the architecture cannot be changed after the goto-binary is
73       generated.
74
75       --16, --32, --64
76              Set width of int
77
78       --LP64, --ILP64, --LLP64, --ILP32, --LP32
79              Set width of int, long and pointers
80
81       --little-endian
82              Allow little-endian word-byte conversions
83
84       --big-endian
85              Allow big-endian word-byte conversions
86
87       --unsigned-char
88              Make "char" unsigned by default
89
90       --arch Set target architecture
91
92       --os   Set target operating system
93
94       --no-arch
95              Don't set up an architecture
96
97       --no-library
98              Disable built-in abstract C library
99
100       --round-to-nearest, --round-to-plus-inf, --round-to-minus-inf, --round-
101       to-zero
102              IEEE floating point rounding mode to use when the program begins
103              (default is round to nearest). The  program  under  verification
104              can override this setting, e.g., with fesetround(3).
105
106   PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)
107       Both  cbmc  and goto-instrument can generate assertions that catch spe‐
108       cific common errors, as listed below.
109
110       --bounds-check
111              Enable array bounds checks
112
113       --div-by-zero-check
114              Enable division by zero checks
115
116       --pointer-check
117              Enable pointer checks
118
119       --signed-overflow-check
120              Enable arithmetic over- and underflow checks for signed  integer
121              arithmetic
122
123       --unsigned-overflow-check
124              Enable  arithmetic over- and underflow checks for unsigned inte‐
125              ger arithmetic
126
127       --nan-check
128              Check floating-point computations for NaN
129
130       --no-assertions
131              Ignore user-provided assertions
132
133       --no-assumptions
134              Ignore user-provided assumptions
135
136       --error-label label
137              Check that the given label is unreachable
138
139   PROGRAM INSTRUMENTATION OPTIONS (goto-instrument only)
140       goto-instrument supports further,  more  complex,  program  transforma‐
141       tions.
142
143       --nondet-volatile
144              Makes reads from volatile variables non-deterministic
145
146       --isr function
147              Instruments an interrupt service routine with the given name
148
149       --mmio Instruments memory-mapped I/O
150
151       --nondet-static
152              Variables with static lifetime are initialized non-deterministi‐
153              cally
154
155       --dump-c
156              Output ANSI-C source code instead of a goto binary.
157
158   BMC OPTIONS (cbmc)
159       --all-properties
160              Report status of all properties
161
162       --show-properties
163              Only show properties
164
165       --show-loops
166              Show the loops in the program
167
168       --cover-assertions
169              Check which assertions are reachable
170
171       --function name
172              Set main function name
173
174       --property id
175              Only check specific property with given identifier
176
177       --program-only
178              Only show program expression
179
180       --depth nr
181              Limit search depth
182
183       --unwind nr
184              Unwind loops nr times
185
186       --unwindset L:B,...
187              Unwind loop L with a bound of B (use  --show-loops  to  get  the
188              loop IDs)
189
190       --show-vcc
191              Show the verification conditions
192
193       --slice-formula
194              Remove assignments unrelated to property
195
196       --no-unwinding-assertions
197              Do not generate unwinding assertions
198
199       --no-pretty-names
200              Do not simplify identifiers
201
202   BACKEND OPTIONS (cbmc)
203       --dimacs
204              Generate CNF in DIMACS format for use by external SAT solvers
205
206       --beautify-greedy
207              Beautify the counterexample (greedy heuristic)
208
209       --smt2 Output subgoals in SMT2 syntax
210
211       --boolector
212              Use Boolector (experimental)
213
214       --mathsat
215              Use MathSAT (experimental)
216
217       --cvc  Use CVC3 (experimental)
218
219       --yices
220              Use Yices (experimental)
221
222       --z3   Use Z3 (experimental)
223
224       --refine
225              Use refinement procedure (experimental)
226
227       --outfile filename
228              Output formula to given file
229
230       --arrays-uf-never
231              Never turn arrays into uninterpreted functions
232
233       --arrays-uf-always
234              Always turn arrays into uninterpreted functions
235

ENVIRONMENT

237       All  tools honor the TMPDIR environment variable when generating tempo‐
238       rary files and directories. Furthermore note that the preprocessor used
239       by  CBMC will use environment variables to locate header files. GOTO-CC
240       aims to accept all environment variables that GCC does.
241
243       2001-2016, Daniel Kroening, Edmund Clarke
244
245
246
247cbmc-4.7                           JUNE 2014                           CBMC(1)
Impressum