cprover
/builddir/build/BUILD/cbmc-cbmc-5.10/doc/cbmc-user-manual.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page cbmc-user-manual CBMC User Manual
3 
4 \author Daniel Kroening
5 
6 This tutorial is intended for users of CProver primarily focused on CBMC.
7 
8 \tableofcontents
9 
10 \section man_introduction Introduction
11 
12 ## Motivation
13 
14 Numerous tools to hunt down functional design flaws in silicon have been
15 available for many years, mainly due to the enormous cost of hardware
16 bugs. The use of such tools is wide-spread. In contrast, the market for
17 tools that address the need for quality software is still in its
18 infancy.
19 
20 Research in software quality has an enormous breadth. We focus the
21 presentation using two criteria:
22 
23 1. We believe that any form of quality requires a specific *guarantee*,
24  in theory and practice.
25 2. The sheer size of software designs requires techniques that are
26  highly *automated*.
27 
28 In practice, quality guarantees usually do not refer to "total
29 correctness" of a design, as ensuring the absence of all bugs is too
30 expensive for most applications. In contrast, a guarantee of the absence
31 of specific flaws is achievable, and is a good metric of quality.
32 
33 ## Bounded Model Checking with CBMC
34 
35 CBMC implements a technique called *Bounded Model Checking* (BMC). In
36 BMC, the transition relation for a complex state machine and its
37 specification are jointly unwound to obtain a Boolean formula, which is
38 then checked for satisfiability by using an efficient SAT procedure. If
39 the formula is satisfiable, a counterexample is extracted from the
40 output of the SAT procedure. If the formula is not satisfiable, the
41 program can be unwound more to determine if a longer counterexample
42 exists.
43 
44 In many engineering domains, real-time guarantees are a strict
45 requirement. An example is software embedded in automotive controllers.
46 As a consequence, the loop constructs in these types of programs often
47 have a strict bound on the number of iterations. CBMC is able to
48 formally verify such bounds by means of *unwinding assertions*. Once
49 this bound is established, CBMC is able to prove the absence of errors.
50 
51 A more detailed description of how to apply CBMC to verify programs is
52 \ref man_cbmc-tutorial "here".
53 
54 
55 ### Example: Buffer Overflows
56 
57 In order to give a brief overview of the capabilities of CBMC
58 we start with a small example. The issue of *[buffer
59 overflows](http://en.wikipedia.org/wiki/Buffer_overflow)* has obtained
60 wide public attention. A buffer is a contiguously-allocated chunk of
61 memory, represented by an array or a pointer in C. Programs written in C
62 do not provide automatic bounds checking on the buffer, which means a
63 program can – accidentally or maliciously – write past a buffer. The
64 following example is a perfectly valid C program (in the sense that a
65 compiler compiles it without any errors):
66 
67 ```{.c}
68 int main()
69 {
70  int buffer[10];
71  buffer[20] = 10;
72 }
73 ```
74 
75 However, the write access to an address outside the allocated memory
76 region can lead to unexpected behavior. In particular, such bugs can be
77 exploited to overwrite the return address of a function, thus enabling
78 the execution of arbitrary user-induced code. CBMC is able
79 to detect this problem and reports that the "upper bound property" of
80 the buffer is violated. CBMC is capable of checking these
81 lower and upper bounds, even for arrays with dynamic size. A detailed
82 discussion of the properties that CBMC can check
83 automatically is \ref man_instrumentation-properties "here".
84 
85 ## Hardware/Software Co-Verification
86 
87 Software programs often interact with hardware in a non-trivial manner,
88 and many properties of the overall design only arise from the interplay
89 of both components. CBMC and SATABS therefore support *Co-Verification*,
90 i.e., are able to reason about a C/C++ program together with a circuit
91 description given in Verilog.
92 
93 These co-verification capabilities can also be applied to perform
94 refinement proofs. Software programs are often used as high-level
95 descriptions of circuitry. While both describe the same functionality,
96 the hardware implementation usually contains more detail. It is highly
97 desirable to establish some form for equivalence between the two
98 descriptions. Hardware/Software co-verification and equivalence checking
99 with CBMC is described
100 \ref man_hard-soft-introduction "here".
101 
102 
103 \section man_installation Installation
104 
105 \subsection man_install-cbmc Installing CBMC
106 
107 ### Requirements
108 
109 CBMC is available for Windows, i86 Linux, and MacOS X. CBMC requires a
110 code pre-processing environment comprising of a suitable preprocessor
111 and an a set of header files.
112 
113 1. **Linux:** the preprocessor and the header files typically come with
114  a package called *gcc*, which must be installed prior to the
115  installation of CBMC.
116 
117 2. **Windows:** The Windows version of CBMC requires the preprocessor
118  `cl.exe`, which is part of Microsoft Visual Studio. We recommend the
119  free [Visual Studio Community
120  2013](http://www.visualstudio.com/en-us/products/visual-studio-community-vs).
121 
122 3. **MacOS:** Install the [XCode Command Line
123  Utilities](http://developer.apple.com/technologies/xcode.html) prior
124  to installing CBMC. Just installing XCode alone is not enough.
125 
126 Important note for Windows users: Visual Studio's `cl.exe` relies on a
127 complex set of environment variables to identify the target architecture
128 and the directories that contain the header files. You must run CBMC
129 from within the *Visual Studio Command Prompt*.
130 
131 Note that the distribution files for the [Eclipse
132 plugin](installation-plugin.shtml) include the CBMC executable.
133 Therefore, if you intend to run CBMC exclusively within Eclipse, you can
134 skip the installation of the CBMC executable. However, you still have to
135 install the compiler environment as described above.
136 
137 ### Installing the CBMC Binaries
138 
139 1. Download CBMC for your operating system. The binaries are available
140  from http://www.cprover.org/cbmc/.
141 2. Unzip/untar the archive into a directory of your choice. We
142  recommend to add this directory to your `PATH` environment variable.
143 
144 You are now ready to \ref man_cbmc-tutorial "use CBMC"!
145 
146 ### Building CBMC from Source
147 
148 Alternatively, the CBMC source code is available [via
149 SVN](http://www.cprover.org/svn/cbmc/). To compile the source code,
150 follow [these
151 instructions](http://www.cprover.org/svn/cbmc/trunk/COMPILING).
152 
153 
154 
155 \subsection man_install-eclipse Installing the Eclipse Plugin
156 
157 ### Requirements
158 
159 We provide a graphical user interface to CBMC which is
160 realized as a plugin to the Eclipse framework. Eclipse is available at
161 http://www.eclipse.org. We do not provide installation instructions for
162 Eclipse (basically, you only have to download the current version and
163 extract the files to your hard-disk) and assume that you have already
164 installed the current version.
165 
166 Important note for Windows users: Visual Studio's `cl.exe` relies on a
167 complex set of environment variables to identify the target architecture
168 and the directories that contain the header files. You must run Eclipse
169 from within the *Visual Studio Command Prompt*.
170 
171 ### Installing the Eclipse Plugin
172 
173 The installation instructions for the Eclipse Plugin, including the link
174 to the download site, are available
175 [here](http://www.cprover.org/eclipse-plugin/). This includes a small
176 tutorial on how to use the Eclipse plugin.
177 
178 \section man_cbmc CBMC: Bounded Model Checking for C, C++ and Java
179 
180 \subsection man_cbmc-tutorial A Short Tutorial
181 
182 ### First Steps
183 
184 We assume you have already installed CBMC and the necessary support
185 files on your system. If not so, please follow the instructions
186 \ref man_install-cbmc "here".
187 
188 Like a compiler, CBMC takes the names of .c files as command line
189 arguments. CBMC then translates the program and merges the function
190 definitions from the various .c files, just like a linker. But instead
191 of producing a binary for execution, CBMC performs symbolic simulation
192 on the program.
193 
194 As an example, consider the following simple program, named file1.c:
195 
196  int puts(const char *s) { }
197 
198  int main(int argc, char **argv) {
199  puts(argv[2]);
200  }
201 
202 Of course, this program is faulty, as the `argv` array might have fewer
203 than three elements, and then the array access `argv[2]` is out of
204 bounds. Now, run CBMC as follows:
205 
206  cbmc file1.c --show-properties --bounds-check --pointer-check
207 
208 The two options `--bounds-check` and `--pointer-check` instruct CBMC to
209 look for errors related to pointers and array bounds. CBMC will print
210 the list of properties it checks. Note that it lists, among others, a
211 property labelled with "object bounds in argv" together with the location
212 of the faulty array access. As you can see, CBMC largely determines the
213 property it needs to check itself. This is realized by means of a
214 preliminary static analysis, which relies on computing a fixed point on
215 various [abstract
216 domains](http://en.wikipedia.org/wiki/Abstract_interpretation). More
217 detail on automatically generated properties is provided
218 \ref man_instrumentation-properties "here".
219 
220 Note that these automatically generated properties need not necessarily
221 correspond to bugs – these are just *potential* flaws, as abstract
222 interpretation might be imprecise. Whether these properties hold or
223 correspond to actual bugs needs to be determined by further analysis.
224 
225 CBMC performs this analysis using *symbolic simulation*, which
226 corresponds to a translation of the program into a formula. The formula
227 is then combined with the property. Let's look at the formula that is
228 generated by CBMC's symbolic simulation:
229 
230  cbmc file1.c --show-vcc --bounds-check --pointer-check
231 
232 With this option, CBMC performs the symbolic simulation and prints the
233 verification conditions on the screen. A verification condition needs to
234 be proven to be valid by a [decision
235 procedure](http://en.wikipedia.org/wiki/Decision_problem) in order to
236 assert that the corresponding property holds. Let's run the decision
237 procedure:
238 
239  cbmc file1.c --bounds-check --pointer-check
240 
241 CBMC transforms the equation you have seen before into CNF and passes it
242 to a SAT solver (more background on this step is in the book on
243 [Decision Procedures](http://www.decision-procedures.org/)). It then
244 determines which of the properties that it has generated for the program
245 hold and which do not. Using the SAT solver, CBMC detects that the
246 property for the object bounds of `argv` does not hold, and will thus
247 print a line as follows:
248 
249  [main.pointer_dereference.6] dereference failure: object bounds in argv[(signed long int)2]: FAILURE
250 
251 ### Counterexample Traces
252 
253 Let us have a closer look at this property and why it fails. To aid the
254 understanding of the problem, CBMC can generate a *counterexample trace*
255 for failed properties. To obtain this trace, run
256 
257  cbmc file1.c --bounds-check --trace
258 
259 CBMC then prints a counterexample trace, i.e., a program trace that
260 begins with `main` and ends in a state which violates the property. In
261 our example, the program trace ends in the faulty array access. It also
262 gives the values the input variables must have for the bug to occur. In
263 this example, `argc` must be one to trigger the out-of-bounds array
264 access. If you add a branch to the example that requires that `argc>=3`,
265 the bug is fixed and CBMC will report that the proofs of all properties
266 have been successful.
267 
268 ### Verifying Modules
269 
270 In the example above, we used a program that starts with a `main`
271 function. However, CBMC is aimed at embedded software, and these kinds
272 of programs usually have different entry points. Furthermore, CBMC is
273 also useful for verifying program modules. Consider the following
274 example, called file2.c:
275 
276  int array[10];
277  int sum() {
278  unsigned i, sum;
279 
280  sum=0;
281  for(i=0; i<10; i++)
282  sum+=array[i];
283  }
284 
285 In order to set the entry point to the `sum` function, run
286 
287  cbmc file2.c --function sum --bounds-check
288 
289 It is often necessary to build a suitable *harness* for the function in
290 order to set up the environment appropriately.
291 
292 ### Loop Unwinding
293 
294 When running the previous example, you will have noted that CBMC unwinds
295 the `for` loop in the program. As CBMC performs Bounded Model Checking,
296 all loops have to have a finite upper run-time bound in order to
297 guarantee that all bugs are found. CBMC can optionally check that enough
298 unwinding is performed. As an example, consider the program binsearch.c:
299 
300  int binsearch(int x) {
301  int a[16];
302  signed low=0, high=16;
303 
304  while(low<high) {
305  signed middle=low+((high-low)>>1);
306 
307  if(a[middle]<x)
308  high=middle;
309  else if(a[middle]>x)
310  low=middle+1;
311  else // a[middle]==x
312  return middle;
313  }
314 
315  return -1;
316  }
317 
318 If you run CBMC on this function, you will notice that the unwinding
319 does not stop on its own. The built-in simplifier is not able to
320 determine a run time bound for this loop. The unwinding bound has to be
321 given as a command line argument:
322 
323  cbmc binsearch.c --function binsearch --unwind 6 --bounds-check --unwinding-assertions
324 
325 CBMC verifies that verifies the array accesses are within the bounds;
326 note that this actually depends on the result of the right shift. In
327 addition, as CBMC is given the option `--unwinding-assertions`, it also
328 checks that enough unwinding is done, i.e., it proves a run-time bound.
329 For any lower unwinding bound, there are traces that require more loop
330 iterations. Thus, CBMC will report that the unwinding assertion has
331 failed. As usual, a counterexample trace that documents this can be
332 obtained with the option `--property`.
333 
334 ### Unbounded Loops
335 
336 CBMC can also be used for programs with unbounded loops. In this case,
337 CBMC is used for bug hunting only; CBMC does not attempt to find all
338 bugs. The following program (lock-example.c) is an example of a program
339 with a user-specified property:
340 
341 ```
342  _Bool nondet_bool();
343  _Bool LOCK = 0;
344 
345  _Bool lock() {
346  if(nondet_bool()) {
347  assert(!LOCK);
348  LOCK=1;
349  return 1; }
350 
351  return 0;
352  }
353 
354  void unlock() {
355  assert(LOCK);
356  LOCK=0;
357  }
358 
359  int main() {
360  unsigned got_lock = 0;
361  int times;
362 
363  while(times > 0) {
364  if(lock()) {
365  got_lock++;
366  /* critical section */
367  }
368 
369  if(got_lock!=0)
370  unlock();
371 
372  got_lock--;
373  times--;
374  }
375  }
376 ```
377 
378 The `while` loop in the `main` function has no (useful) run-time bound.
379 Thus, a bound has to be set on the amount of unwinding that CBMC
380 performs. There are two ways to do so:
381 
382 1. The `--unwind` command-line parameter can to be used to limit the
383  number of times loops are unwound.
384 2. The `--depth` command-line parameter can be used to limit the number
385  of program steps to be processed.
386 
387 Given the option `--unwinding-assertions`, CBMC checks whether the
388 argument to `--unwind` is large enough to cover all program paths. If
389 the argument is too small, CBMC will detect that not enough unwinding is
390 done reports that an unwinding assertion has failed.
391 
392 Reconsider the example. For a loop unwinding bound of one, no bug is
393 found. But already for a bound of two, CBMC detects a trace that
394 violates an assertion. Without unwinding assertions, or when using the
395 `--depth` command line switch, CBMC does not prove the program correct,
396 but it can be helpful to find program bugs. The various command line
397 options that CBMC offers for loop unwinding are described in the section
398 on \ref man_cbmc-loops "understanding loop unwinding".
399 
400 ### A Note About Compilers and the ANSI-C Library
401 
402 Most C programs make use of functions provided by a library; instances
403 are functions from the standard ANSI-C library such as `malloc` or
404 `printf`. The verification of programs that use such functions has two
405 requirements:
406 
407 1. Appropriate header files have to be provided. These header files
408  contain *declarations* of the functions that are to be used.
409 2. Appropriate *definitions* have to be provided.
410 
411 Most C compilers come with header files for the ANSI-C library
412 functions. We briefly discuss how to obtain/install these library files.
413 
414 #### Linux
415 
416 Linux systems that are able to compile software are usually equipped
417 with the appropriate header files. Consult the documentation of your
418 distribution on how to install the compiler and the header files. First
419 try to compile some significant program before attempting to verify it.
420 
421 #### Windows
422 
423 On Microsoft Windows, CBMC is pre-configured to use the compiler that is
424 part of Microsoft's Visual Studio. Microsoft's [Visual Studio
425 Community](http://www.visualstudio.com/en-us/products/visual-studio-community-vs)
426 is fully featured and available for download for free from the Microsoft
427 webpage. Visual Studio installs the usual set of header files together
428 with the compiler. However, the Visual Studio compiler requires a large
429 set of environment variables to function correctly. It is therefore
430 required to run CBMC from the *Visual Studio Command Prompt*, which can
431 be found in the menu *Visual Studio Tools*.
432 
433 Note that in both cases, only header files are available. CBMC only
434 comes with a small set of definitions, which includes functions such as
435 `malloc`. Detailed information about the built-in definitions is
436 \ref man_instrumentation-libraries "here".
437 
438 ### Command Line Interface
439 
440 This section describes the command line interface of CBMC. Like a C
441 compiler, CBMC takes the names of the .c source files as arguments.
442 Additional options allow to customize the behavior of CBMC. Use
443 `cbmc --help` to get a full list of the available options.
444 
445 Structured output can be obtained from CBMC using the option `--xml-ui`.
446 Any output from CBMC (e.g., counterexamples) will then use an XML
447 representation.
448 
449 ### Further Reading
450 
451 - \ref man_cbmc-loops "Understanding Loop Unwinding"
452 - [Hardware Verification using ANSI-C Programs as a
453  Reference](http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html)
454 - [Behavioral Consistency of C and Verilog Programs Using Bounded
455  Model Checking](http://www-2.cs.cmu.edu/~svc/papers/view-publications-cky03.html)
456 - [A Tool for Checking ANSI-C
457  Programs](http://www-2.cs.cmu.edu/~svc/papers/view-publications-ckl2004.html)
458 
459 We also have a [list of interesting applications of
460 CBMC](http://www.cprover.org/cbmc/applications/).
461 
462 
463 \subsection man_cbmc-loops Understanding Loop Unwinding
464 
465 ### Iteration-based Unwinding
466 
467 The basic idea of CBMC is to model the computation of the programs up to
468 a particular depth. Technically, this is achieved by a process that
469 essentially amounts to *unwinding loops*. This concept is best
470 illustrated with a generic example:
471 
472 ```
473  int main(int argc, char **argv) {
474  while(cond) {
475  BODY CODE
476  }
477  }
478 ```
479 
480 A BMC instance that will find bugs with up to five iterations of the
481 loop would contain five copies of the loop body, and essentially
482 corresponds to checking the following loop-free program:
483 
484 ```
485  int main(int argc, char **argv) {
486  if(cond) {
487  BODY CODE COPY 1
488  if(cond) {
489  BODY CODE COPY 2
490  if(cond) {
491  BODY CODE COPY 3
492  if(cond) {
493  BODY CODE COPY 4
494  if(cond) {
495  BODY CODE COPY 5
496  }
497  }
498  }
499  }
500  }
501  }
502 ```
503 
504 Note the use of the `if` statement to prevent the execution of the loop
505 body in the case that the loop ends before five iterations are executed.
506 The construction above is meant to produce a program that is trace
507 equivalent with the original programs for those traces that contain up
508 to five iterations of the loop.
509 
510 In many cases, CBMC is able to automatically determine an upper bound on
511 the number of loop iterations. This may even work when the number of
512 loop unwindings is not constant. Consider the following example:
513 
514 ```
515  _Bool f();
516 
517  int main() {
518  for(int i=0; i<100; i++) {
519  if(f()) break;
520  }
521  assert(0);
522  }
523 ```
524 
525 The loop in the program above has an obvious upper bound on the number
526 of iterations, but note that the loop may abort prematurely depending on
527 the value that is returned by `f()`. CBMC is nevertheless able to
528 automatically unwind the loop to completion.
529 
530 This automatic detection of the unwinding bound may fail if the number
531 of loop iterations is highly data-dependent. Furthermore, the number of
532 iterations that are executed by any given loop may be too large or may
533 simply be unbounded. For this case, CBMC offers the command-line option
534 `--unwind B`, where `B` denotes a number that corresponds to the maximal
535 number of loop unwindings CBMC performs on any loop.
536 
537 Note that the number of unwindings is measured by counting the number of
538 *backjumps*. In the example above, note that the condition `i<100` is in
539 fact evaluated 101 times before the loop terminates. Thus, the loop
540 requires a limit of 101, and not 100.
541 
542 ### Setting Separate Unwinding Limits
543 
544 The setting given with `--unwind` is used globally, that is, for all
545 loops in the program. In order to set individual limits for the loops,
546 first use
547 
548  --show-loops
549 
550 to obtain a list of all loops in the program. Then identify the loops
551 you need to set a separate bound for, and note their loop ID. Then use
552 
553  --unwindset L:B,L:B,...
554 
555 where `L` denotes a loop ID and `B` denotes the bound for that loop.
556 
557 As an example, consider a program with two loops in the function main:
558 
559  --unwindset c::main.0:10,c::main.1:20
560 
561 This sets a bound of 10 for the first loop, and a bound of 20 for the
562 second loop.
563 
564 What if the number of unwindings specified is too small? In this case,
565 bugs that require paths that are deeper may be missed. In order to
566 address this problem, CBMC can optionally insert checks that the given
567 unwinding bound is actually sufficiently large. These checks are called
568 *unwinding assertions*, and are enabled with the option
569 `--unwinding-assertions`. Continuing the generic example above, this
570 unwinding assertion for a bound of five corresponds to checking the
571 following loop-free program:
572 
573 ```
574  int main(int argc, char **argv) {
575  if(cond) {
576  BODY CODE COPY 1
577  if(cond) {
578  BODY CODE COPY 2
579  if(cond) {
580  BODY CODE COPY 3
581  if(cond) {
582  BODY CODE COPY 4
583  if(cond) {
584  BODY CODE COPY 5
585  assert(!cond);
586  }
587  }
588  }
589  }
590  }
591  }
592 ```
593 
594 The unwinding assertions can be verified just like any other generated
595 assertion. If all of them are proven to hold, the given loop bounds are
596 sufficient for the program. This establishes a [high-level worst-case
597 execution time](http://en.wikipedia.org/wiki/Worst-case_execution_time)
598 (WCET).
599 
600 In some cases, it is desirable to cut off very deep loops in favor of
601 code that follows the loop. As an example, consider the following
602 program:
603 
604 ```
605  int main() {
606  for(int i=0; i<10000; i++) {
607  BODY CODE
608  }
609  assert(0);
610  }
611 ```
612 
613 In the example above, small values of `--unwind` will prevent that the
614 assertion is reached. If the code in the loop is considered irrelevant
615 to the later assertion, use the option
616 
617  --partial-loops
618 
619 This option will allow paths that execute loops only partially, enabling
620 a counterexample for the assertion above even for small unwinding
621 bounds. The disadvantage of using this option is that the resulting path
622 may be spurious, i.e., may not exist in the original program.
623 
624 ### Depth-based Unwinding
625 
626 The loop-based unwinding bound is not always appropriate. In particular,
627 it is often difficult to control the size of the generated formula when
628 using the `--unwind` option. The option
629 
630  --depth nr
631 
632 specifies an unwinding bound in terms of the number of instructions that
633 are executed on a given path, irrespectively of the number of loop
634 iterations. Note that CBMC uses the number of instructions in the
635 control-flow graph as the criterion, not the number of instructions in
636 the source code.
637 
638 \subsection man_cbmc-cover COVER: Test Suite Generation with CBMC
639 
640 
641 ### A Small Tutorial with A Case Study
642 
643 We assume that CBMC is installed on your system. If not so, follow
644 \ref man_install-cbmc "these instructions".
645 
646 CBMC can be used to automatically generate test cases that satisfy a
647 certain [code coverage](https://en.wikipedia.org/wiki/Code_coverage)
648 criteria. Common coverage criteria include branch coverage, condition
649 coverage and [Modified Condition/Decision Coverage
650 (MC/DC)](https://en.wikipedia.org/wiki/Modified_condition/decision_coverage).
651 Among others, MC/DC is required by several avionics software development
652 guidelines to ensure adequate testing of safety critical software.
653 Briefly, in order to satisfy MC/DC, for every conditional statement
654 containing boolean decisions, each Boolean variable should be evaluated
655 one time to "true" and one time to "false", in a way that affects the
656 outcome of the decision.
657 
658 In the following, we are going to demonstrate how to apply the test
659 suite generation functionality in CBMC, by means of a case study. The
660 following program is an excerpt from a real-time embedded benchmark
661 [PapaBench](https://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=97),
662 and implements part of a fly-by-wire autopilot for an Unmanned Aerial
663 Vehicle (UAV). It is adjusted mildly for our purposes.
664 
665 The aim of function `climb_pid_run` is to control the vertical climb of
666 the UAV. Details on the theory behind this operation are documented in
667 the [wiki](https://wiki.paparazziuav.org/wiki/Theory_of_Operation) for
668 the Paparazzi UAV project. The behaviour of this simple controller,
669 supposing that the desired speed is 0.5 meters per second, is plotted in
670 the Figure below.
671 
672 \image html pid.png "The pid controller"
673 
674 ```
675  01: // CONSTANTS:
676  02: #define MAX_CLIMB_SUM_ERR 10
677  03: #define MAX_CLIMB 1
678  04:
679  05: #define CLOCK 16
680  06: #define MAX_PPRZ (CLOCK*600)
681  07:
682  08: #define CLIMB_LEVEL_GAZ 0.31
683  09: #define CLIMB_GAZ_OF_CLIMB 0.75
684  10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
685  11: #define CLIMB_PGAIN -0.03
686  12: #define CLIMB_IGAIN 0.1
687  13:
688  14: const float pitch_of_vz_pgain=CLIMB_PITCH_OF_VZ_PGAIN;
689  15: const float climb_pgain=CLIMB_PGAIN;
690  16: const float climb_igain=CLIMB_IGAIN;
691  17: const float nav_pitch=0;
692  18:
693  19: /** PID function INPUTS */
694  20: // The user input: target speed in vertical direction
695  21: float desired_climb;
696  22: // Vertical speed of the UAV detected by GPS sensor
697  23: float estimator_z_dot;
698  24:
699  25: /** PID function OUTPUTS */
700  26: float desired_gaz;
701  27: float desired_pitch;
702  28:
703  29: /** The state variable: accumulated error in the control */
704  30: float climb_sum_err=0;
705  31:
706  32: /** Computes desired_gaz and desired_pitch */
707  33: void climb_pid_run()
708  34: {
709  35:
710  36: float err=estimator_z_dot-desired_climb;
711  37:
712  38: float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
713  39:
714  40: float pprz=fgaz*MAX_PPRZ;
715  41: desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
716  42:
717  43: /** pitch offset for climb */
718  44: float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
719  45: desired_pitch=nav_pitch+pitch_of_vz;
720  46:
721  47: climb_sum_err=err+climb_sum_err;
722  48: if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
723  49: if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
724  50:
725  51: }
726  52:
727  53: int main()
728  54: {
729  55:
730  56: while(1)
731  57: {
732  58: /** Non-deterministic input values */
733  59: desired_climb=nondet_float();
734  60: estimator_z_dot=nondet_float();
735  61:
736  62: /** Range of input values */
737  63: __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
738  64: __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
739  65:
740  66: __CPROVER_input("desired_climb", desired_climb);
741  67: __CPROVER_input("estimator_z_dot", estimator_z_dot);
742  68:
743  69: climb_pid_run();
744  70:
745  71: __CPROVER_output("desired_gaz", desired_gaz);
746  72: __CPROVER_output("desired_pitch", desired_pitch);
747  73:
748  74: }
749  75:
750  76: return 0;
751  77: }
752 ```
753 
754 In order to test the PID controller, we construct a main control loop,
755 which repeatedly invokes the function `climb_pid_run` (line 69). This
756 PID function has two input variables: the desired speed `desired_climb`
757 and the estimated speed `estimated_z_dot`. In the beginning of each loop
758 iteration, values of the inputs are assigned non-deterministically.
759 Subsequently, the `__CPROVER_assume` statement in lines 63 and 64
760 guarantees that both values are bounded within a valid range. The
761 `__CPROVER_input` and `__CPROVER_output` will help clarify the inputs
762 and outputs of interest for generating test suites.
763 
764 To demonstrate the automatic test suite generation in CBMC, we call the
765 following command and we are going to explain the command line options
766 one by one.
767 
768  cbmc pid.c --cover mcdc --unwind 6 --xml-ui
769 
770 The option `--cover mcdc` specifies the code coverage criterion. There
771 are four conditional statements in the PID function: in line 41, line
772 44, line 48 and line 49. To satisfy MC/DC, the test suite has to meet
773 multiple requirements. For instance, each conditional statement needs to
774 evaluate to *true* and *false*. Consider the condition
775 `"pprz>=0 && pprz<=MAX_PPRZ"` in line 41. CBMC instruments three
776 coverage goals to control the respective evaluated results of
777 `"pprz>=0"` and `"pprz<=MAX_PPRZ"`. We list them in below and they
778 satisfy the MC/DC rules. Note that `MAX_PPRZ` is defined as 16 \* 600 in
779 line 06 of the program.
780 
781  !(pprz >= (float)0) && pprz <= (float)(16 * 600) id="climb_pid_run.coverage.1"
782  pprz >= (float)0 && !(pprz <= (float)(16 * 600)) id="climb_pid_run.coverage.2"
783  pprz >= (float)0 && pprz <= (float)(16 * 600) id="climb_pid_run.coverage.3"
784 
785 The "id" of each coverage goal is automatically assigned by CBMC. For
786 every coverage goal, a test suite (if there exists) that satisfies such
787 a goal is printed out in XML format, as the parameter `--xml-ui` is
788 given. Multiple coverage goals can share a test suite, when the
789 corresponding execution of the program satisfies all these goals at the
790 same time.
791 
792 In the end, the following test suites are automatically generated for
793 testing the PID controller. A test suite consists of a sequence of input
794 parameters that are passed to the PID function `climb_pid_run` at each
795 loop iteration. For example, Test 1 covers the MC/DC goal with
796 id="climb\_pid\_run.coverage.1". The complete output from CBMC is in
797 [pid\_test\_suites.xml](pid_test_suites.xml), where every test suite and
798 the coverage goals it is for are clearly described.
799 
800  Test suite:
801  Test 1.
802  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
803 
804  Test 2.
805  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
806  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
807 
808  Test 3.
809  (iteration 1) desired_climb=0.000000f, estimator_z_dot=-1.000000f
810  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
811 
812  Test 4.
813  (iteration 1) desired_climb=1.000000f, estimator_z_dot=-1.000000f
814  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
815  (iteration 3) desired_climb=1.000000f, estimator_z_dot=-1.000000f
816  (iteration 4) desired_climb=1.000000f, estimator_z_dot=-1.000000f
817  (iteration 5) desired_climb=0.000000f, estimator_z_dot=-1.000000f
818  (iteration 6) desired_climb=1.000000f, estimator_z_dot=-1.000000f
819 
820  Test 5.
821  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
822  (iteration 2) desired_climb=-1.000000f, estimator_z_dot=1.000000f
823  (iteration 3) desired_climb=-1.000000f, estimator_z_dot=1.000000f
824  (iteration 4) desired_climb=-1.000000f, estimator_z_dot=1.000000f
825  (iteration 5) desired_climb=-1.000000f, estimator_z_dot=1.000000f
826  (iteration 6) desired_climb=-1.000000f, estimator_z_dot=1.000000f
827 
828 The option `--unwind 6` unwinds the loop inside the main function body
829 six times. In order to achieve the complete coverage on all the
830 instrumented goals in the PID function `climb_pid_run`, the loop must be
831 unwound sufficient enough times. For example, `climb_pid_run` needs to
832 be called at least six times for evaluating the condition
833 `climb_sum_err>MAX_CLIMB_SUM_ERR` in line 48 to *true*. This corresponds
834 to the Test 5. An introduction to the use of loop unwinding can be found
835 in [Understanding Loop Unwinding](cbmc-loops.shtml).
836 
837 In this small tutorial, we present the automatic test suite generation
838 functionality of CBMC, by applying the MC/DC code coverage criterion to
839 a PID controller case study. In addition to `--cover mcdc`, other
840 coverage criteria like `branch`, `decision`, `path` etc. are also
841 available when calling CBMC.
842 
843 ### Coverage Criteria
844 
845 The table below summarizes the coverage criteria that CBMC supports.
846 
847 Criterion |Definition
848 ----------|----------
849 assertion |For every assertion, generate a test that reaches it
850 location |For every location, generate a test that reaches it
851 branch |Generate a test for every branch outcome
852 decision |Generate a test for both outcomes of every Boolean expression that is not an operand of a propositional connective
853 condition |Generate a test for both outcomes of every Boolean expression
854 mcdc |Modified Condition/Decision Coverage (MC/DC)
855 path |Bounded path coverage
856 cover |Generate a test for every `__CPROVER_cover` statement
857 
858 \section man_modelling Modelling
859 
860 \subsection man_modelling-nondet Nondeterminism
861 
862 ### Rationale
863 
864 Programs typically read inputs from an environment. These inputs can
865 take the form of data read from a file, keyboard or network socket, or
866 arguments passed on the command line. It is usually desirable to analyze
867 the program for any choice of these inputs. In Model Checking, inputs
868 are therefore modeled by means of *nondeterminism*, which means that the
869 value of the input is not specified. The program may follow any
870 computation that results from any choice of inputs.
871 
872 ### Sources of Nondeterminism
873 
874 The CPROVER tools support the following sources of nondeterminism:
875 
876 - functions that read inputs from the environments;
877 - the thread schedule in concurrent programs;
878 - initial values of local-scoped variables and memory allocated with
879  `malloc`;
880 - initial values of variables that are `extern` in all compilation
881  units;
882 - explicit functions for generating nondeterminism.
883 
884 The CPROVER tools are shipped with a number of stubs for the most
885 commonly used library functions. When executing a statement such as
886 `getchar()`, a nondeterministic value is chosen instead of reading a
887 character from the keyboard.
888 
889 When desired, nondeterminism can be introduced explicitly into the
890 program by means of functions that begin with the prefix `nondet_`. As
891 an example, the following function returns a nondeterministically chosen
892 unsigned short int:
893 
894  unsigned short int nondet_ushortint();
895 
896 Note that the body of the function is not defined. The name of the
897 function itself is irrelevant (save for the prefix), but must be unique.
898 Also note that a nondeterministic choice is not to be confused with a
899 probabilistic (or random) choice.
900 
901 ### Uninterpreted Functions
902 
903 It may be necessary to check parts of a program independently.
904 Nondeterminism can be used to over-approximate the behaviour of part of
905 the system which is not being checked. Rather than calling a complex or
906 unrelated function, a nondeterministic stub is used. However, separate
907 calls to the function can return different results, even for the same
908 inputs. If the function output only depends on its inputs then this can
909 introduce spurious errors. To avoid this problem, functions whose names
910 begin with the prefix `__CPROVER_uninterpreted_` are treated as
911 uninterpreted functions. Their value is non-deterministic but different
912 invocations will return the same value if their inputs are the same.
913 Note that uninterpreted functions are not supported by all back-end
914 solvers.
915 
916 \subsection man_modelling-assumptions Modeling with Assertions and Assumptions
917 
918 ### Assertions
919 
920 [Assertions](http://en.wikipedia.org/wiki/Assertion_%28computing%29) are
921 statements within the program that attempt to capture the programmer's
922 intent. The ANSI-C standard defines a header file
923 [assert.h](http://en.wikipedia.org/wiki/Assert.h), which offers a macro
924 `assert(cond)`. When executing a statement such as
925 
926  assert(p!=NULL);
927 
928 the execution is aborted with an error message if the condition
929 evaluates to *false*, i.e., if `p` is NULL in the example above. The
930 CPROVER tools can check the validity of the programmer-annotated
931 assertions statically. Specifically, the CPROVER tools will check that
932 the assertions hold for *any* nondeterministic choice that the program
933 can make. The static assertion checks can be disabled using the
934 `--no-assertions` command line option.
935 
936 In addition, there is a CPROVER-specific way to specify assertions,
937 using the built-in function `__CPROVER_assert`:
938 
939  __CPROVER_assert(p!=NULL, "p is not NULL");
940 
941 The (mandatory) string that is passed as the second argument provides an
942 informal description of the assertion. It is shown in the list of
943 properties together with the condition.
944 
945 The assertion language of the CPROVER tools is identical to the language
946 used for expressions. Note that \ref man_modelling-nondet
947 "nondeterminism"
948 can be exploited in order to check a range of choices. As an example,
949 the following code fragment asserts that **all** elements of the array
950 are zero:
951 
952  int a[100], i;
953 
954  ...
955 
956  i=nondet_uint();
957  if(i>=0 && i<100)
958  assert(a[i]==0);
959 
960 The nondeterministic choice will guess the element of the array that is
961 nonzero. The code fragment above is therefore equivalent to
962 
963  int a[100], i;
964 
965  ...
966 
967  for(i=0; i<100; i++)
968  assert(a[i]==0);
969 
970 Future CPROVER releases will support explicit quantifiers with a syntax
971 that resembles Spec\#:
972 
973  __CPROVER_forall { *type identifier* ; *expression* }
974  __CPROVER_exists { *type identifier* ; *expression* }
975 
976 ### Assumptions
977 
978 Assumptions are used to restrict nondeterministic choices made by the
979 program. As an example, suppose we wish to model a nondeterministic
980 choice that returns a number from 1 to 100. There is no integer type
981 with this range. We therefore use \_\_CPROVER\_assume to restrict the
982 range of a nondeterministically chosen integer:
983 
984  unsigned int nondet_uint();
985 
986  unsigned int one_to_hundred()
987  {
988  unsigned int result=nondet_uint();
989  __CPROVER_assume(result>=1 && result<=100);
990  return result;
991  }
992 
993 The function above returns the desired integer from 1 to 100. You must
994 ensure that the condition given as an assumption is actually satisfiable
995 by some nondeterministic choice, or otherwise the model checking step
996 will pass vacuously.
997 
998 Also note that assumptions are never retroactive: They only affect
999 assertions (or other properties) that follow them in program order. This
1000 is best illustrated with an example. In the following fragment, the
1001 assumption has no effect on the assertion, which means that the
1002 assertion will fail:
1003 
1004  x=nondet_uint();
1005  assert(x==100);
1006  __CPROVER_assume(x==100);
1007 
1008 Assumptions do restrict the search space, but only for assertions that
1009 follow. As an example, the following program will pass:
1010 
1011  int main() {
1012  int x;
1013 
1014  __CPROVER_assume(x>=1 && x<=100000);
1015 
1016  x*=-1;
1017 
1018  __CPROVER_assert(x<0, "x is negative");
1019  }
1020 
1021 Beware that nondeterminism cannot be used to obtain the effect of
1022 universal quantification in assumptions. As an example,
1023 
1024  int main() {
1025  int a[10], x, y;
1026 
1027  x=nondet_int();
1028  y=nondet_int();
1029  __CPROVER_assume(x>=0 && x<10 && y>=0 && y<10);
1030 
1031  __CPROVER_assume(a[x]>=0);
1032 
1033  assert(a[y]>=0);
1034  }
1035 
1036 fails, as there is a choice of x and y which results in a counterexample
1037 (any choice in which x and y are different).
1038 
1039 \subsection man_modelling-pointers Pointer Model
1040 
1041 ### Pointers in C
1042 
1043 C programs (and sometimes C++ programs as well) make intensive use of
1044 pointers in order to decouple program code from specific data. A pointer
1045 variable does not store data such as numbers or letters, but instead
1046 points to a location in memory that hold the relevant data. This section
1047 describes the way the CPROVER tools model pointers.
1048 
1049 ### Objects and Offsets
1050 
1051 The CPROVER tools represent pointers as a pair. The first member of the
1052 pair is the *object* the pointer points to, and the second is the offset
1053 within the object.
1054 
1055 In C, objects are simply continuous fragments of memory (this definition
1056 of "object" is not to be confused with the use of the term in
1057 object-oriented programming). Variables of any type are guaranteed to be
1058 stored as one object, irrespectively of their type. As an example, all
1059 members of a struct or array belong to the same object. CPROVER simply
1060 assigns a number to each active object. The object number of a pointer
1061 `p` can be extracted using the expression `__CPROVER_POINTER_OBJECT(p)`.
1062 As a consequence, pointers to different objects are always different,
1063 which is not sound.
1064 
1065 The offset (the second member of the pair that forms a pointer) is
1066 relative to the beginning of the object; it uses byte granularity. As an
1067 example, the code fragment
1068 
1069  unsigned array[10];
1070  char *p;
1071 
1072  p=(char *)(array+1);
1073  p++;
1074 
1075 will result in a pointer with offset 5. The offset of a pointer `p` can
1076 be extracted using the expression `__CPROVER_POINTER_OFFSET(p)`.
1077 
1078 ### Dereferencing Pointers
1079 
1080 The CPROVER tools require that pointers that are dereferenced point to a
1081 valid object. Assertions that check this requirement can be generated
1082 using the option --pointer-check and, if desired, --bounds-check. These
1083 options will ensure that NULL pointers are not dereferenced, and that
1084 dynamically allocated objects have not yet been deallocated.
1085 
1086 Furthermore, the CPROVER tools check that dynamically allocated memory
1087 is not deallocated twice. The goto-instrument tool is also able to add
1088 checks for memory leaks, i.e., it detects dynamically allocated objects
1089 that are not deallocated once the program terminates.
1090 
1091 The CPROVER tools support pointer typecasts. Most casts are supported,
1092 with the following exceptions:
1093 
1094 1. One notable exception is that pointers can only be accessed using a
1095  pointer type. The conversion of a pointer into an integer-type using
1096  a pointer typecast is not supported.
1097 
1098 2. Casts from integers to pointers yield a pointer that is either NULL
1099  (if the integer is zero) or that point into a special array for
1100  modeling [memory-mapped
1101  I/O](http://en.wikipedia.org/wiki/Memory-mapped_I/O). Such pointers
1102  are assumed not to overlap with any other objects. This is, of
1103  course, only sound if a corresponding range check is instrumented.
1104 
1105 3. Accesses to arrays via pointers that have the array subtype need to
1106  be well-aligned.
1107 
1108 ### Pointers in Open Programs
1109 
1110 It is frequently desired to validate an open program, i.e., a fragment
1111 of a program. Some variables are left undefined. In case an undefined
1112 pointer is dereferenced, CBMC assumes that the pointer points to a
1113 separate object of appropriate type with unbounded size. The object is
1114 assumed not to alias with any other object. This assumption may
1115 obviously be wrong in specific extensions of the program.
1116 
1117 \subsection man_modelling-floating-point Floating Point
1118 
1119 The CPROVER tools support bit-accurate reasoning about IEEE-754
1120 floating-point and fixed-point arithmetic. The C standard contains a
1121 number of areas of implementation-defined behaviour with regard to
1122 floating-point arithmetic:
1123 
1124 - CPROVER supports C99 Appendix F, and thus, the `__STD_IEC_559__`
1125  macro is defined. This means that the C `float` data type maps to
1126  IEEE 754 `binary32` and `double` maps to `binary64` and operations
1127  on them are as specified in IEEE 754.
1128 
1129 - `long double` can be configured to be `binary64`, `binary128`
1130  (quad precision) or a 96 bit type with 15 exponent bits and 80
1131  significant bits. The last is an approximation of Intel's x87
1132  extended precision double data type. As the C standard allows a
1133  implementations a fairly wide set of options for `long double`, it
1134  is best avoided for both portable code and bit-precise analysis. The
1135  default is to match the build architecture as closely as possible.
1136 
1137 - In CPROVER, floating-point expressions are evaluated at the 'natural
1138  precision' (the greatest of the arguments) and not at a
1139  higher precision. This corresponds to `FLT_EVAL_METHOD` set to `0`.
1140  Note that this is a different policy to some platforms (see below).
1141 
1142 - Expression contraction (for example, converting `x * y + c` to
1143  `fma(x,y,c)`) is not performed. In effect, the `FP_CONTRACT` pragma
1144  is always off.
1145 
1146 - Constant expressions are evaluated at \`run' time wherever possible
1147  and so will respect changes in the rounding mode. In effect, the
1148  `FENV_ACCESS` pragma is always off. Note that floating point
1149  constants are treated as doubles (unless they are followed by `f`
1150  when they are float) as specified in the C standard. `goto-cc`
1151  supports `-fsingle-precision-constant`, which allows
1152  the (non-standard) treatment of constants as floats.
1153 
1154 - Casts from int to float and float to float make use of the current
1155  rounding mode. Note that the standard requires that casts from float
1156  to int use round-to-zero (i.e. truncation).
1157 
1158 ### x86 and Other Platform-specific Issues
1159 
1160 Not all platforms have the same implementation-defined behaviour as
1161 CPROVER. This can cause mismatches between the verification environment
1162 and the execution environment. If this occurs, check the compiler manual
1163 for the choices listed above. There are two common cases that can cause
1164 these problems: 32-bit x86 code and the use of unsafe optimisations.
1165 
1166 Many compilers that target 32-bit x86 platforms employ a different
1167 evaluation method. The extended precision format of the x87 unit is used
1168 for all computations regardless of their native precision. Most of the
1169 time, this results in more accurate results and avoids edge cases.
1170 However, it can result in some obscure and difficult to debug behaviour.
1171 Checking if the `FLT_EVAL_METHOD` macro is non-zero (for these platforms
1172 it will typically be 2), should warn of these problems. Changing the
1173 compiler flags to use the SSE registers will resolve many of them, give
1174 a more standards-compliant platform and will likely perform better. Thus
1175 it is *highly* recommended. Use `-msse2 -mfpmath=sse` to enable this
1176 option for GCC. Visual C++ does not have an option to force the
1177 exclusive use of SSE instructions, but `/arch:SSE2` will pick SSE
1178 instructions "when it \[the compiler\] determines that it is faster to
1179 use the SSE/SSE2 instructions" and is thus better than `/arch:IA32`,
1180 which exclusively uses the x87 unit.
1181 
1182 The other common cause of discrepancy between CPROVER results and the
1183 actual platform are the use of unsafe optimisations. Some higher
1184 optimisation levels enable transformations that are unsound with respect
1185 to the IEEE-754 standard. Consult the compiler manual and disable any
1186 optimisations that are described as unsafe (for example, the GCC options
1187 `-ffast-math`). The options `-ffp-contract=off` (which replaces
1188 `-mno-fused-madd`), `-frounding-math` and `-fsignaling-nans` are needed
1189 for GCC to be strictly compliant with IEEE-754.
1190 
1191 ### Rounding Mode
1192 
1193 CPROVER supports the four rounding modes given by IEEE-754 1985; round
1194 to nearest (ties to even), round up, round down and round towards zero.
1195 By default, round to nearest is used. However, command line options
1196 (`--round-to-zero`, etc.) can be used to over-ride this. If more control
1197 is needed, CPROVER has models of `fesetround` (for POSIX systems) and
1198 `_controlfp` (for Windows), which can be used to change the rounding
1199 mode during program execution. Furthermore, the inline assembly commands
1200 fstcw/fnstcw/fldcw (on x86) can be used.
1201 
1202 The rounding mode is stored in the (thread local) variable
1203 `__CPROVER_rounding_mode`, but users are strongly advised not to use
1204 this directly.
1205 
1206 ### Math Library
1207 
1208 CPROVER implements some of `math.h`, including `fabs`, `fpclassify` and
1209 `signbit`. It has very limited support for elementary functions. Care
1210 must be taken when verifying properties that are dependent on these
1211 functions as the accuracy of implementations can vary considerably. The
1212 C compilers can (and many do) say that the accuracy of these functions
1213 is unknown.
1214 
1215 ### Fixed-point Arithmetic
1216 
1217 CPROVER also has support for fixed-point types. The `--fixedbv` flag
1218 switches `float`, `double` and `long double` to fixed-point types. The
1219 length of these types is platform specific. The upper half of each type
1220 is the integer component and the lower half is the fractional part.
1221 
1222 
1223 \section man_hard-soft Hardware and Software Equivalence and Co-Verification
1224 
1225 \subsection man_hard-soft-introduction Introduction
1226 
1227 A common hardware design approach employed by many companies is to first
1228 write a quick prototype that behaves like the planned circuit in a
1229 language like ANSI-C. This program is then used for extensive testing
1230 and debugging, in particular of any embedded software that will later on
1231 be shipped with the circuit. An example is the hardware of a cell phone
1232 and its software. After testing and debugging of the program, the actual
1233 hardware design is written using hardware description languages like
1234 [VHDL](http://en.wikipedia.org/wiki/VHDL) or
1235 [Verilog](http://en.wikipedia.org/wiki/Verilog).
1236 
1237 Thus, there are two implementations of the same design: one written in
1238 ANSI-C, which is written for simulation, and one written in register
1239 transfer level HDL, which is the actual product. The ANSI-C
1240 implementation is usually thoroughly tested and debugged.
1241 
1242 Due to market constraints, companies aim to sell the chip as soon as
1243 possible, i.e., shortly after the HDL implementation is designed. There
1244 is usually little time for additional debugging and testing of the HDL
1245 implementation. Thus, an automated, or nearly automated way of
1246 establishing the consistency of the HDL implementation is highly
1247 desirable.
1248 
1249 This motivates the verification problem: we want to verify the
1250 consistency of the HDL implementation, i.e., the product, [using the
1251 ANSI-C implementation as a
1252 reference](http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=936243&userType=inst).
1253 Es­ta­bli­shing the consistency does not re­quire a formal
1254 specification. However, formal methods to verify either the hardware or
1255 software design are still desirable.
1256 
1257 ### Related Work
1258 
1259 There have been several attempts in the past to tackle the problem.
1260 [Semeria et al.](http://portal.acm.org/citation.cfm?id=513951) describe
1261 a tool for verifying the combinational equivalence of RTL-C and an HDL.
1262 They translate the C code into HDL and use standard equivalence checkers
1263 to establish the equivalence. The C code has to be very close to a
1264 hardware description (RTL level), which implies that the source and
1265 target have to be implemented in a very similar way. There are also
1266 variants of C specifically for this purpose. The [SystemC
1267 standard](http://en.wikipedia.org/wiki/SystemC) defines a subset of C++
1268 that can be used for synthesis. Further variants of ANSI-C for
1269 specifying hardware are SpecC and Handel C, among others.
1270 
1271 The concept of verifying the equivalence of a software implementation
1272 and a synchronous transition system was introduced by [Pnueli, Siegel,
1273 and Shtrichman](http://www.springerlink.com/content/ah5lpxaagrjp8ax2/).
1274 The C program is re­quired to be in a very specific form, since a
1275 mechanical translation is assumed.
1276 
1277 In 2000, [Currie, Hu, and
1278 Rajan](http://doi.acm.org/10.1145/337292.337339) transform DSP assembly
1279 language into an equation for the Stanford Validity Checker. The
1280 symbolic execution of programs for comparison with RTL is now common
1281 practice.
1282 
1283 The previous work focuses on a small subset of ANSI-C that is
1284 particularly close to register transfer language. Thus, the designer is
1285 often re­quired to rewrite the C program manually in order to comply
1286 with these constraints. We extend the methodology to handle the full set
1287 of ANSI-C language features. This is a challenge in the presence of
1288 complex, dynamic data structures and pointers that may dynamically point
1289 to multiple objects. Furthermore, our methodology allows arbitrary loop
1290 constructs.
1291 
1292 ### Further Material
1293 
1294 We provide a small \ref man_hard-soft-tutorial "tutorial" and a
1295 description on
1296 \ref man_hard-soft-inputs "how to synchronize inputs between the C model and the Verilog model".
1297 There is also a collection of
1298 [benchmark problems](http://www.cprover.org/hardware/sequential-equivalence/)
1299 available.
1300 
1301 Further Reading
1302 
1303 - [Hardware Verification using ANSI-C Programs as a
1304  Reference](http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html)
1305 - [Behavioral Consistency of C and Verilog Programs Using Bounded
1306  Model Checking](http://www-2.cs.cmu.edu/~svc/papers/view-publications-cky03.html)
1307 - [A Tool for Checking ANSI-C
1308  Programs](http://www-2.cs.cmu.edu/~svc/papers/view-publications-ckl2004.html)
1309 - [Checking Consistency of C and Verilog using Predicate Abstraction
1310  and Induction](http://www.kroening.com/publications/view-publications-kc2004.html)
1311 
1312 
1313 \subsection man_hard-soft-tutorial Tutorial
1314 
1315 ### Verilog vs. ANSI-C
1316 
1317 We assume that CBMC is installed on your system. If not so, follow
1318 \ref man_install-cbmc "these instructions".
1319 
1320 The following Verilog module implements a 4-bit counter
1321 (counter.v):
1322 
1323  module top(input clk);
1324 
1325  reg [3:0] counter;
1326 
1327  initial counter=0;
1328 
1329  always @(posedge clk)
1330  counter=counter+1;
1331 
1332  endmodule
1333 
1334 HW-CBMC can take Verilog modules as the one above as additional input.
1335 Similar as in co-simulation, the data in the Verilog modules is
1336 available to the C program by means of global variables. For the example
1337 above, the following C fragment shows the definition of the variable
1338 that holds the value of the `counter` register:
1339 
1340  struct module_top {
1341  unsigned int counter;
1342  };
1343 
1344  extern struct module_top top;
1345 
1346 Using this definition, the value of the `counter` register in the
1347 Verilog fragment above can be accessed as `top.counter`. Please note
1348 that the name of the variable **must** match the name of the top module.
1349 The C program only has a view of one state of the Verilog model. The
1350 Verilog model makes a transition once the function `next_timeframe()` is
1351 called.
1352 
1353 As CBMC performs Bounded Model Checking, the number of timeframes
1354 available for analysis must be bounded (SATABS). As it is desirable to
1355 change the bound to adjust it to the available computing capacity, the
1356 bound is given on the command line and not as part of the C program.
1357 This makes it easy to use only one C program for arbitrary bounds. The
1358 actual bound is available in the C program using the following
1359 declaration:
1360 
1361  extern const unsigned int bound;
1362 
1363 Also note that the fragment above declares a constant variable of struct
1364 type. Thus, the C program can only read the trace values and is not able
1365 to modify them. We will later on describe how to drive inputs of the
1366 Verilog module from within the C program.
1367 
1368 As described in previous chapters, assertions can be used to verify
1369 properties of the Verilog trace. As an example, the following program
1370 checks two values of the trace of the counter module (counter.c):
1371 
1372  void next_timeframe();
1373 
1374  struct module_top {
1375  unsigned int counter;
1376  };
1377 
1378  extern struct module_top top;
1379 
1380  int main() {
1381  next_timeframe();
1382  next_timeframe();
1383  assert(top.counter==2);
1384  next_timeframe();
1385  assert(top.counter==3);
1386  }
1387 
1388 The following CBMC command line checks these assertions with a bound of
1389 20:
1390 
1391  hw-cbmc counter.c counter.v --module top --bound 20
1392 
1393 Note that a specific version of CBMC is used, called `hw-cbmc`. The
1394 module name given must match the name of the module in the Verilog file.
1395 Multiple Verilog files can be given on the command line.
1396 
1397 The `--bound` parameter is not to be confused with the `--unwind`
1398 parameter. While the `--unwind` parameter specifies the maximum
1399 unwinding depth for loops within the C program, the `--bound` parameter
1400 specifies the number of times the transition relation of the Verilog
1401 module is to be unwound.
1402 
1403 ### Counterexamples
1404 
1405 For the given example, the verification is successful. If the first
1406 assertion is changed to
1407 
1408  assert(top.counter==10);
1409 
1410 and the bound on the command line is changed to 6, CBMC will produce a
1411 counterexample. CBMC produces two traces: One for the C program, which
1412 matches the traces described earlier, and a separate trace for the
1413 Verilog module. The values of the registers in the Verilog module are
1414 also shown in the C trace as part of the initial state.
1415 
1416  Initial State
1417  ----------------------------------------------------
1418  bound=6 (00000000000000000000000000000110)
1419  counter={ 0, 1, 2, 3, 4, 5, 6 }
1420 
1421  Failed assertion: assertion line 6 function main
1422 
1423  Transition system state 0
1424  ----------------------------------------------------
1425  counter=0 (0000)
1426 
1427  Transition system state 1
1428  ----------------------------------------------------
1429  counter=1 (0001)
1430 
1431  Transition system state 2
1432  ----------------------------------------------------
1433  counter=2 (0010)
1434 
1435  Transition system state 3
1436  ----------------------------------------------------
1437  counter=3 (0011)
1438 
1439  Transition system state 4
1440  ----------------------------------------------------
1441  counter=4 (0100)
1442 
1443  Transition system state 5
1444  ----------------------------------------------------
1445  counter=5 (0101)
1446 
1447  Transition system state 6
1448  ----------------------------------------------------
1449  counter=6 (0110)
1450 
1451 ### Using the Bound
1452 
1453 The following program is using the bound variable to check the counter
1454 value in all cycles:
1455 
1456  void next_timeframe();
1457  extern const unsigned int bound;
1458 
1459  struct module_top {
1460  unsigned int counter;
1461  };
1462 
1463  extern struct module_top top;
1464 
1465  int main() {
1466  unsigned cycle;
1467 
1468  for(cycle=0; cycle<bound; cycle++) {
1469  assert(top.counter==(cycle & 15));
1470  next_timeframe();
1471  }
1472  }
1473 
1474 CBMC performs bounds checking, and restricts the number of times that
1475 `next_timeframe()` can be called. SATABS does not re­quire a bound, and
1476 thus, `next_timeframe()` can be called arbitrarily many times.
1477 
1478 
1479 \subsection man_hard-soft-mapping Mapping Variables
1480 
1481 ### Mapping Variables within the Module Hierarchy
1482 
1483 Verilog modules are hierarchical. The `extern` declarations shown above
1484 only allow reading the values of signals and registers that are in the
1485 top module. In order to read values from sub-modules, CBMC uses
1486 structures.
1487 
1488 As an example, consider the following Verilog file
1489 (heirarchy.v):
1490 
1491  module counter(input clk, input [7:0] increment);
1492 
1493  reg [7:0] counter;
1494 
1495  initial counter=0;
1496 
1497  always @(posedge clk)
1498  counter=counter+increment;
1499 
1500  endmodule
1501 
1502  module top(input clk);
1503 
1504  counter c1(clk, 1);
1505  counter c2(clk, 2);
1506 
1507  endmodule
1508 
1509 The file has two modules: a top module and a counter module. The counter
1510 module is instantiated twice within the top module. A reference to the
1511 register `counter` within the C program would be ambiguous, as the two
1512 module instances have separate instances of the register. CBMC and
1513 SATABS use the following data structures for this example:
1514 
1515  void next_timeframe();
1516  extern const unsigned int bound;
1517 
1518  struct counter {
1519  unsigned char increment;
1520  unsigned char counter;
1521  };
1522 
1523  struct module_top {
1524  struct module_counter c1, c2;
1525  };
1526 
1527  extern struct module_top top;
1528 
1529  int main() {
1530  next_timeframe();
1531  next_timeframe();
1532  next_timeframe();
1533  assert(top.c1.counter==3);
1534  assert(top.c2.counter==6);
1535  }
1536 
1537 The `main` function reads both counter values for cycle 3. A deeper
1538 hierarchy (modules in modules) is realized by using additional structure
1539 members. Writing these data structures for large Verilog designs is
1540 error prone, and thus, HW-CBMC can generate them automatically. The
1541 declarations above are generated using the command line
1542 
1543  hw-cbmc --gen-interface --module top hierarchy.v
1544 
1545 ### Mapping Verilog Vectors to Arrays or Scalars
1546 
1547 In Verilog, a definition such as
1548 
1549  wire [31:0] x;
1550 
1551 can be used for arithmetic (as in `x+10`) and as array of Booleans (as
1552 in `x[2]`). ANSI-C does not allow both, so when mapping variables from
1553 Verilog to C, the user has to choose one option for each such variable.
1554 As an example, the C declaration
1555 
1556  unsigned int x;
1557 
1558 will allow using `x` in arithmetic expressions, while the C declaration
1559 
1560  __CPROVER_bool x[32];
1561 
1562 will allow accessing the individual bits of `x` using the syntax
1563 `x[bit]`. The `--gen-interface` option of HW-CBMC will generate the
1564 first variant if the vector has the same size as one of the standard
1565 integer types, and will use the `__CPROVER_bitvector[]` type if not
1566 so. This choice can be changed by adjusting the declaration accordingly.
1567 Note that both SpecC and SystemC offer bit-extraction operators, which
1568 means that it unnecessary to use the declaration as array in order to
1569 access individual bits of a vector.
1570 
1571 \subsection man_hard-soft-inputs Synchronizing Inputs
1572 
1573 ### Driving Primary Inputs
1574 
1575 The examples in the \ref man_hard-soft-tutorial "tutorial" are trivial
1576 in the sense that the model has only one possible trace. The initial
1577 state is deterministic, and there is only one possible transition, so
1578 the verification problem can be solved by testing a single run. In
1579 contrast, consider the following Verilog module:
1580 
1581  module top(input clk, input i);
1582 
1583  reg [3:0] counter;
1584 
1585  initial counter=0;
1586 
1587  always @(posedge clk)
1588  if(i)
1589  counter=counter+1;
1590 
1591  endmodule
1592 
1593 The module above has an input named `i`. The top-level inputs of the
1594 Verilog design have to be generated by the C program. This is done by
1595 assigning the desired values to the corresponding struct member, and
1596 then calling the `set_inputs()` function before calling
1597 `next_timeframe()`. Consider the following example:
1598 
1599  void next_timeframe();
1600  void set_inputs();
1601  extern const unsigned int bound;
1602 
1603  struct module_top {
1604  unsigned int counter;
1605  _Bool i;
1606  };
1607 
1608  extern struct module_top top;
1609 
1610  int main() {
1611  assert(top.counter==0);
1612 
1613  top.i=1;
1614  set_inputs(); next_timeframe();
1615  assert(top.counter==1);
1616 
1617  top.i=1;
1618  set_inputs(); next_timeframe();
1619  assert(top.counter==2);
1620 
1621  top.i=0;
1622  set_inputs(); next_timeframe();
1623  assert(top.counter==2);
1624  }
1625 
1626 As an example, consider a Verilog module that has a signal `reset` as an
1627 input, which is active-low. The following C fragment drives this input
1628 to be active in the first cycle, and not active in any subsequent cycle:
1629 
1630  top.resetn=0;
1631  set_inputs(); next_timeframe();
1632 
1633  for(i=1; i<bound; i++) {
1634  top.resetn=1;
1635  set_inputs(); next_timeframe();
1636  }
1637 
1638 Note that the value of the input must be set *before* calling
1639 `next_timeframe()`. The effect of the input values on values derived in
1640 a combinatorial way is immediately visible. The effect on clocked values
1641 becomes visible in the next time frame.
1642 
1643 ### Using Nondeterminism
1644 
1645 The examples above use particular, constant values to drive the primary
1646 inputs. In order to check the behavior of the Verilog model for more
1647 than one specific input, use \ref man_modelling-nondet "nondeterminism".
1648 
1649 
1650 \section man_instrumentation Build Systems, Libraries, and Instrumentation
1651 
1652 \subsection man_instrumentation-libraries Build Systems and Libraries
1653 
1654 ### The Problem
1655 
1656 Similar to unit testing, the model checking approach requires the user
1657 to clearly define what parts of the program should be tested and what
1658 the behaviour of these parts is. This requirement has following reasons:
1659 
1660 - Despite recent advances, the size of the programs that model
1661  checkers can cope with is still restricted.
1662 
1663 - Typically, you want to verify *your* program and not the libraries
1664  or the operating that it uses (the correctness of these libraries
1665  and the OS us usually addressed separately).
1666 
1667 - CBMC and SATABS cannot verify binary libraries.
1668 
1669 - CBMC and SATABS does not provide a model for the hardware (e.g.,
1670  hard disk, input/output devices) the tested program runs on. Since
1671  CBMC and SATABS are supposed to examine the behavior of the tested
1672  program for **all** possible inputs and outputs, it is reasonable to
1673  model input and output by means of non-deterministic choice.
1674 
1675 ### Further Reading
1676 
1677 Existing software projects usually do not come in a single source file
1678 that may simply be passed to a model checker, but is a collection of
1679 files held together by a build system. The extraction of models from
1680 such a build system using goto-cc is described
1681 \ref man_instrumentation-goto-cc "here".
1682 
1683 \subsection man_instrumentation-goto-cc Integration into Build Systems with goto-cc
1684 
1685 Existing software projects usually do not come in a single source file
1686 that may simply be passed to a model checker. They rather come in a
1687 multitude of source files in different directories and refer to external
1688 libraries and system-wide options. A *build system* then collects the
1689 configuration options from the system and compiles the software
1690 according to build rules.
1691 
1692 The most prevalent build tool on Unix (-based) systems surely is the
1693 `make` utility. This tool uses build rules given in a *Makefile* that
1694 comes with the software sources. Running software verification tools on
1695 projects like these is greatly simplified by a compiler that first
1696 collects all the necessary models into a single model file.
1697 [goto-cc](http://www.cprover.org/goto-cc/) is such a model file
1698 extractor, which can seamlessly replace `gcc` and `cl.exe` in Makefiles.
1699 The normal build system for the project may be used to build the
1700 software, but the outcome will be a model file with suitable detail for
1701 verification, as opposed to a flat executable program. Note that goto-cc
1702 comes in different variants depending on the compilation environment.
1703 These variants are described [here](goto-cc-variants.shtml).
1704 
1705 ### Example: Building wu-ftpd
1706 
1707 This example assumes a Unix-like machine.
1708 
1709 1. Download the sources of wu-ftpd from
1710  [here](ftp://ftp.wu-ftpd.org/pub/wu-ftpd/wu-ftpd-current.tar.gz).
1711 
1712 2. Unpack the sources by running ` tar xfz wu-ftpd-current.tar.gz`
1713 
1714 3. Change to the source directory, by entering, e.g.,
1715  `cd wu-ftpd-2.6.2`
1716 
1717 4. Configure the project for verification by running
1718 
1719  `./configure YACC=byacc CC=goto-cc --host=none-none-none`
1720 
1721 5. Build the project by running `make`. This creates multiple model
1722  files in the `src` directory. Among them is a model for the main
1723  executable `ftpd`.
1724 
1725 6. Run a model-checker, e.g., CBMC, on the model file:
1726 
1727  `cbmc src/ftpd`
1728 
1729  CBMC automatically recognizes that the file is a goto binary.
1730 
1731 ### Important Notes
1732 
1733 More elaborate build or configuration scripts often make use of features
1734 of the compiler or the system library to detect configuration options
1735 automatically, e.g., in a `configure` script. Replacing `gcc` by goto-cc
1736 at this stage may confuse the script, or detect wrong options. For
1737 example, missing library functions do not cause goto-cc to throw an
1738 error (only to issue a warning). Because of this, configuration scripts
1739 sometimes falsely assume the availability of a system function or
1740 library.
1741 
1742 In the case of this or similar problems, it is more advisable to
1743 configure the project using the normal routine, and replacing the
1744 compiler setting manually in the generated Makefiles, e.g., by replacing
1745 lines like `CC=gcc` by `CC=goto-cc`.
1746 
1747 A helpful command that accomplishes this task successfully for many
1748 projects is the following:
1749 
1750  for i in `find . -name Makefile`; do sed -e 's/^\(\s*CC[ \t]*=\)\(.*$\)/\1goto-cc/g' -i $i done
1751 
1752 Here are additional examples on how to use goto-cc:
1753 
1754 - \ref man_goto-cc-linux "Linux Kernel"
1755 - \ref man_goto-cc-apache "Apache HTTPD"
1756 
1757 A description of how to integrate goto-cc into Microsoft's Visual Studio
1758 is \ref man_instrumentation-vs "here".
1759 
1760 ### Linking Libraries
1761 
1762 Some software projects come with their own libraries; also, the goal may
1763 be to analyze a library by itself. For this purpose it is possible to
1764 use goto-cc to link multiple model files into a library of model files.
1765 An object file can then be linked against this model library. For this
1766 purpose, goto-cc also features a linker mode.
1767 
1768 To enable this linker mode, create a link to the goto-cc binary by the
1769 name of goto-ld (Linux and Mac) or copy the goto-cc binary to
1770 goto-link.exe (Windows). The goto-ld tool can now be used as a seamless
1771 replacement for the `ld` tool present on most Unix (-based) systems and
1772 for the `link` tool on Windows.
1773 
1774 The default linker may need to be replaced by `goto-ld` or
1775 `goto-link.exe` in the build script, which can be achieved in much the
1776 same way as replacing the compiler.
1777 
1778 
1779 \subsection man_instrumentation-vs Integration into Visual Studio 2008 to 2012
1780 
1781 Visual Studio version 2008 onwards comes with a new XML-based build
1782 system called
1783 [MSBuild](http://msdn.microsoft.com/en-us/library/ms171452.aspx).
1784 The MSBuild system is also activated when triggering a build from the
1785 Visual Studio GUI. The project files created by the Visual Studio GUI
1786 are used as input by the MSBuild tool.
1787 
1788 The MSBuild system can be used to generate goto-binaries from your
1789 Visual Studio project as follows:
1790 
1791 1. Install the `goto-cl.exe` and `goto-link.exe` binaries in some
1792  directory that is contained in the PATH environment variable.
1793 
1794 2. Add a configuration for the goto-cc build for your project in the
1795  configuration manager, named "goto-cc".
1796 
1797 3. Open the Visual Studio Command Prompt (in the Tools menu).
1798 
1799 4. Locate the directory that contains the project. Change into this
1800  directory using "CD".
1801 
1802 5. Type
1803 
1804  msbuild /p:CLToolExe=goto-cl.exe /p:LinkToolExe=goto-link.exe /p:Flavor=goto-cc /p:Platform=x86
1805 
1806  The platform can be adjusted as required; the "Flavor" given should
1807  match the configuration that was created earlier.
1808 
1809 Note that the recent versions of goto-cc also support file names with
1810 non-ASCII (Unicode) characters on Windows platforms.
1811 
1812 \subsection man_instrumentation-goto-cc-variants Variants of goto-cc
1813 
1814 The goto-cc utility comes in several variants, summarised in the
1815 following table.
1816 
1817 Executable | Environment | Preprocessor
1818 --------------|-------------------------------------------------------------------------|-------
1819  goto-cc | [gcc](http://gcc.gnu.org/) (control-flow graph only) | gcc -E
1820  goto-gcc | [gcc](http://gcc.gnu.org/) ("hybrid" executable) | gcc -E
1821  goto-armcc | [ARM RVDS](http://arm.com/products/tools/software-tools/rvds/index.php) | armcc -E
1822  goto-cl | [Visual Studio](http://www.microsoft.com/visualstudio/) | cl /E
1823  goto-cw | [Freescale CodeWarrior](http://www.freescale.com/webapp/sps/site/homepage.jsp?code=CW_HOME) | mwcceppc
1824 
1825 The primary difference between the variants is the preprocessor called.
1826 Furthermore, the language recognized varies slightly. The variants can
1827 be obtained by simply renaming the goto-cc executable. On Linux/MacOS,
1828 the variants can be obtained by creating a symbolic link.
1829 
1830 The "hybrid" executables contain both the control-flow graph for
1831 verification purposes and the usual, executable machine code.
1832 
1833 \subsection man_instrumentation-architecture Architectural Settings
1834 
1835 The behavior of a C/C++ program depends on a number of parameters that
1836 are specific to the architecture the program was compiled for. The three
1837 most important architectural parameters are:
1838 
1839 - The width of the various scalar types; e.g., compare the value of
1840  `sizeof(long int)` on various machines.
1841 - The width of pointers; e.g., compare the value of `sizeof(int *)` on
1842  various machines.
1843 - The [endianness](http://en.wikipedia.org/wiki/Endianness) of
1844  the architecture.
1845 
1846 In general, the CPROVER tools attempt to adopt the settings of the
1847 particular architecture the tool itself was compiled for. For example,
1848 when running a 64 bit binary of CBMC on Linux, the program will be
1849 processed assuming that `sizeof(long int)==8`.
1850 
1851 As a consequence of these architectural parameters, you may observe
1852 different verification results for an identical program when running
1853 CBMC on different machines. In order to get consistent results, or when
1854 aiming at validating a program written for a different platform, the
1855 following command-line arguments can be passed to the CPROVER tools:
1856 
1857 - The word-width can be set with `--16`, `--32`, `--64`.
1858 - The endianness can be defined with `--little-endian` and
1859  `--big-endian`.
1860 
1861 When using a goto binary, CBMC and the other tools read the
1862 configuration from the binary, i.e., the setting when running goto-cc is
1863 the one that matters; the option given to the model checker is ignored
1864 in this case.
1865 
1866 In order to see the effect of the options `--16`, `--32` and `--64`,
1867 pass the following program to CBMC:
1868 
1869  #include <stdio.h>
1870  #include <assert.h>
1871 
1872  int main() {
1873  printf("sizeof(long int): %d\n", (int)sizeof(long int));
1874  printf("sizeof(int *): %d\n", (int)sizeof(int *));
1875  assert(0);
1876  }
1877 
1878 The counterexample trace contains the strings printed by the `printf`
1879 command.
1880 
1881 The effects of endianness are more subtle. Try the following program
1882 with `--big-endian` and `--little-endian`:
1883 
1884  #include <stdio.h>
1885  #include <assert.h>
1886 
1887  int main() {
1888  int i=0x01020304;
1889  char *p=(char *)&i;
1890  printf("Bytes of i: %d, %d, %d, %d\n", p[0], p[1], p[2], p[3]);
1891  assert(0);
1892  }
1893 
1894 
1895 \subsection man_instrumentation-properties Property Instrumentation
1896 
1897 ### Properties
1898 
1899 We have mentioned *properties* several times so far, but we never
1900 explained *what* kind of properties CBMC and SATABS can verify. We cover
1901 this topic in more detail in this section.
1902 
1903 Both CBMC and SATABS use
1904 [assertions](http://en.wikipedia.org/wiki/Assertion_(computing)) to
1905 specify program properties. Assertions are properties of the state of
1906 the program when the program reaches a particular program location.
1907 Assertions are often written by the programmer by means of the `assert`
1908 macro.
1909 
1910 In addition to the assertions written by the programmer, assertions for
1911 specific properties can also be generated automatically by CBMC and
1912 SATABS, often relieving the programmer from writing "obvious"
1913 assertions.
1914 
1915 CBMC and SATABS come with an assertion generator called
1916 `goto-instrument`, which performs a conservative [static
1917 analysis](http://en.wikipedia.org/wiki/Static_code_analysis) to
1918 determine program locations that potentially contain a bug. Due to the
1919 imprecision of the static analysis, it is important to emphasize that
1920 these generated assertions are only *potential* bugs, and that the Model
1921 Checker first needs to confirm that they are indeed genuine bugs.
1922 
1923 The assertion generator can generate assertions for the verification of
1924 the following properties:
1925 
1926 - **Buffer overflows.** For each array access, check whether the upper
1927  and lower bounds are violated.
1928 - **Pointer safety.** Search for `NULL`-pointer dereferences or
1929  dereferences of other invalid pointers.
1930 
1931 - **Division by zero.** Check whether there is a division by zero in
1932  the program.
1933 
1934 - **Not-a-Number.** Check whether floating-point computation may
1935  result in [NaNs](http://en.wikipedia.org/wiki/NaN).
1936 
1937 - **Unitialized local.** Check whether the program uses an
1938  uninitialized local variable.
1939 
1940 - **Data race.** Check whether a concurrent program accesses a shared
1941  variable at the same time in two threads.
1942 
1943 We refrain from explaining the properties above in detail. Most of them
1944 relate to behaviors that are left undefined by the respective language
1945 semantics. For a discussion on why these behaviors are usually very
1946 undesirable, read [this](http://blog.regehr.org/archives/213) blog post
1947 by John Regehr.
1948 
1949 All the properties described above are *reachability* properties. They
1950 are always of the form
1951 
1952 "*Is there a path through the program such that property ... is
1953 violated?*"
1954 
1955 The counterexamples to such properties are always program paths. Users
1956 of the Eclipse plugin can step through these counterexamples in a way
1957 that is similar to debugging programs. The installation of this plugin
1958 is explained \ref man_install-eclipse "here".
1959 
1960 ### Using goto-instrument
1961 
1962 The goto-instrument static analyzer operates on goto-binaries, which is
1963 a binary representation of control-flow graphs. The goto-binary is
1964 extracted from program source code using goto-cc, which is explained
1965 \ref man_instrumentation-goto-cc "here". Given a goto-program,
1966 goto-instrument operates as follows:
1967 
1968 1. A goto-binary is read in.
1969 2. The specified static analyses are performed.
1970 3. Any potential bugs found are transformed into corresponding
1971  assertions, and are added into the program.
1972 4. A new goto-binary (with assertions) is written to disc.
1973 
1974 As an example, we begin with small C program we call `expr.c` (taken
1975 from [here](http://www.spinroot.com/uno/)):
1976 
1977  int *ptr;
1978 
1979  int main(void) {
1980  if (ptr)
1981  *ptr = 0;
1982  if (!ptr)
1983  *ptr = 1;
1984  }
1985 
1986 The program contains an obvious NULL-pointer dereference. We first
1987 compile the example program with goto-cc and then instrument the
1988 resulting goto-binary with pointer checks.
1989 
1990  goto-cc expr.c -o in.gb goto-instrument in.gb out.gb --pointer-check
1991 
1992 We can now get a list of the assertions that have been generated as
1993 follows:
1994 
1995  goto-instrument out.gb --show-properties
1996 
1997 Using either CBMC or SATABS on `out.gb`, we can obtain a counterexample
1998 trace for the NULL-pointer dereference:
1999 
2000  cbmc out.gb
2001 
2002 The goto-instrument program supports the following checks:
2003 
2004 Flag | Check
2005 -----------------------------|----------------------------------------------
2006 `--no-assertions` | ignore user assertions
2007 `--bounds-check` | add array bounds checks
2008 `--div-by-zero-check` | add division by zero checks
2009 `--pointer-check` | add pointer checks
2010 `--signed-overflow-check` | add arithmetic over- and underflow checks
2011 `--unsigned-overflow-check` | add arithmetic over- and underflow checks
2012 `--undefined-shift-check` | add range checks for shift distances
2013 `--nan-check` | add floating-point NaN checks
2014 `--uninitialized-check` | add checks for uninitialized locals (experimental)
2015 `--error-label label` | check that given label is unreachable
2016 
2017 #### Generating function bodies
2018 
2019 Sometimes implementations for called functions are not available in the goto
2020 program, or it is desirable to replace bodies of functions with certain
2021 predetermined stubs (for example to confirm that these functions are never
2022 called, or to indicate that these functions will never return). For this purpose
2023 goto-instrument provides the `--generate-function-body` option, that takes a
2024 regular expression (in [ECMAScript syntax]
2025 (http://en.cppreference.com/w/cpp/regex/ecmascript)) that describes the names of
2026 the functions to generate. Note that this will only generate bodies for
2027 functions that do not already have one; If one wishes to replace the body of a
2028 function with an existing definition, the `--remove-function-body` option can be
2029 used to remove the body of the function prior to generating a new one.
2030 
2031 The shape of the stub itself can be chosen with the
2032 `--generate-function-body-options` parameter, which can take the following
2033 values:
2034 
2035  Option | Result
2036 -----------------------------|-------------------------------------------------------------
2037  `nondet-return` | Do nothing and return a nondet result (this is the default)
2038  `assert-false` | Make the body contain an assert(false)
2039  `assume-false` | Make the body contain an assume(false)
2040  `assert-false-assume-false` | Combines assert-false and assume-false
2041  `havoc` | Set the contents of parameters and globals to nondet
2042 
2043 The various combinations of assert-false and assume-false can be used to
2044 indicate that functions shouldn't be called, that they will never return or
2045 both.
2046 
2047 Example: We have a program like this:
2048 
2049  // error_example.c
2050  #include <stdlib.h>
2051 
2052  void api_error(void);
2053  void internal_error(void);
2054 
2055  int main(void)
2056  {
2057  int arr[10] = {1,2,3,4,5, 6, 7, 8, 9, 10};
2058  int sum = 0;
2059  for(int i = 1; i < 10; ++i)
2060  {
2061  sum += arr[i];
2062  }
2063  if(sum != 55)
2064  {
2065  // we made a mistake when calculating the sum
2066  internal_error();
2067  }
2068  if(rand() < 0)
2069  {
2070  // we think this cannot happen
2071  api_error();
2072  }
2073  return 0;
2074  }
2075 
2076 Now, we can compile the program and detect that the error functions are indeed
2077 called by invoking these commands
2078 
2079  goto-cc error_example.c -o error_example.goto
2080  # Replace all functions ending with _error
2081  # (Excluding those starting with __)
2082  # With ones that have an assert(false) body
2083  goto-instrument error_example.goto error_example_replaced.goto \
2084  --generate-function-body '(?!__).*_error' \
2085  --generate-function-body-options assert-false
2086  cbmc error_example_replaced.goto
2087 
2088 Which gets us the output
2089 
2090 > ** Results:
2091 > [internal_error.assertion.1] assertion false: FAILURE
2092 > [api_error.assertion.1] assertion false: FAILURE
2093 >
2094 >
2095 > ** 2 of 2 failed (2 iterations)
2096 > VERIFICATION FAILED
2097 
2098 As opposed to the verification success we would have gotten without the
2099 generation.
2100 
2101 
2102 The havoc option takes further parameters `globals` and `params` with this
2103 syntax: `havoc[,globals:<regex>][,params:<regex>]` (where the square brackets
2104 indicate an optional part). The regular expressions have the same format as the
2105 those for the `--generate-function-body` option and indicate which globals and
2106 function parameters should be set to nondet. All regular expressions require
2107 exact matches (i.e. the regular expression `a|b` will match 'a' and 'b' but not
2108 'adrian' or 'bertha').
2109 
2110 Example: With a C program like this
2111 
2112  struct Complex {
2113  double real;
2114  double imag;
2115  };
2116 
2117  struct Complex AGlobalComplex;
2118  int do_something_with_complex(struct Complex *complex);
2119 
2120 And the command line
2121 
2122  goto-instrument in.goto out.goto
2123  --generate-function-body do_something_with_complex
2124  --generate-function-body-options
2125  'havoc,params:.*,globals:AGlobalComplex'
2126 
2127 The goto code equivalent of the following will be generated:
2128 
2129  int do_something_with_complex(struct Complex *complex)
2130  {
2131  if(complex)
2132  {
2133  complex->real = nondet_double();
2134  complex->imag = nondet_double();
2135  }
2136  AGlobalComplex.real = nondet_double();
2137  AGlobalComplex.imag = nondet_double();
2138  return nondet_int();
2139  }
2140 
2141 A note on limitations: Because only static information is used for code
2142 generation, arrays of unknown size and pointers will not be affected by this;
2143 Which means that for code like this:
2144 
2145  struct Node {
2146  int val;
2147  struct Node *next;
2148  };
2149 
2150  void do_something_with_node(struct Node *node);
2151 
2152 Code like this will be generated:
2153 
2154  void do_something_with_node(struct Node *node)
2155  {
2156  if(node)
2157  {
2158  node->val = nondet_int();
2159  node->next = nondet_0();
2160  }
2161  }
2162 
2163 Note that no attempt to follow the `next` pointer is made. If an array of
2164 unknown (or 0) size is encountered, a diagnostic is emitted and the array is not
2165 further examined.
2166 
2167 Some care must be taken when choosing the regular expressions for globals and
2168 functions. Names starting with `__` are reserved for internal purposes; For
2169 example, replacing functions or setting global variables with the `__CPROVER`
2170 prefix might make analysis impossible. To avoid doing this by accident, negative
2171 lookahead can be used. For example, `(?!__).*` matches all names not starting
2172 with `__`.
2173 
2174 
2175 \subsection man_instrumentation-api The CPROVER API Reference
2176 
2177 The following sections summarize the functions available to programs
2178 that are passed to the CPROVER tools.
2179 
2180 ### Functions
2181 
2182 #### \_\_CPROVER\_assume, \_\_CPROVER\_assert, assert
2183 
2184  void __CPROVER_assume(_Bool assumption);
2185  void __CPROVER_assert(_Bool assertion, const char *description);
2186  void assert(_Bool assertion);
2187 
2188 The function **\_\_CPROVER\_assume** adds an expression as a constraint
2189 to the program. If the expression evaluates to false, the execution
2190 aborts without failure. More detail on the use of assumptions is in the
2191 section on [Assumptions and Assertions](modeling-assertions.shtml).
2192 
2193 #### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
2194 
2195  void __CPROVER_r_ok(const void *, size_t size);
2196  void __CPROVER_w_ok(cosnt void *, size_t size);
2197 
2198 The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
2199 memory starting at the given pointer with the given size is safe.
2200 **\_\_CPROVER\_w_ok** does the same with writing.
2201 
2202 #### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
2203 
2204  _Bool __CPROVER_same_object(const void *, const void *);
2205  __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p);
2206  __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p);
2207  _Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
2208 
2209 The function **\_\_CPROVER\_same\_object** returns true if the two
2210 pointers given as arguments point to the same object. The function
2211 **\_\_CPROVER\_POINTER\_OFFSET** returns the offset of the given pointer
2212 relative to the base address of the object. The function
2213 **\_\_CPROVER\_DYNAMIC\_OBJECT** returns true if the pointer passed as
2214 arguments points to a dynamically allocated object.
2215 
2216 #### \_\_CPROVER\_is\_zero\_string, \_\_CPROVER\_zero\_string\_length, \_\_CPROVER\_buffer\_size
2217 
2218  _Bool __CPROVER_is_zero_string(const void *);
2219  __CPROVER_size_t __CPROVER_zero_string_length(const void *);
2220  __CPROVER_size_t __CPROVER_buffer_size(const void *);
2221 
2222 #### \_\_CPROVER\_initialize
2223 
2224  void __CPROVER_initialize(void);
2225 
2226 The function **\_\_CPROVER\_initialize** computes the initial state of
2227 the program. It is called prior to calling the main procedure of the
2228 program.
2229 
2230 #### \_\_CPROVER\_input, \_\_CPROVER\_output
2231 
2232  void __CPROVER_input(const char *id, ...);
2233  void __CPROVER_output(const char *id, ...);
2234 
2235 The functions **\_\_CPROVER\_input** and **\_\_CPROVER\_output** are
2236 used to report an input or output value. Note that they do not generate
2237 input or output values. The first argument is a string constant to
2238 distinguish multiple inputs and outputs (inputs are typically generated
2239 using nondeterminism, as described [here](modeling-nondet.shtml)). The
2240 string constant is followed by an arbitrary number of values of
2241 arbitrary types.
2242 
2243 #### \_\_CPROVER\_cover
2244 
2245  void __CPROVER_cover(_Bool condition);
2246 
2247 This statement defines a custom coverage criterion, for usage with the
2248 [test suite generation feature](cover.shtml).
2249 
2250 #### \_\_CPROVER\_isnan, \_\_CPROVER\_isfinite, \_\_CPROVER\_isinf, \_\_CPROVER\_isnormal, \_\_CPROVER\_sign
2251 
2252  _Bool __CPROVER_isnan(double f);
2253  _Bool __CPROVER_isfinite(double f);
2254  _Bool __CPROVER_isinf(double f);
2255  _Bool __CPROVER_isnormal(double f);
2256  _Bool __CPROVER_sign(double f);
2257 
2258 The function **\_\_CPROVER\_isnan** returns true if the double-precision
2259 floating-point number passed as argument is a
2260 [NaN](http://en.wikipedia.org/wiki/NaN).
2261 
2262 The function **\_\_CPROVER\_isfinite** returns true if the
2263 double-precision floating-point number passed as argument is a finite
2264 number.
2265 
2266 This function **\_\_CPROVER\_isinf** returns true if the
2267 double-precision floating-point number passed as argument is plus or
2268 minus infinity.
2269 
2270 The function **\_\_CPROVER\_isnormal** returns true if the
2271 double-precision floating-point number passed as argument is a normal
2272 number.
2273 
2274 This function **\_\_CPROVER\_sign** returns true if the double-precision
2275 floating-point number passed as argument is negative.
2276 
2277 #### \_\_CPROVER\_abs, \_\_CPROVER\_labs, \_\_CPROVER\_fabs, \_\_CPROVER\_fabsl, \_\_CPROVER\_fabsf
2278 
2279  int __CPROVER_abs(int x);
2280  long int __CPROVER_labs(long int x);
2281  double __CPROVER_fabs(double x);
2282  long double __CPROVER_fabsl(long double x);
2283  float __CPROVER_fabsf(float x);
2284 
2285 These functions return the absolute value of the given argument.
2286 
2287 #### \_\_CPROVER\_array\_equal, \_\_CPROVER\_array\_copy, \_\_CPROVER\_array\_set
2288 
2289  _Bool __CPROVER_array_equal(const void array1[], const void array2[]);
2290  void __CPROVER_array_copy(const void dest[], const void src[]);
2291  void __CPROVER_array_set(const void dest[], value);
2292 
2293 The function **\_\_CPROVER\_array\_equal** returns true if the values
2294 stored in the given arrays are equal. The function
2295 **\_\_CPROVER\_array\_copy** copies the contents of the array **src** to
2296 the array **dest**. The function **\_\_CPROVER\_array\_set** initializes
2297 the array **dest** with the given value.
2298 
2299 #### Uninterpreted Functions
2300 
2301 Uninterpreted functions are documented \ref man_modelling-nondet "here".
2302 
2303 ### Predefined Types and Symbols
2304 
2305 #### \_\_CPROVER\_bitvector
2306 
2307  __CPROVER_bitvector [ expression ]
2308 
2309 This type is only available in the C frontend. It is used to specify a
2310 bit vector with arbitrary but fixed size. The usual integer type
2311 modifiers **signed** and **unsigned** can be applied. The usual
2312 arithmetic promotions will be applied to operands of this type.
2313 
2314 #### \_\_CPROVER\_floatbv
2315 
2316  __CPROVER_floatbv [ expression ] [ expression ]
2317 
2318 This type is only available in the C frontend. It is used to specify an
2319 IEEE-754 floating point number with arbitrary but fixed size. The first
2320 parameter is the total size (in bits) of the number, and the second is
2321 the size (in bits) of the mantissa, or significand (not including the
2322 hidden bit, thus for single precision this should be 23).
2323 
2324 #### \_\_CPROVER\_fixedbv
2325 
2326  __CPROVER_fixedbv [ expression ] [ expression ]
2327 
2328 This type is only available in the C frontend. It is used to specify a
2329 fixed-point bit vector with arbitrary but fixed size. The first
2330 parameter is the total size (in bits) of the type, and the second is the
2331 number of bits after the radix point.
2332 
2333 #### \_\_CPROVER\_size\_t
2334 
2335 The type of sizeof expressions.
2336 
2337 #### \_\_CPROVER\_rounding\_mode
2338 
2339  extern int __CPROVER_rounding_mode;
2340 
2341 This variable contains the IEEE floating-point arithmetic rounding mode.
2342 
2343 #### \_\_CPROVER\_constant\_infinity\_uint
2344 
2345 This is a constant that models a large unsigned integer.
2346 
2347 #### \_\_CPROVER\_integer, \_\_CPROVER\_rational
2348 
2349 **\_\_CPROVER\_integer** is an unbounded, signed integer type.
2350 **\_\_CPROVER\_rational** is an unbounded, signed rational number type.
2351 
2352 #### \_\_CPROVER\_memory
2353 
2354  extern unsigned char __CPROVER_memory[];
2355 
2356 This array models the contents of integer-addressed memory.
2357 
2358 #### \_\_CPROVER::unsignedbv&lt;N&gt; (C++ only)
2359 
2360 This type is the equivalent of **unsigned \_\_CPROVER\_bitvector\[N\]**
2361 in the C++ front-end.
2362 
2363 #### \_\_CPROVER::signedbv&lt;N&gt; (C++ only)
2364 
2365 This type is the equivalent of **signed \_\_CPROVER\_bitvector\[N\]** in
2366 the C++ front-end.
2367 
2368 #### \_\_CPROVER::fixedbv&lt;N&gt; (C++ only)
2369 
2370 This type is the equivalent of **\_\_CPROVER\_fixedbv\[N,m\]** in the
2371 C++ front-end.
2372 
2373 ### Concurrency
2374 
2375 Asynchronous threads are created by preceding an instruction with a
2376 label with the prefix **\_\_CPROVER\_ASYNC\_**.
2377 
2378 \subsection man_goto-cc-linux goto-cc: Extracting Models from the Linux Kernel
2379 
2380 The Linux kernel code consists of more than 11 million lines of
2381 low-level C and is frequently used to evaluate static analysis
2382 techniques. In the following, we show how to extract models from Linux
2383 2.6.39.
2384 
2385 1. First of all, you will need to make sure you have around 100 GB of
2386  free disc space available.
2387 
2388 2. Download the Kernel sources at
2389  <http://www.kernel.org/pub/linux/kernel/v2.6/linux-2.6.39.tar.bz2>.
2390 
2391 3. Now do
2392 
2393  `bunzip2 linux-2.6.39.tar.bz2`\
2394  `tar xvf linux-2.6.39.tar`\
2395  `cd linux-2.6.39`
2396 
2397 4. Now ensure that you can actually compile a kernel by doing
2398 
2399  `make defconfig`\
2400  `make`
2401 
2402  These steps need to succeed before you can try to extract models
2403  from the kernel.
2404 
2405 5. Now compile [gcc-wrap.c](gcc-wrap.c) and put the resulting binary
2406  into a directory that is in your PATH variable:
2407 
2408  `lwp-download http://www.cprover.org/cprover-manual/gcc-wrap.c`\
2409  `gcc gcc-wrap.c -o gcc-wrap`\
2410  `cp gcc-wrap ~/bin/`\
2411 
2412  This assumes that the directory `~/bin` exists and is in your
2413  PATH variable.
2414 
2415 6. Now change the variable CC in the kernel Makefile as follows:
2416 
2417  CC = ~/bin/gcc-wrap
2418 
2419 7. Now do
2420 
2421  make clean
2422  make
2423 
2424  This will re-compile the kernel, but this time retaining the
2425  preprocessed source files.
2426 
2427 8. You can now compile the preprocessed source files with goto-cc as
2428  follows:
2429 
2430  find ./ -name .tmp_*.i > source-file-list
2431  for a in `cat source-file-list` ; do
2432  goto-cc -c $a -o $a.gb
2433  done
2434 
2435  Note that it is important that the word-size of the kernel
2436  configuration matches that of goto-cc. Otherwise, compile-time
2437  assertions will fail, generating the error message "bit field size
2438  is negative". For a kernel configured for a 64-bit word-width, pass
2439  the option --64 to goto-cc.
2440 
2441 The resulting `.gb` files can be passed to any of the CPROVER tools.
2442 
2443 \subsection man_goto-cc-apache goto-cc: Extracting Models from the Apache HTTPD
2444 
2445 The [Apache HTTPD](http://httpd.apache.org/) is still the most
2446 frequently used web server. Together with the relevant libraries, it
2447 consists of around 0.4 million lines of C code. In the following, we
2448 show how to extract models from Apache HTTPD 2.4.2.
2449 
2450 1. First of all, we download the sources of Apache HTTPD and two
2451  supporting libraries and uncompress them:
2452 
2453  lwp-download http://www.mirrorservice.org/sites/ftp.apache.org/apr/apr-1.4.6.tar.bz2
2454  lwp-download http://www.mirrorservice.org/sites/ftp.apache.org/apr/apr-util-1.4.1.tar.bz2
2455  lwp-download http://mirror.catn.com/pub/apache/httpd/httpd-2.4.2.tar.bz2
2456  bunzip2 < apr-1.4.6.tar.bz2 | tar x
2457  bunzip2 < apr-util-1.4.1.tar.bz2 | tar x
2458  bunzip2 < httpd-2.4.2.tar.bz2 | tar x
2459 
2460 2. Now compile [gcc-wrap.c](gcc-wrap.c) and put the resulting binary
2461  into a directory that is in your PATH variable:
2462 
2463  lwp-download http://www.cprover.org/cprover-manual/gcc-wrap.c
2464  gcc gcc-wrap.c -o gcc-wrap
2465  cp gcc-wrap ~/bin/
2466 
2467  This assumes that the directory `~/bin` exists and is in your
2468  PATH variable.
2469 
2470 3. We now build the sources with gcc:
2471 
2472  (cd apr-1.4.6; ./configure; make CC=gcc-wrap)
2473  (cd apr-util-1.4.1; ./configure --with-apr=../apr-1.4.6 ; make CC=gcc-wrap)
2474  (cd httpd-2.4.2; ./configure --with-apr=../apr-1.4.6 --with-apr-util=../apr-util-1.4.1 ; make CC=gcc-wrap)
2475 
2476 4. You can now compile the preprocessed source files with goto-cc as
2477  follows:
2478 
2479  find ./ -name *.i > source-file-list
2480  for a in `cat source-file-list` ; do
2481  goto-cc -c $a -o $a.gb
2482  done
2483 
2484 The resulting `.gb` files can be passed to any of the CPROVER tools.