2 \page cbmc-user-manual CBMC User Manual
4 \author Daniel Kroening
6 This tutorial is intended for users of CProver primarily focused on CBMC.
10 \section man_introduction Introduction
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
20 Research in software quality has an enormous breadth. We focus the
21 presentation using two criteria:
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
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.
33 ## Bounded Model Checking with CBMC
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
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.
51 A more detailed description of how to apply CBMC to verify programs is
52 \ref man_cbmc-tutorial "here".
55 ### Example: Buffer Overflows
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):
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".
85 ## Hardware/Software Co-Verification
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.
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".
103 \section man_installation Installation
105 \subsection man_install-cbmc Installing CBMC
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.
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.
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).
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.
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*.
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.
137 ### Installing the CBMC Binaries
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.
144 You are now ready to \ref man_cbmc-tutorial "use CBMC"!
146 ### Building CBMC from Source
148 Alternatively, the CBMC source code is available [via
149 SVN](http://www.cprover.org/svn/cbmc/). To compile the source code,
151 instructions](http://www.cprover.org/svn/cbmc/trunk/COMPILING).
155 \subsection man_install-eclipse Installing the Eclipse Plugin
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.
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*.
171 ### Installing the Eclipse Plugin
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.
178 \section man_cbmc CBMC: Bounded Model Checking for C, C++ and Java
180 \subsection man_cbmc-tutorial A Short Tutorial
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".
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
194 As an example, consider the following simple program, named file1.c:
196 int puts(const char *s) { }
198 int main(int argc, char **argv) {
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:
206 cbmc file1.c --show-properties --bounds-check --pointer-check
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
216 domains](http://en.wikipedia.org/wiki/Abstract_interpretation). More
217 detail on automatically generated properties is provided
218 \ref man_instrumentation-properties "here".
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.
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:
230 cbmc file1.c --show-vcc --bounds-check --pointer-check
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
239 cbmc file1.c --bounds-check --pointer-check
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:
249 [main.pointer_dereference.6] dereference failure: object bounds in argv[(signed long int)2]: FAILURE
251 ### Counterexample Traces
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
257 cbmc file1.c --bounds-check --trace
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.
268 ### Verifying Modules
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:
285 In order to set the entry point to the `sum` function, run
287 cbmc file2.c --function sum --bounds-check
289 It is often necessary to build a suitable *harness* for the function in
290 order to set up the environment appropriately.
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:
300 int binsearch(int x) {
302 signed low=0, high=16;
305 signed middle=low+((high-low)>>1);
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:
323 cbmc binsearch.c --function binsearch --unwind 6 --bounds-check --unwinding-assertions
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`.
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:
360 unsigned got_lock = 0;
366 /* critical section */
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:
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.
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.
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".
400 ### A Note About Compilers and the ANSI-C Library
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
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.
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.
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.
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*.
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".
438 ### Command Line Interface
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.
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
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)
459 We also have a [list of interesting applications of
460 CBMC](http://www.cprover.org/cbmc/applications/).
463 \subsection man_cbmc-loops Understanding Loop Unwinding
465 ### Iteration-based Unwinding
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:
473 int main(int argc, char **argv) {
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:
485 int main(int argc, char **argv) {
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.
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:
518 for(int i=0; i<100; i++) {
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.
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.
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.
542 ### Setting Separate Unwinding Limits
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,
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
553 --unwindset L:B,L:B,...
555 where `L` denotes a loop ID and `B` denotes the bound for that loop.
557 As an example, consider a program with two loops in the function main:
559 --unwindset c::main.0:10,c::main.1:20
561 This sets a bound of 10 for the first loop, and a bound of 20 for the
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:
574 int main(int argc, char **argv) {
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)
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
606 for(int i=0; i<10000; i++) {
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
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.
624 ### Depth-based Unwinding
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
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
638 \subsection man_cbmc-cover COVER: Test Suite Generation with CBMC
641 ### A Small Tutorial with A Case Study
643 We assume that CBMC is installed on your system. If not so, follow
644 \ref man_install-cbmc "these instructions".
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.
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.
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
672 \image html pid.png "The pid controller"
676 02: #define MAX_CLIMB_SUM_ERR 10
677 03: #define MAX_CLIMB 1
680 06: #define MAX_PPRZ (CLOCK*600)
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
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;
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;
699 25: /** PID function OUTPUTS */
700 26: float desired_gaz;
701 27: float desired_pitch;
703 29: /** The state variable: accumulated error in the control */
704 30: float climb_sum_err=0;
706 32: /** Computes desired_gaz and desired_pitch */
707 33: void climb_pid_run()
710 36: float err=estimator_z_dot-desired_climb;
712 38: float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
714 40: float pprz=fgaz*MAX_PPRZ;
715 41: desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
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;
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;
732 58: /** Non-deterministic input values */
733 59: desired_climb=nondet_float();
734 60: estimator_z_dot=nondet_float();
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);
740 66: __CPROVER_input("desired_climb", desired_climb);
741 67: __CPROVER_input("estimator_z_dot", estimator_z_dot);
745 71: __CPROVER_output("desired_gaz", desired_gaz);
746 72: __CPROVER_output("desired_pitch", desired_pitch);
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.
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
768 cbmc pid.c --cover mcdc --unwind 6 --xml-ui
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.
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"
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
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.
802 (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
805 (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
806 (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
809 (iteration 1) desired_climb=0.000000f, estimator_z_dot=-1.000000f
810 (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
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
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
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).
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.
843 ### Coverage Criteria
845 The table below summarizes the coverage criteria that CBMC supports.
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
858 \section man_modelling Modelling
860 \subsection man_modelling-nondet Nondeterminism
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.
872 ### Sources of Nondeterminism
874 The CPROVER tools support the following sources of nondeterminism:
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
880 - initial values of variables that are `extern` in all compilation
882 - explicit functions for generating nondeterminism.
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.
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
894 unsigned short int nondet_ushortint();
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.
901 ### Uninterpreted Functions
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
916 \subsection man_modelling-assumptions Modeling with Assertions and Assumptions
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
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.
936 In addition, there is a CPROVER-specific way to specify assertions,
937 using the built-in function `__CPROVER_assert`:
939 __CPROVER_assert(p!=NULL, "p is not NULL");
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.
945 The assertion language of the CPROVER tools is identical to the language
946 used for expressions. Note that \ref man_modelling-nondet
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
960 The nondeterministic choice will guess the element of the array that is
961 nonzero. The code fragment above is therefore equivalent to
970 Future CPROVER releases will support explicit quantifiers with a syntax
971 that resembles Spec\#:
973 __CPROVER_forall { *type identifier* ; *expression* }
974 __CPROVER_exists { *type identifier* ; *expression* }
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:
984 unsigned int nondet_uint();
986 unsigned int one_to_hundred()
988 unsigned int result=nondet_uint();
989 __CPROVER_assume(result>=1 && result<=100);
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
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:
1006 __CPROVER_assume(x==100);
1008 Assumptions do restrict the search space, but only for assertions that
1009 follow. As an example, the following program will pass:
1014 __CPROVER_assume(x>=1 && x<=100000);
1018 __CPROVER_assert(x<0, "x is negative");
1021 Beware that nondeterminism cannot be used to obtain the effect of
1022 universal quantification in assumptions. As an example,
1029 __CPROVER_assume(x>=0 && x<10 && y>=0 && y<10);
1031 __CPROVER_assume(a[x]>=0);
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).
1039 \subsection man_modelling-pointers Pointer Model
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.
1049 ### Objects and Offsets
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
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,
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
1072 p=(char *)(array+1);
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)`.
1078 ### Dereferencing Pointers
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.
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.
1091 The CPROVER tools support pointer typecasts. Most casts are supported,
1092 with the following exceptions:
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.
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.
1105 3. Accesses to arrays via pointers that have the array subtype need to
1108 ### Pointers in Open Programs
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.
1117 \subsection man_modelling-floating-point Floating Point
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:
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.
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.
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).
1142 - Expression contraction (for example, converting `x * y + c` to
1143 `fma(x,y,c)`) is not performed. In effect, the `FP_CONTRACT` pragma
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.
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).
1158 ### x86 and Other Platform-specific Issues
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.
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.
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.
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.
1202 The rounding mode is stored in the (thread local) variable
1203 `__CPROVER_rounding_mode`, but users are strongly advised not to use
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
1215 ### Fixed-point Arithmetic
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.
1223 \section man_hard-soft Hardware and Software Equivalence and Co-Verification
1225 \subsection man_hard-soft-introduction Introduction
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).
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.
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
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 Establishing the consistency does not require a formal
1254 specification. However, formal methods to verify either the hardware or
1255 software design are still desirable.
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.
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 required to be in a very specific form, since a
1275 mechanical translation is assumed.
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
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 required 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
1292 ### Further Material
1294 We provide a small \ref man_hard-soft-tutorial "tutorial" and a
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/)
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)
1313 \subsection man_hard-soft-tutorial Tutorial
1315 ### Verilog vs. ANSI-C
1317 We assume that CBMC is installed on your system. If not so, follow
1318 \ref man_install-cbmc "these instructions".
1320 The following Verilog module implements a 4-bit counter
1323 module top(input clk);
1329 always @(posedge clk)
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:
1341 unsigned int counter;
1344 extern struct module_top top;
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
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
1361 extern const unsigned int bound;
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.
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):
1372 void next_timeframe();
1375 unsigned int counter;
1378 extern struct module_top top;
1383 assert(top.counter==2);
1385 assert(top.counter==3);
1388 The following CBMC command line checks these assertions with a bound of
1391 hw-cbmc counter.c counter.v --module top --bound 20
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.
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.
1405 For the given example, the verification is successful. If the first
1406 assertion is changed to
1408 assert(top.counter==10);
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.
1417 ----------------------------------------------------
1418 bound=6 (00000000000000000000000000000110)
1419 counter={ 0, 1, 2, 3, 4, 5, 6 }
1421 Failed assertion: assertion line 6 function main
1423 Transition system state 0
1424 ----------------------------------------------------
1427 Transition system state 1
1428 ----------------------------------------------------
1431 Transition system state 2
1432 ----------------------------------------------------
1435 Transition system state 3
1436 ----------------------------------------------------
1439 Transition system state 4
1440 ----------------------------------------------------
1443 Transition system state 5
1444 ----------------------------------------------------
1447 Transition system state 6
1448 ----------------------------------------------------
1453 The following program is using the bound variable to check the counter
1454 value in all cycles:
1456 void next_timeframe();
1457 extern const unsigned int bound;
1460 unsigned int counter;
1463 extern struct module_top top;
1468 for(cycle=0; cycle<bound; cycle++) {
1469 assert(top.counter==(cycle & 15));
1474 CBMC performs bounds checking, and restricts the number of times that
1475 `next_timeframe()` can be called. SATABS does not require a bound, and
1476 thus, `next_timeframe()` can be called arbitrarily many times.
1479 \subsection man_hard-soft-mapping Mapping Variables
1481 ### Mapping Variables within the Module Hierarchy
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
1488 As an example, consider the following Verilog file
1491 module counter(input clk, input [7:0] increment);
1497 always @(posedge clk)
1498 counter=counter+increment;
1502 module top(input clk);
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:
1515 void next_timeframe();
1516 extern const unsigned int bound;
1519 unsigned char increment;
1520 unsigned char counter;
1524 struct module_counter c1, c2;
1527 extern struct module_top top;
1533 assert(top.c1.counter==3);
1534 assert(top.c2.counter==6);
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
1543 hw-cbmc --gen-interface --module top hierarchy.v
1545 ### Mapping Verilog Vectors to Arrays or Scalars
1547 In Verilog, a definition such as
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
1558 will allow using `x` in arithmetic expressions, while the C declaration
1560 __CPROVER_bool x[32];
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.
1571 \subsection man_hard-soft-inputs Synchronizing Inputs
1573 ### Driving Primary Inputs
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:
1581 module top(input clk, input i);
1587 always @(posedge clk)
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:
1599 void next_timeframe();
1601 extern const unsigned int bound;
1604 unsigned int counter;
1608 extern struct module_top top;
1611 assert(top.counter==0);
1614 set_inputs(); next_timeframe();
1615 assert(top.counter==1);
1618 set_inputs(); next_timeframe();
1619 assert(top.counter==2);
1622 set_inputs(); next_timeframe();
1623 assert(top.counter==2);
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:
1631 set_inputs(); next_timeframe();
1633 for(i=1; i<bound; i++) {
1635 set_inputs(); next_timeframe();
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.
1643 ### Using Nondeterminism
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".
1650 \section man_instrumentation Build Systems, Libraries, and Instrumentation
1652 \subsection man_instrumentation-libraries Build Systems and Libraries
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:
1660 - Despite recent advances, the size of the programs that model
1661 checkers can cope with is still restricted.
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).
1667 - CBMC and SATABS cannot verify binary libraries.
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.
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".
1683 \subsection man_instrumentation-goto-cc Integration into Build Systems with goto-cc
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.
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).
1705 ### Example: Building wu-ftpd
1707 This example assumes a Unix-like machine.
1709 1. Download the sources of wu-ftpd from
1710 [here](ftp://ftp.wu-ftpd.org/pub/wu-ftpd/wu-ftpd-current.tar.gz).
1712 2. Unpack the sources by running ` tar xfz wu-ftpd-current.tar.gz`
1714 3. Change to the source directory, by entering, e.g.,
1717 4. Configure the project for verification by running
1719 `./configure YACC=byacc CC=goto-cc --host=none-none-none`
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
1725 6. Run a model-checker, e.g., CBMC, on the model file:
1729 CBMC automatically recognizes that the file is a goto binary.
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
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`.
1747 A helpful command that accomplishes this task successfully for many
1748 projects is the following:
1750 for i in `find . -name Makefile`; do sed -e 's/^\(\s*CC[ \t]*=\)\(.*$\)/\1goto-cc/g' -i $i done
1752 Here are additional examples on how to use goto-cc:
1754 - \ref man_goto-cc-linux "Linux Kernel"
1755 - \ref man_goto-cc-apache "Apache HTTPD"
1757 A description of how to integrate goto-cc into Microsoft's Visual Studio
1758 is \ref man_instrumentation-vs "here".
1760 ### Linking Libraries
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.
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.
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.
1779 \subsection man_instrumentation-vs Integration into Visual Studio 2008 to 2012
1781 Visual Studio version 2008 onwards comes with a new XML-based build
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.
1788 The MSBuild system can be used to generate goto-binaries from your
1789 Visual Studio project as follows:
1791 1. Install the `goto-cl.exe` and `goto-link.exe` binaries in some
1792 directory that is contained in the PATH environment variable.
1794 2. Add a configuration for the goto-cc build for your project in the
1795 configuration manager, named "goto-cc".
1797 3. Open the Visual Studio Command Prompt (in the Tools menu).
1799 4. Locate the directory that contains the project. Change into this
1800 directory using "CD".
1804 msbuild /p:CLToolExe=goto-cl.exe /p:LinkToolExe=goto-link.exe /p:Flavor=goto-cc /p:Platform=x86
1806 The platform can be adjusted as required; the "Flavor" given should
1807 match the configuration that was created earlier.
1809 Note that the recent versions of goto-cc also support file names with
1810 non-ASCII (Unicode) characters on Windows platforms.
1812 \subsection man_instrumentation-goto-cc-variants Variants of goto-cc
1814 The goto-cc utility comes in several variants, summarised in the
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
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.
1830 The "hybrid" executables contain both the control-flow graph for
1831 verification purposes and the usual, executable machine code.
1833 \subsection man_instrumentation-architecture Architectural Settings
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:
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
1843 - The [endianness](http://en.wikipedia.org/wiki/Endianness) of
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`.
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:
1857 - The word-width can be set with `--16`, `--32`, `--64`.
1858 - The endianness can be defined with `--little-endian` and
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
1866 In order to see the effect of the options `--16`, `--32` and `--64`,
1867 pass the following program to CBMC:
1873 printf("sizeof(long int): %d\n", (int)sizeof(long int));
1874 printf("sizeof(int *): %d\n", (int)sizeof(int *));
1878 The counterexample trace contains the strings printed by the `printf`
1881 The effects of endianness are more subtle. Try the following program
1882 with `--big-endian` and `--little-endian`:
1890 printf("Bytes of i: %d, %d, %d, %d\n", p[0], p[1], p[2], p[3]);
1895 \subsection man_instrumentation-properties Property Instrumentation
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.
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`
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"
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.
1923 The assertion generator can generate assertions for the verification of
1924 the following properties:
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.
1931 - **Division by zero.** Check whether there is a division by zero in
1934 - **Not-a-Number.** Check whether floating-point computation may
1935 result in [NaNs](http://en.wikipedia.org/wiki/NaN).
1937 - **Unitialized local.** Check whether the program uses an
1938 uninitialized local variable.
1940 - **Data race.** Check whether a concurrent program accesses a shared
1941 variable at the same time in two threads.
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
1949 All the properties described above are *reachability* properties. They
1950 are always of the form
1952 "*Is there a path through the program such that property ... is
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".
1960 ### Using goto-instrument
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:
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.
1974 As an example, we begin with small C program we call `expr.c` (taken
1975 from [here](http://www.spinroot.com/uno/)):
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.
1990 goto-cc expr.c -o in.gb goto-instrument in.gb out.gb --pointer-check
1992 We can now get a list of the assertions that have been generated as
1995 goto-instrument out.gb --show-properties
1997 Using either CBMC or SATABS on `out.gb`, we can obtain a counterexample
1998 trace for the NULL-pointer dereference:
2002 The goto-instrument program supports the following checks:
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
2017 #### Generating function bodies
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.
2031 The shape of the stub itself can be chosen with the
2032 `--generate-function-body-options` parameter, which can take the following
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
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
2047 Example: We have a program like this:
2052 void api_error(void);
2053 void internal_error(void);
2057 int arr[10] = {1,2,3,4,5, 6, 7, 8, 9, 10};
2059 for(int i = 1; i < 10; ++i)
2065 // we made a mistake when calculating the sum
2070 // we think this cannot happen
2076 Now, we can compile the program and detect that the error functions are indeed
2077 called by invoking these commands
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
2088 Which gets us the output
2091 > [internal_error.assertion.1] assertion false: FAILURE
2092 > [api_error.assertion.1] assertion false: FAILURE
2095 > ** 2 of 2 failed (2 iterations)
2096 > VERIFICATION FAILED
2098 As opposed to the verification success we would have gotten without the
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').
2110 Example: With a C program like this
2117 struct Complex AGlobalComplex;
2118 int do_something_with_complex(struct Complex *complex);
2120 And the command line
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'
2127 The goto code equivalent of the following will be generated:
2129 int do_something_with_complex(struct Complex *complex)
2133 complex->real = nondet_double();
2134 complex->imag = nondet_double();
2136 AGlobalComplex.real = nondet_double();
2137 AGlobalComplex.imag = nondet_double();
2138 return nondet_int();
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:
2150 void do_something_with_node(struct Node *node);
2152 Code like this will be generated:
2154 void do_something_with_node(struct Node *node)
2158 node->val = nondet_int();
2159 node->next = nondet_0();
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
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
2175 \subsection man_instrumentation-api The CPROVER API Reference
2177 The following sections summarize the functions available to programs
2178 that are passed to the CPROVER tools.
2182 #### \_\_CPROVER\_assume, \_\_CPROVER\_assert, assert
2184 void __CPROVER_assume(_Bool assumption);
2185 void __CPROVER_assert(_Bool assertion, const char *description);
2186 void assert(_Bool assertion);
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).
2193 #### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
2195 void __CPROVER_r_ok(const void *, size_t size);
2196 void __CPROVER_w_ok(cosnt void *, size_t size);
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.
2202 #### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
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);
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.
2216 #### \_\_CPROVER\_is\_zero\_string, \_\_CPROVER\_zero\_string\_length, \_\_CPROVER\_buffer\_size
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 *);
2222 #### \_\_CPROVER\_initialize
2224 void __CPROVER_initialize(void);
2226 The function **\_\_CPROVER\_initialize** computes the initial state of
2227 the program. It is called prior to calling the main procedure of the
2230 #### \_\_CPROVER\_input, \_\_CPROVER\_output
2232 void __CPROVER_input(const char *id, ...);
2233 void __CPROVER_output(const char *id, ...);
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
2243 #### \_\_CPROVER\_cover
2245 void __CPROVER_cover(_Bool condition);
2247 This statement defines a custom coverage criterion, for usage with the
2248 [test suite generation feature](cover.shtml).
2250 #### \_\_CPROVER\_isnan, \_\_CPROVER\_isfinite, \_\_CPROVER\_isinf, \_\_CPROVER\_isnormal, \_\_CPROVER\_sign
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);
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).
2262 The function **\_\_CPROVER\_isfinite** returns true if the
2263 double-precision floating-point number passed as argument is a finite
2266 This function **\_\_CPROVER\_isinf** returns true if the
2267 double-precision floating-point number passed as argument is plus or
2270 The function **\_\_CPROVER\_isnormal** returns true if the
2271 double-precision floating-point number passed as argument is a normal
2274 This function **\_\_CPROVER\_sign** returns true if the double-precision
2275 floating-point number passed as argument is negative.
2277 #### \_\_CPROVER\_abs, \_\_CPROVER\_labs, \_\_CPROVER\_fabs, \_\_CPROVER\_fabsl, \_\_CPROVER\_fabsf
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);
2285 These functions return the absolute value of the given argument.
2287 #### \_\_CPROVER\_array\_equal, \_\_CPROVER\_array\_copy, \_\_CPROVER\_array\_set
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);
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.
2299 #### Uninterpreted Functions
2301 Uninterpreted functions are documented \ref man_modelling-nondet "here".
2303 ### Predefined Types and Symbols
2305 #### \_\_CPROVER\_bitvector
2307 __CPROVER_bitvector [ expression ]
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.
2314 #### \_\_CPROVER\_floatbv
2316 __CPROVER_floatbv [ expression ] [ expression ]
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).
2324 #### \_\_CPROVER\_fixedbv
2326 __CPROVER_fixedbv [ expression ] [ expression ]
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.
2333 #### \_\_CPROVER\_size\_t
2335 The type of sizeof expressions.
2337 #### \_\_CPROVER\_rounding\_mode
2339 extern int __CPROVER_rounding_mode;
2341 This variable contains the IEEE floating-point arithmetic rounding mode.
2343 #### \_\_CPROVER\_constant\_infinity\_uint
2345 This is a constant that models a large unsigned integer.
2347 #### \_\_CPROVER\_integer, \_\_CPROVER\_rational
2349 **\_\_CPROVER\_integer** is an unbounded, signed integer type.
2350 **\_\_CPROVER\_rational** is an unbounded, signed rational number type.
2352 #### \_\_CPROVER\_memory
2354 extern unsigned char __CPROVER_memory[];
2356 This array models the contents of integer-addressed memory.
2358 #### \_\_CPROVER::unsignedbv<N> (C++ only)
2360 This type is the equivalent of **unsigned \_\_CPROVER\_bitvector\[N\]**
2361 in the C++ front-end.
2363 #### \_\_CPROVER::signedbv<N> (C++ only)
2365 This type is the equivalent of **signed \_\_CPROVER\_bitvector\[N\]** in
2368 #### \_\_CPROVER::fixedbv<N> (C++ only)
2370 This type is the equivalent of **\_\_CPROVER\_fixedbv\[N,m\]** in the
2375 Asynchronous threads are created by preceding an instruction with a
2376 label with the prefix **\_\_CPROVER\_ASYNC\_**.
2378 \subsection man_goto-cc-linux goto-cc: Extracting Models from the Linux Kernel
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
2385 1. First of all, you will need to make sure you have around 100 GB of
2386 free disc space available.
2388 2. Download the Kernel sources at
2389 <http://www.kernel.org/pub/linux/kernel/v2.6/linux-2.6.39.tar.bz2>.
2393 `bunzip2 linux-2.6.39.tar.bz2`\
2394 `tar xvf linux-2.6.39.tar`\
2397 4. Now ensure that you can actually compile a kernel by doing
2402 These steps need to succeed before you can try to extract models
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:
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/`\
2412 This assumes that the directory `~/bin` exists and is in your
2415 6. Now change the variable CC in the kernel Makefile as follows:
2424 This will re-compile the kernel, but this time retaining the
2425 preprocessed source files.
2427 8. You can now compile the preprocessed source files with goto-cc as
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
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.
2441 The resulting `.gb` files can be passed to any of the CPROVER tools.
2443 \subsection man_goto-cc-apache goto-cc: Extracting Models from the Apache HTTPD
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.
2450 1. First of all, we download the sources of Apache HTTPD and two
2451 supporting libraries and uncompress them:
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
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:
2463 lwp-download http://www.cprover.org/cprover-manual/gcc-wrap.c
2464 gcc gcc-wrap.c -o gcc-wrap
2467 This assumes that the directory `~/bin` exists and is in your
2470 3. We now build the sources with gcc:
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)
2476 4. You can now compile the preprocessed source files with goto-cc as
2479 find ./ -name *.i > source-file-list
2480 for a in `cat source-file-list` ; do
2481 goto-cc -c $a -o $a.gb
2484 The resulting `.gb` files can be passed to any of the CPROVER tools.