1CBMC(1) User Manual CBMC(1)
2
6 cbmc - Bounded Model Checker for C/C++ and Java programs
7
9 cbmc [--property property-id] file.c ...
10 cbmc [--show-properties] file.c ...
12 cbmc [--all-properties] file.c ...
14 goto-cc [-I include-path] [-c] file.c [-o outfile.o]
16 goto-instrument infile outfile
18 Only the most useful options are listed here; see below for the remain‐
21 der.
22
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 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 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 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
50 FRONTEND OPTIONS (cbmc and goto-cc)
51 -I path
52 Set include path (C/C++)
53 -D macro
55 Define preprocessor macro (C/C++)
56 --preprocess
58 Stop after preprocessing
59 --show-symbol-table
61 Show symbol table
62 --show-goto-functions
64 Show goto program
65 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 --16, --32, --64
76 Set width of int
77 --LP64, --ILP64, --LLP64, --ILP32, --LP32
79 Set width of int, long and pointers
80 --little-endian
82 Allow little-endian word-byte conversions
83 --big-endian
85 Allow big-endian word-byte conversions
86 --unsigned-char
88 Make "char" unsigned by default
89 --arch Set target architecture
91 --os Set target operating system
93 --no-arch
95 Don't set up an architecture
96 --no-library
98 Disable built-in abstract C library
99 --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 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 --bounds-check
111 Enable array bounds checks
112 --div-by-zero-check
114 Enable division by zero checks
115 --pointer-check
117 Enable pointer checks
118 --signed-overflow-check
120 Enable arithmetic over- and underflow checks for signed integer
121 arithmetic
122 --unsigned-overflow-check
124 Enable arithmetic over- and underflow checks for unsigned inte‐
125 ger arithmetic
126 --nan-check
128 Check floating-point computations for NaN
129 --no-assertions
131 Ignore user-provided assertions
132 --no-assumptions
134 Ignore user-provided assumptions
135 --error-label label
137 Check that the given label is unreachable
138 PROGRAM INSTRUMENTATION OPTIONS (goto-instrument only)
140 goto-instrument supports further, more complex, program transforma‐
141 tions.
142 --nondet-volatile
144 Makes reads from volatile variables non-deterministic
145 --isr function
147 Instruments an interrupt service routine with the given name
148 --mmio Instruments memory-mapped I/O
150 --nondet-static
152 Variables with static lifetime are initialized non-deterministi‐
153 cally
154 --dump-c
156 Output ANSI-C source code instead of a goto binary.
157 BMC OPTIONS (cbmc)
159 --all-properties
160 Report status of all properties
161 --show-properties
163 Only show properties
164 --show-loops
166 Show the loops in the program
167 --cover-assertions
169 Check which assertions are reachable
170 --function name
172 Set main function name
173 --property id
175 Only check specific property with given identifier
176 --program-only
178 Only show program expression
179 --depth nr
181 Limit search depth
182 --unwind nr
184 Unwind loops nr times
185 --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 --show-vcc
194 Show the verification conditions
195 --slice-formula
197 Remove assignments unrelated to property
198 --no-unwinding-assertions
200 Do not generate unwinding assertions
201 --no-pretty-names
203 Do not simplify identifiers
204 BACKEND OPTIONS (cbmc)
206 --dimacs
207 Generate CNF in DIMACS format for use by external SAT solvers
208 --beautify-greedy
210 Beautify the counterexample (greedy heuristic)
211 --smt2 Output subgoals in SMT2 syntax
213 --boolector
215 Use Boolector (experimental)
216 --mathsat
218 Use MathSAT (experimental)
219 --cvc3 Use CVC3 (experimental)
221 --cvc4 Use CVC4 (experimental)
223 --yices
225 Use Yices (experimental)
226 --z3 Use Z3 (experimental)
228 --refine
230 Use refinement procedure (experimental)
231 --outfile filename
233 Output formula to given file
234 --arrays-uf-never
236 Never turn arrays into uninterpreted functions
237 --arrays-uf-always
239 Always turn arrays into uninterpreted functions
240
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
249cbmc-4.7 JUNE 2014 CBMC(1)