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 re‐
33       sult  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 fi‐
47       nally (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 ma‐
69       chine 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 [T:]L:B,...
187              Unwind loop L with a bound of B, optionally restricted to thread
188              T.  Use --show-loops to get the loop IDs. Thread numbers are set
189              as follows: The initial thread has index 0, and threads are con‐
190              secutively  numbered  in program order of threads being spawned.
191              The`--unwindset` option can be given multiple times.
192
193       --show-vcc
194              Show the verification conditions
195
196       --slice-formula
197              Remove assignments unrelated to property
198
199       --no-unwinding-assertions
200              Do not generate unwinding assertions
201
202       --no-pretty-names
203              Do not simplify identifiers
204
205   BACKEND OPTIONS (cbmc)
206       --dimacs
207              Generate CNF in DIMACS format for use by external SAT solvers
208
209       --beautify-greedy
210              Beautify the counterexample (greedy heuristic)
211
212       --smt2 Output subgoals in SMT2 syntax
213
214       --boolector
215              Use Boolector (experimental)
216
217       --mathsat
218              Use MathSAT (experimental)
219
220       --cvc3 Use CVC3 (experimental)
221
222       --cvc4 Use CVC4 (experimental)
223
224       --yices
225              Use Yices (experimental)
226
227       --z3   Use Z3 (experimental)
228
229       --refine
230              Use refinement procedure (experimental)
231
232       --outfile filename
233              Output formula to given file
234
235       --arrays-uf-never
236              Never turn arrays into uninterpreted functions
237
238       --arrays-uf-always
239              Always turn arrays into uninterpreted functions
240

ENVIRONMENT

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