+**Task:** Read the documentation for `goto_function_templatet`
+and `goto_programt`.
+
+
+Each goto_programt object contains a list of
+\ref goto_program_templatet::instructiont called
+`instructions`. Each instruction has a field called `code`, which has
+type \ref codet.
+
+
+**Task:** Add a `--pretty-program` switch to `goto-instrument`. This
+switch should use the `codet::pretty()` function to pretty-print every
+\ref codet in the entire program. The strings that `pretty()` generates
+for a codet look like this:
+
+ index
+ * type: unsignedbv
+ * width: 8
+ * #c_type: char
+ 0: symbol
+ * type: array
+ * size: nil
+ * type:
+ * #source_location:
+ * file: src/main.c
+ * line: 18
+ * function:
+ * working_directory: /some/dir
+ 0: unsignedbv
+ * width: 8
+ * #c_type: char
+ ...
+
+
+The sub-nodes of a particular node in the pretty representation are
+numbered, starting from 0. They can be accessed through the `op0()`,
+`op1()` and `op2()` methods in the `exprt` class.
+
+Every node in the pretty representation has an identifier, accessed
+through the `id()` function. The file `util/irep_ids.def` lists the
+possible values of these identifiers; have a quick scan through that
+file. In the pretty representation above, the following facts are true
+of that particular node:
+
+ - `node.id() == ID_index`
+ - `node.type().id() == ID_unsignedbv`
+ - `node.op0().id() == ID_symbol`
+ - `node.op0().type().id() == ID_array`
+
+The fact that the `op0()` child has a `symbol` ID menas that you could
+cast it to a `symbol_exprt` (which is a subtype of `exprt`) using the
+function `to_symbol_expr`.
+
+
+**Task:** Add flags to `goto-instrument` to print out the following information:
+* the name of every function that is *called* in the program;
+* the value of every constant in the program;
+* the value of every symbol in the program.
+
diff --git a/doc/html-manual/binsearch.c b/doc/assets/binsearch.c
similarity index 100%
rename from doc/html-manual/binsearch.c
rename to doc/assets/binsearch.c
diff --git a/doc/html-manual/c_to_ir.svg b/doc/assets/c_to_ir.svg
similarity index 100%
rename from doc/html-manual/c_to_ir.svg
rename to doc/assets/c_to_ir.svg
diff --git a/doc/html-manual/cegar-1.png b/doc/assets/cegar-1.png
similarity index 100%
rename from doc/html-manual/cegar-1.png
rename to doc/assets/cegar-1.png
diff --git a/doc/html-manual/counter.c b/doc/assets/counter.c
similarity index 100%
rename from doc/html-manual/counter.c
rename to doc/assets/counter.c
diff --git a/doc/html-manual/boop-example/driver.c b/doc/assets/driver.c
similarity index 100%
rename from doc/html-manual/boop-example/driver.c
rename to doc/assets/driver.c
diff --git a/doc/html-manual/boop-example/driver.h b/doc/assets/driver.h
similarity index 100%
rename from doc/html-manual/boop-example/driver.h
rename to doc/assets/driver.h
diff --git a/doc/html-manual/expr.c b/doc/assets/expr.c
similarity index 100%
rename from doc/html-manual/expr.c
rename to doc/assets/expr.c
diff --git a/doc/html-manual/expr.svg b/doc/assets/expr.svg
similarity index 100%
rename from doc/html-manual/expr.svg
rename to doc/assets/expr.svg
diff --git a/doc/html-manual/file1.c b/doc/assets/file1.c
similarity index 100%
rename from doc/html-manual/file1.c
rename to doc/assets/file1.c
diff --git a/doc/html-manual/file2.c b/doc/assets/file2.c
similarity index 100%
rename from doc/html-manual/file2.c
rename to doc/assets/file2.c
diff --git a/doc/html-manual/gcc-wrap.c b/doc/assets/gcc-wrap.c
similarity index 100%
rename from doc/html-manual/gcc-wrap.c
rename to doc/assets/gcc-wrap.c
diff --git a/doc/html-manual/goto_program.svg b/doc/assets/goto_program.svg
similarity index 100%
rename from doc/html-manual/goto_program.svg
rename to doc/assets/goto_program.svg
diff --git a/doc/html-manual/ireptree.svg b/doc/assets/ireptree.svg
similarity index 100%
rename from doc/html-manual/ireptree.svg
rename to doc/assets/ireptree.svg
diff --git a/doc/html-manual/boop-example/kdev_t.h b/doc/assets/kdev_t.h
similarity index 100%
rename from doc/html-manual/boop-example/kdev_t.h
rename to doc/assets/kdev_t.h
diff --git a/doc/html-manual/lock-example-fixed.c b/doc/assets/lock-example-fixed.c
similarity index 100%
rename from doc/html-manual/lock-example-fixed.c
rename to doc/assets/lock-example-fixed.c
diff --git a/doc/html-manual/lock-example.c b/doc/assets/lock-example.c
similarity index 100%
rename from doc/html-manual/lock-example.c
rename to doc/assets/lock-example.c
diff --git a/doc/html-manual/boop-example/modules.h b/doc/assets/modules.h
similarity index 100%
rename from doc/html-manual/boop-example/modules.h
rename to doc/assets/modules.h
diff --git a/doc/html-manual/pid.c b/doc/assets/pid.c
similarity index 100%
rename from doc/html-manual/pid.c
rename to doc/assets/pid.c
diff --git a/doc/html-manual/pid.png b/doc/assets/pid.png
similarity index 100%
rename from doc/html-manual/pid.png
rename to doc/assets/pid.png
diff --git a/doc/html-manual/refinement.png b/doc/assets/refinement.png
similarity index 100%
rename from doc/html-manual/refinement.png
rename to doc/assets/refinement.png
diff --git a/doc/html-manual/ring_buffer1.c b/doc/assets/ring_buffer1.c
similarity index 100%
rename from doc/html-manual/ring_buffer1.c
rename to doc/assets/ring_buffer1.c
diff --git a/doc/html-manual/ring_buffer2.c b/doc/assets/ring_buffer2.c
similarity index 100%
rename from doc/html-manual/ring_buffer2.c
rename to doc/assets/ring_buffer2.c
diff --git a/doc/html-manual/boop-example/spec.c b/doc/assets/spec.c
similarity index 100%
rename from doc/html-manual/boop-example/spec.c
rename to doc/assets/spec.c
diff --git a/doc/html-manual/states.png b/doc/assets/states.png
similarity index 100%
rename from doc/html-manual/states.png
rename to doc/assets/states.png
diff --git a/doc/cprover-manual.md b/doc/cprover-manual.md
new file mode 100644
index 00000000000..90d609193d9
--- /dev/null
+++ b/doc/cprover-manual.md
@@ -0,0 +1,2982 @@
+\ingroup module_hidden
+\page cprover-manual CProver User Manual
+
+\author Daniel Kroening
+
+This tutorial is intended for users of CProver (CBMC, SatAbs, and
+associated tools).
+
+\tableofcontents
+
+\section man_introduction Introduction
+
+## Motivation
+
+Numerous tools to hunt down functional design flaws in silicon have been
+available for many years, mainly due to the enormous cost of hardware
+bugs. The use of such tools is wide-spread. In contrast, the market for
+tools that address the need for quality software is still in its
+infancy.
+
+Research in software quality has an enormous breadth. We focus the
+presentation using two criteria:
+
+1. We believe that any form of quality requires a specific *guarantee*,
+ in theory and practice.
+2. The sheer size of software designs requires techniques that are
+ highly *automated*.
+
+In practice, quality guarantees usually do not refer to "total
+correctness" of a design, as ensuring the absence of all bugs is too
+expensive for most applications. In contrast, a guarantee of the absence
+of specific flaws is achievable, and is a good metric of quality.
+
+We document two programs that try to achieve formal guarantees of the
+absence of specific problems: CBMC and SATABS. The algorithms
+implemented by CBMC and SATABS are complementary, and often, one tool is
+able to solve a problem that the other cannot solve.
+
+Both CBMC and SATABS are verification tools for ANSI-C/C++ programs.
+They verify array bounds (buffer overflows), pointer safety, exceptions
+and user-specified assertions. Both tools model integer arithmetic
+accurately, and are able to reason about machine-level artifacts such as
+integer overflow. CBMC and SATABS are therefore able to detect a class
+of bugs that has so far gone unnoticed by many other verification tools.
+This manual also covers some variants of CBMC, which includes HW-CBMC
+for
+\ref man_hard-soft-introduction "hardware/software co-verification".
+
+## Bounded Model Checking with CBMC
+
+CBMC implements a technique called *Bounded Model Checking* (BMC). In
+BMC, the transition relation for a complex state machine and its
+specification are jointly unwound to obtain a Boolean formula, which is
+then checked for satisfiability by using an efficient SAT procedure. If
+the formula is satisfiable, a counterexample is extracted from the
+output of the SAT procedure. If the formula is not satisfiable, the
+program can be unwound more to determine if a longer counterexample
+exists.
+
+In many engineering domains, real-time guarantees are a strict
+requirement. An example is software embedded in automotive controllers.
+As a consequence, the loop constructs in these types of programs often
+have a strict bound on the number of iterations. CBMC is able to
+formally verify such bounds by means of *unwinding assertions*. Once
+this bound is established, CBMC is able to prove the absence of errors.
+
+A more detailed description of how to apply CBMC to verify programs is
+\ref man_cbmc-tutorial "here".
+
+## Automatic Program Verification with SATABS
+
+In many cases, lightweight properties such as array bounds do not rely
+on the entire program. A large fraction of the program is *irrelevant*
+to the property. SATABS exploits this observation and computes an
+*abstraction* of the program in order to handle large amounts of code.
+
+In order to use SATABS it is not necessary to understand the abstraction
+refinement process. For the interested reader, a high-level introduction
+to abstraction refinement is provided
+\ref man_satabs-overview "here".
+We also provide
+\ref man_satabs-tutorials "tutorials on how to use SATABS".
+
+Just as CBMC, SATABS attempts to build counterexamples that refute the
+property. If such a counterexample is found, it is presented to the
+engineer to facilitate localization and repair of the program.
+
+### Example: Buffer Overflows
+
+In order to give a brief overview of the capabilities of CBMC and SATABS
+we start with a small example. The issue of *[buffer
+overflows](http://en.wikipedia.org/wiki/Buffer_overflow)* has obtained
+wide public attention. A buffer is a contiguously-allocated chunk of
+memory, represented by an array or a pointer in C. Programs written in C
+do not provide automatic bounds checking on the buffer, which means a
+program can – accidentally or maliciously – write past a buffer. The
+following example is a perfectly valid C program (in the sense that a
+compiler compiles it without any errors):
+
+```{.c}
+int main()
+{
+ int buffer[10];
+ buffer[20] = 10;
+}
+```
+
+However, the write access to an address outside the allocated memory
+region can lead to unexpected behavior. In particular, such bugs can be
+exploited to overwrite the return address of a function, thus enabling
+the execution of arbitrary user-induced code. CBMC and SATABS are able
+to detect this problem and reports that the "upper bound property" of
+the buffer is violated. CBMC and SATABS are capable of checking these
+lower and upper bounds, even for arrays with dynamic size. A detailed
+discussion of the properties that CBMC and SATABS can check
+automatically is \ref man_instrumentation-properties "here".
+
+## Hardware/Software Co-Verification
+
+Software programs often interact with hardware in a non-trivial manner,
+and many properties of the overall design only arise from the interplay
+of both components. CBMC and SATABS therefore support *Co-Verification*,
+i.e., are able to reason about a C/C++ program together with a circuit
+description given in Verilog.
+
+These co-verification capabilities can also be applied to perform
+refinement proofs. Software programs are often used as high-level
+descriptions of circuitry. While both describe the same functionality,
+the hardware implementation usually contains more detail. It is highly
+desirable to establish some form for equivalence between the two
+descriptions. Hardware/Software co-verification and equivalence checking
+with CBMC and SATABS are described
+\ref man_hard-soft-introduction "here".
+
+
+\section man_installation Installation
+
+\subsection man_install-cbmc Installing CBMC
+
+### Requirements
+
+CBMC is available for Windows, i86 Linux, and MacOS X. CBMC requires a
+code pre-processing environment comprising of a suitable preprocessor
+and an a set of header files.
+
+1. **Linux:** the preprocessor and the header files typically come with
+ a package called *gcc*, which must be installed prior to the
+ installation of CBMC.
+
+2. **Windows:** The Windows version of CBMC requires the preprocessor
+ `cl.exe`, which is part of Microsoft Visual Studio. We recommend the
+ free [Visual Studio Community
+ 2013](http://www.visualstudio.com/en-us/products/visual-studio-community-vs).
+
+3. **MacOS:** Install the [XCode Command Line
+ Utilities](http://developer.apple.com/technologies/xcode.html) prior
+ to installing CBMC. Just installing XCode alone is not enough.
+
+Important note for Windows users: Visual Studio's `cl.exe` relies on a
+complex set of environment variables to identify the target architecture
+and the directories that contain the header files. You must run CBMC
+from within the *Visual Studio Command Prompt*.
+
+Note that the distribution files for the [Eclipse
+plugin](installation-plugin.shtml) include the CBMC executable.
+Therefore, if you intend to run CBMC exclusively within Eclipse, you can
+skip the installation of the CBMC executable. However, you still have to
+install the compiler environment as described above.
+
+### Installing the CBMC Binaries
+
+1. Download CBMC for your operating system. The binaries are available
+ from http://www.cprover.org/cbmc/.
+2. Unzip/untar the archive into a directory of your choice. We
+ recommend to add this directory to your `PATH` environment variable.
+
+You are now ready to \ref man_cbmc-tutorial "use CBMC"!
+
+### Building CBMC from Source
+
+Alternatively, the CBMC source code is available [via
+SVN](http://www.cprover.org/svn/cbmc/). To compile the source code,
+follow [these
+instructions](http://www.cprover.org/svn/cbmc/trunk/COMPILING).
+
+\subsection man_install-satabs Installing SATABS
+
+### Requirements
+
+SATABS is available for Windows, i86 Linux, and MacOS X. SATABS requires
+a code pre-processing environment comprising of a suitable preprocessor
+and an a set of header files.
+
+1. **Linux:** the preprocessor and the header files typically come with
+ a package called *gcc*, which must be installed prior to the
+ installation of SATABS.
+2. **Windows:** The Windows version of SATABS requires the preprocessor
+ `cl.exe`, which is part of Visual Studio (including the free [Visual
+ Studio
+ Express](http://msdn.microsoft.com/vstudio/express/visualc/)).
+3. **MacOS:** Install
+ [XCode](http://developer.apple.com/technologies/xcode.html) prior to
+ installing SATABS.
+
+Important note for Windows users: Visual Studio's `cl.exe` relies on a
+complex set of environment variables to identify the target architecture
+and the directories that contain the header files. You must run SATABS
+from within the *Visual Studio Command Prompt*.
+
+Note that the distribution files for the [Eclipse
+plugin](installation-plugin.shtml) include the command-line tools.
+Therefore, if you intend to run SATABS exclusively within Eclipse, you
+can skip the installation of the command-line tools. However, you still
+have to install the compiler environment as described above.
+
+### Choosing and Installing a Model Checker
+
+You need to install a Model Checker in order to be able to run SATABS.
+You can choose between following alternatives:
+
+- **Cadence SMV**. Available from http://www.kenmcmil.com/smv.html.
+ Cadence SMV is a commercial model checker. The free version that is
+ available on the homepage above must not be used for commercial
+ purposes (read the license agreement thoroughly before you download
+ the tool). The documentation for SMV can be found in the directory
+ where you unzip/untar SMV under ./smv/doc/smv/. Read the
+ installation instructions carefully. The Linux/MacOS versions
+ require setting environment variables. You must add add the
+ directory containing the `smv` binary (located in ./smv/bin/,
+ relative to the path where you unpacked it) to your `PATH`
+ environment variable. SATABS uses Cadence SMV by default.
+
+- **NuSMV**. Available from http://nusmv.irst.itc.it/. NuSMV is the
+ open source alternative to Cadence SMV. Installation instructions
+ and documentation can be found on the NuSMV homepage. The directory
+ containing the NuSMV binary should be added to your `PATH`
+ environment variable. Use the option
+
+ --modelchecker nusmv
+
+ to instruct SATABS to use NuSMV.
+
+- **BOPPO**. Available from http://www.cprover.org/boppo/. BOPPO is
+ a model checker that uses SAT-solving algorithms. BOPPO relies on a
+ built-in SAT solver and Quantor, a solver for quantified boolean
+ formulas that is currently bundled with BOPPO, but also available
+ separately from The CPROVER API Reference
- --The following sections summarize the functions available to programs -that are passed to the CPROVER tools. -
- -Functions
- -__CPROVER_assume, __CPROVER_assert, assert
- --
-void __CPROVER_assume(_Bool assumption);
-void __CPROVER_assert(_Bool assertion, const char *description);
-void assert(_Bool assertion);
-
-- -
-The function __CPROVER_assume adds an expression as a constraint -to the program. If the expression evaluates to false, the execution -aborts without failure. More detail on the use of assumptions is -in the section on Assumptions -and Assertions. -
- -__CPROVER_same_object, __CPROVER_POINTER_OBJECT, -__CPROVER_POINTER_OFFSET, -__CPROVER_DYNAMIC_OBJECT
- --
-_Bool __CPROVER_same_object(const void *, const void *);
-unsigned __CPROVER_POINTER_OBJECT(const void *p);
-signed __CPROVER_POINTER_OFFSET(const void *p);
-_Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
-
-- -
-The function __CPROVER_same_object returns true -if the two pointers given as arguments point to the same -object. -The function __CPROVER_POINTER_OFFSET returns -the offset of the given pointer relative to the base -address of the object. -The function __CPROVER_DYNAMIC_OBJECT -returns true if the pointer passed -as arguments points to a dynamically allocated object. -
- -__CPROVER_is_zero_string, -__CPROVER_zero_string_length, -__CPROVER_buffer_size
- --
-_Bool __CPROVER_is_zero_string(const void *);
-__CPROVER_size_t __CPROVER_zero_string_length(const void *);
-__CPROVER_size_t __CPROVER_buffer_size(const void *);
-
-- -
-
- -__CPROVER_initialize
- --
-void __CPROVER_initialize(void);
-
-- -
-The function __CPROVER_initialize computes the initial -state of the program. It is called prior to calling the -main procedure of the program. -
- -__CPROVER_input, __CPROVER_output
- --
-void __CPROVER_input(const char *id, ...);
-void __CPROVER_output(const char *id, ...);
-
-- -
-The functions __CPROVER_input and __CPROVER_output -are used to report an input or output value. Note that they do not generate -input or output values. The first argument is a string constant -to distinguish multiple inputs and outputs (inputs are typically -generated using nondeterminism, as described -here). -The string constant is followed by an arbitrary number of values of -arbitrary types. -
- -__CPROVER_cover
- --
-void __CPROVER_cover(_Bool condition);
-
-- -
This statement defines a custom coverage criterion, for usage -with the test suite generation feature.
- --
- -__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isinf, -__CPROVER_isnormal, __CPROVER_sign
- --
-_Bool __CPROVER_isnan(double f);
-_Bool __CPROVER_isfinite(double f);
-_Bool __CPROVER_isinf(double f);
-_Bool __CPROVER_isnormal(double f);
-_Bool __CPROVER_sign(double f);
-
-- -
-The function __CPROVER_isnan returns true if the double-precision -floating-point number passed as argument is a -NaN. -
- --The function __CPROVER_isfinite returns true if the double-precision -floating-point number passed as argument is a -finite number. -
- --This function __CPROVER_isinf returns true if the double-precision -floating-point number passed as argument is plus -or minus infinity. -
- --The function __CPROVER_isnormal returns true if the double-precision -floating-point number passed as argument is a -normal number. -
- --This function __CPROVER_sign returns true if the double-precision -floating-point number passed as argument is -negative. -
- -__CPROVER_abs, __CPROVER_labs, __CPROVER_fabs, __CPROVER_fabsl, __CPROVER_fabsf
- --
-int __CPROVER_abs(int x);
-long int __CPROVER_labs(long int x);
-double __CPROVER_fabs(double x);
-long double __CPROVER_fabsl(long double x);
-float __CPROVER_fabsf(float x);
-
-- -
-These functions return the absolute value of the given -argument. -
- -__CPROVER_array_equal, __CPROVER_array_copy, __CPROVER_array_set
- --
-_Bool __CPROVER_array_equal(const void array1[], const void array2[]);
-void __CPROVER_array_copy(const void dest[], const void src[]);
-void __CPROVER_array_set(const void dest[], value);
-
-- -
-The function __CPROVER_array_equal returns true if the values -stored in the given arrays are equal. -The function __CPROVER_array_copy copies the contents of -the array src to the array dest. -The function __CPROVER_array_set initializes the array dest with -the given value. -
- -Uninterpreted Functions
- --Uninterpreted functions are documented here. -
- -Predefined Types and Symbols
- -__CPROVER_bitvector
- --
-__CPROVER_bitvector [ expression ]
-
-- -
-This type is only available in the C frontend. It is used -to specify a bit vector with arbitrary but fixed size. The -usual integer type modifiers signed and unsigned -can be applied. The usual arithmetic promotions will be -applied to operands of this type. -
- -__CPROVER_floatbv
- --
-__CPROVER_floatbv [ expression ] [ expression ]
-
-- -
-This type is only available in the C frontend. It is used -to specify an IEEE-754 floating point number with arbitrary -but fixed size. The first parameter is the total size (in bits) -of the number, and the second is the size (in bits) of the -mantissa, or significand (not including the hidden bit, thus for -single precision this should be 23). -
- -__CPROVER_fixedbv
- --
-__CPROVER_fixedbv [ expression ] [ expression ]
-
-- -
-This type is only available in the C frontend. It is used -to specify a fixed-point bit vector with arbitrary -but fixed size. The first parameter is the total size (in bits) -of the type, and the second is the number of bits after the radix -point. -
- -__CPROVER_size_t
- --The type of sizeof expressions. -
- -__CPROVER_rounding_mode
- --
-extern int __CPROVER_rounding_mode;
-
-- -
-This variable contains the IEEE floating-point -arithmetic rounding mode. -
- -__CPROVER_constant_infinity_uint
- --This is a constant that models a large unsigned -integer. -
- -__CPROVER_integer, __CPROVER_rational
- --__CPROVER_integer is an unbounded, signed integer type. -__CPROVER_rational is an unbounded, signed rational -number type. -
- -__CPROVER_memory
- --
-extern unsigned char __CPROVER_memory[];
-
-- -
-This array models the contents of integer-addressed memory. -
- -__CPROVER::unsignedbv<N> (C++ only)
- -This type is the equivalent of unsigned __CPROVER_bitvector[N] in the C++ front-end. -
- -__CPROVER::signedbv<N> (C++ only)
- -This type is the equivalent of signed __CPROVER_bitvector[N] in the C++ front-end. -
- -__CPROVER::fixedbv<N> (C++ only)
- -This type is the equivalent of __CPROVER_fixedbv[N,m] in the C++ front-end. -
- -Concurrency
- --Asynchronous threads are created by preceding an instruction with a label with the prefix __CPROVER_ASYNC_. -
- - diff --git a/doc/html-manual/architecture.shtml b/doc/html-manual/architecture.shtml deleted file mode 100644 index 18ef3e0b1fc..00000000000 --- a/doc/html-manual/architecture.shtml +++ /dev/null @@ -1,93 +0,0 @@ - - - - -Build Systems and Libraries
- -Architectural Settings
- -The behavior of a C/C++ program depends on a number of -parameters that are specific to the architecture the program was compiled -for. The three most important architectural parameters are:
- --
-
- The width of the various scalar types; e.g., compare the value
-of
sizeof(long int)on various machines.
-
- - The width of pointers; e.g., compare the value
-of
sizeof(int *)on various machines.
-
- - The endianness -of the architecture. -
-In general, the CPROVER tools attempt to adopt the settings of the
-particular architecture the tool itself was compiled for. For example,
-when running a 64 bit binary of CBMC on Linux, the program will be processed
-assuming that sizeof(long int)==8.
-As a consequence of these architectural parameters, -you may observe different verification results for an identical -program when running CBMC on different machines. In order to get -consistent results, or when aiming at validating a program written -for a different platform, the following command-line arguments can -be passed to the CPROVER tools:
- --
-
- The word-width can be set with
--16, ---32,--64.
- - The endianness can be defined with
-
--little-endianand--big-endian.
-
-When using a goto binary, CBMC and the other tools read the configuration -from the binary, i.e., the setting when running goto-cc is the one that -matters; the option given to the model checker is ignored in this case. -
- -
-In order to see the effect of the options --16,
---32 and --64, pass
-the following program to CBMC:
-
-#include <stdio.h>
-#include <assert.h>
-
-int main() {
- printf("sizeof(long int): %d\n", (int)sizeof(long int));
- printf("sizeof(int *): %d\n", (int)sizeof(int *));
- assert(0);
-}
-
-- -
-The counterexample trace contains the strings printed by the
-printf command.
-The effects of endianness are
-more subtle. Try the following program with --big-endian
-and --little-endian:
-
-#include <stdio.h>
-#include <assert.h>
-
-int main() {
- int i=0x01020304;
- char *p=(char *)&i;
- printf("Bytes of i: %d, %d, %d, %d\n",
- p[0], p[1], p[2], p[3]);
- assert(0);
-}
-- - diff --git a/doc/html-manual/cbmc-loops.shtml b/doc/html-manual/cbmc-loops.shtml deleted file mode 100644 index da4df1eaeea..00000000000 --- a/doc/html-manual/cbmc-loops.shtml +++ /dev/null @@ -1,233 +0,0 @@ - - - - - - - - -
CBMC: Bounded Model Checking for C/C++ and Java
- -Understanding Loop Unwinding
- -Iteration-based Unwinding
- --The basic idea of CBMC is to model the computation of the programs up to a -particular depth. Technically, this is achieved by a process that -essentially amounts to unwinding loops. This concept is best -illustrated with a generic example: -
- -int main(int argc, char **argv) {
- while(cond) {
- BODY CODE
- }
-}
--A BMC instance that will find bugs with up to five iterations of the loop would -contain five copies of the loop body, and essentially corresponds to checking -the following loop-free program: -
- -int main(int argc, char **argv) {
- if(cond) {
- BODY CODE COPY 1
- if(cond) {
- BODY CODE COPY 2
- if(cond) {
- BODY CODE COPY 3
- if(cond) {
- BODY CODE COPY 4
- if(cond) {
- BODY CODE COPY 5
- }
- }
- }
- }
- }
-}
-
-Note the use of the if statement to prevent the execution of
-the loop body in the case that the loop ends before five iterations are executed.
-The construction above is meant to produce a program that is trace equivalent
-with the original programs for those traces that contain up to five iterations
-of the loop.
-
-In many cases, CBMC is able to automatically determine an upper bound on the - -number of loop iterations. This may even work when the number of loop -unwindings is not constant. Consider the following example: -
- -_Bool f();
-
-int main() {
- for(int i=0; i<100; i++) {
- if(f()) break;
- }
-
- assert(0);
-}
-
-The loop in the program above has an obvious upper bound on the number of
-iterations, but note that the loop may abort prematurely depending on the
-value that is returned by f(). CBMC is nevertheless able to
-automatically unwind the loop to completion.
-This automatic detection of the unwinding
-bound may fail if the number of loop iterations is highly data-dependent.
-Furthermore, the number of iterations that are executed by any given
-loop may be too large or may simply be unbounded. For this case,
-CBMC offers the command-line option --unwind B, where
-B denotes a number that corresponds to the maximal number
-of loop unwindings CBMC performs on any loop.
-
-Note that the number of unwindings is measured by counting the number of
-backjumps. In the example above, note that the condition
-i<100 is in fact evaluated 101 times before the loop
-terminates. Thus, the loop requires a limit of 101, and not 100.
Setting Separate Unwinding Limits
- -
-The setting given with --unwind is used globally,
-that is, for all loops in the program. In order to set individual
-limits for the loops, first use
-
- --show-loops
-
-
--to obtain a list of all loops in the program. Then identify the loops -you need to set a separate bound for, and note their loop ID. Then -use -
- -
- --unwindset L:B,L:B,...
-
-
-
-where L denotes a loop ID and B denotes
-the bound for that loop.
-As an example, consider a program with two loops in the function -main: -
- -
- --unwindset c::main.0:10,c::main.1:20
-
-
--This sets a bound of 10 for the first loop, and a bound of 20 for -the second loop. -
- -
-What if the number of unwindings specified is too small? In this case, bugs
-that require paths that are deeper may be missed. In order to address this
-problem, CBMC can optionally insert checks that the given unwinding bound is
-actually sufficiently large. These checks are called unwinding
-assertions, and are enabled with the option
---unwinding-assertions. Continuing the generic example above,
-this unwinding assertion for a bound of five corresponds to checking the
-following loop-free program:
-
int main(int argc, char **argv) {
- if(cond) {
- BODY CODE COPY 1
- if(cond) {
- BODY CODE COPY 2
- if(cond) {
- BODY CODE COPY 3
- if(cond) {
- BODY CODE COPY 4
- if(cond) {
- BODY CODE COPY 5
- assert(!cond);
- }
- }
- }
- }
- }
-}
--The unwinding assertions can be verified just like any other generated -assertion. If all of them are proven to hold, the given loop bounds are -sufficient for the program. This establishes a high-level -worst-case execution time (WCET). -
- --In some cases, it is desirable to cut off very deep loops in favor -of code that follows the loop. As an example, consider the -following program: -
- -int main() {
- for(int i=0; i<10000; i++) {
- BODY CODE
- }
-
- assert(0);
-}
-
-In the example above, small values of --unwind will
-prevent that the assertion is reached. If the code in the loop
-is considered irrelevant to the later assertion, use the option
-
- --partial-loops
-
-
--This option will allow paths that execute loops only partially, -enabling a counterexample for the assertion above even for -small unwinding bounds. The disadvantage of using this option -is that the resulting path may be spurious, i.e., may not -exist in the original program. -
- -Depth-based Unwinding
- -
-The loop-based unwinding bound is not always appropriate. In particular,
-it is often difficult to control the size of the generated formula
-when using the --unwind option. The option
-
- --depth nr
-
-
--specifies an unwinding bound in terms of the number of instructions that are -executed on a given path, irrespectively of the number of loop iterations. -Note that CBMC uses the number of instructions in the control-flow graph -as the criterion, not the number of instructions in the source code. -
- - diff --git a/doc/html-manual/cbmc.shtml b/doc/html-manual/cbmc.shtml deleted file mode 100644 index a52f39a90f5..00000000000 --- a/doc/html-manual/cbmc.shtml +++ /dev/null @@ -1,377 +0,0 @@ - - - - - - - - -CBMC: Bounded Model Checking for C/C++ and Java
- -A Short Tutorial
- -First Steps
- --We assume you have already installed CBMC and the necessary support files -on your system. If not so, please follow -these instructions. -
- --Like a compiler, CBMC takes the names of .c files as command line -arguments. CBMC then translates the program and merges the function -definitions from the various .c files, just like a linker. But instead -of producing a binary for execution, CBMC performs symbolic simulation on -the program. -
- --As an example, consider the following simple program, named -file1.c: -
- -int puts(const char *s) { }
-
-int main(int argc, char **argv) {
- puts(argv[2]);
-}
-
-Of course, this program is faulty, as the argv array might have fewer
-than three elements, and then the array access argv[2] is out of bounds.
-Now, run CBMC as follows:
-
- cbmc file1.c --show-properties --bounds-check --pointer-check
-
-
-The two options --bounds-check and --pointer-check
-instruct CBMC to look for errors related to pointers and array bounds.
-CBMC will print the list of properties it checks. Note that it lists,
-among others, a property labeled with "object bounds in argv" together with
-the location of the faulty array access. As you can see, CBMC largely
-determines the property it needs to check itself. This is realized by means
-of a preliminary static analysis, which relies on computing a fixed point on
-various abstract
-domains. More detail on automatically generated properties is provided
-here.
-Note that these automatically generated properties need not necessarily -correspond to bugs – these are just potential flaws, as -abstract interpretation might be imprecise. Whether these properties -hold or correspond to actual bugs needs to be determined by further analysis. -
- --CBMC performs this analysis using symbolic simulation, which -corresponds to a translation of the program into a formula. The formula is -then combined with the property. Let's look at the formula that is -generated by CBMC's symbolic simulation:
- -
- cbmc file1.c --show-vcc --bounds-check --pointer-check
-
-
--With this option, CBMC performs the symbolic simulation and prints the -verification conditions on the screen. A verification condition needs -to be proven to be valid by a -decision procedure in order to assert that the corresponding property -holds. Let's run the decision procedure:
- -
- cbmc file1.c --bounds-check --pointer-check
-
-
-
-CBMC transforms the equation you have seen before into CNF and passes it to
-a SAT solver (more background on this step is in the book on Decision Procedures). It
-then determines which of the properties that it has generated for the
-program hold and which do not. Using the SAT solver, CBMC detects that the
-property for the object bounds of argv does not hold, and will
-thus print a line as follows:
-
-[main.pointer_dereference.6] dereference failure: object bounds in argv[(signed long int)2]: FAILURE
-
-
-Counterexample Traces
- --Let us have a closer look at this property and why it fails. To aid the -understanding of the problem, CBMC can generate a counterexample -trace for failed properties. To obtain this trace, run -
- -
- cbmc file1.c --bounds-check --trace
-
-
-
-CBMC then prints a counterexample trace, i.e., a program trace that begins
-with main and ends in a state which violates the property. In
-our example, the program trace ends in the faulty array access. It also
-gives the values the input variables must have for the bug to occur. In
-this example, argc must be one to trigger the out-of-bounds
-array access. If you add a branch to the example that requires that
-argc>=3, the bug is fixed and CBMC will report that the
-proofs of all properties have been successful.
Verifying Modules
- -
-In the example above, we used a program that starts with a main
-function. However, CBMC is aimed at embedded software, and these
-kinds of programs usually have different entry points. Furthermore, CBMC
-is also useful for verifying program modules. Consider the following example,
-called file2.c:
-
int array[10];
-int sum() {
- unsigned i, sum;
-
- sum=0;
- for(i=0; i<10; i++)
- sum+=array[i];
-}
-
-In order to set the entry point to the sum function, run
-
- cbmc file2.c --function sum --bounds-check
-
-
--It is often necessary to build a suitable harness for the function -in order to set up the environment appropriately. -
- -Loop Unwinding
- -
-When running the previous example, you will have noted that CBMC unwinds the
-for loop in the program. As CBMC performs Bounded Model
-Checking, all loops have to have a finite upper run-time bound in order to
-guarantee that all bugs are found. CBMC can optionally check that enough
-unwinding is performed. As an example, consider the program binsearch.c:
-
int binsearch(int x) {
- int a[16];
- signed low=0, high=16;
-
- while(low<high) {
- signed middle=low+((high-low)>>1);
-
- if(a[middle]<x)
- high=middle;
- else if(a[middle]>x)
- low=middle+1;
- else // a[middle]==x
- return middle;
- }
-
- return -1;
-}
--If you run CBMC on this function, you will notice that the unwinding -does not stop on its own. The built-in simplifier is not able to determine -a run time bound for this loop. The unwinding bound has to be given as a -command line argument:
- -
- cbmc binsearch.c --function binsearch --unwind 6 --bounds-check --unwinding-assertions
-
-
-
-CBMC verifies that verifies the array accesses are within the bounds; note
-that this actually depends on the result of the right shift. In addition,
-as CBMC is given the option
---unwinding-assertions--property.
-
Unbounded Loops
- --CBMC can also be used for programs with unbounded loops. In this -case, CBMC is used for bug hunting only; CBMC does not attempt to find -all bugs. The following program -(lock-example.c) is an example -of a program with a user-specified property:
- -_Bool nondet_bool();
-_Bool LOCK = 0;
-
-_Bool lock() {
- if(nondet_bool()) {
- assert(!LOCK);
- LOCK=1;
- return 1; }
-
- return 0;
-}
-
-void unlock() {
- assert(LOCK);
- LOCK=0;
-}
-
-int main() {
- unsigned got_lock = 0;
- int times;
-
- while(times > 0) {
- if(lock()) {
- got_lock++;
- /* critical section */
- }
-
- if(got_lock!=0)
- unlock();
-
- got_lock--;
- times--;
-} }
-
-The while loop in the main function has no
-(useful) run-time bound. Thus, a bound has to be set on the amount of
-unwinding that CBMC performs. There are two ways to do so:
-
-
-
-
- The
--unwindcommand-line parameter can to be used to limit -the number of times loops are unwound.
-
- - The
--depthcommand-line parameter can be used to limit -the number of program steps to be processed.
-
-
-Given the option --unwinding-assertions, CBMC checks whether
-the arugment to --unwind is large enough to cover all program
-paths. If the argument is too small, CBMC will detect that not enough
-unwinding is done reports that an unwinding assertion has failed.
-
-Reconsider the example. For a loop unwinding bound of one, no bug is found.
-But already for a bound of two, CBMC detects a trace that violates an
-assertion. Without unwinding assertions, or when using the --depth
-command line switch, CBMC does not prove the program correct, but it can be
-helpful to find program bugs. The various command line options that CBMC
-offers for loop unwinding are described in the section on
-understanding loop unwinding.
A Note About Compilers and the ANSI-C Library
- -
-Most C programs make use of functions provided by a library; instances are
-functions from the standard ANSI-C library such as malloc or
-printf. The verification of programs that use such functions
-has two requirements:
-
-
-
- Appropriate header files have to be provided. These header files -contain declarations of the functions that are to be used. - - -
- Appropriate definitions have to be provided. - -
-Most C compilers come with header files for the ANSI-C library functions. -We briefly discuss how to obtain/install these library files. -
- -Linux
- --Linux systems that are able to compile software are usually equipped with -the appropriate header files. Consult the documentation of your distribution -on how to install the compiler and the header files. First try to compile -some significant program before attempting to verify it. -
- -Windows
- --On Microsoft Windows, CBMC is pre-configured to use the compiler that is -part of Microsoft's Visual Studio. Microsoft's -Visual Studio Community is fully featured and available for download for -free from the Microsoft webpage. Visual Studio installs the usual set of -header files together with the compiler. However, the Visual Studio -compiler requires a large set of environment variables to function -correctly. It is therefore required to run CBMC from the Visual Studio -Command Prompt, which can be found in the menu Visual Studio -Tools. -
- -
-Note that in both cases, only header files are available. CBMC only
-comes with a small set of definitions, which includes functions such as
-malloc. Detailed information about the built-in definitions is
-here.
Command Line Interface
- -
-This section describes the command line interface of CBMC. Like a C
-compiler, CBMC takes the names of the .c source files as arguments.
-Additional options allow to customize the behavior of CBMC. Use
-cbmc --help to get a full list of the available options.
-
-Structured output can be obtained from CBMC using the option --xml-ui.
-Any output from CBMC (e.g., counterexamples) will then use an XML
-representation.
-
-
-
-
-
diff --git a/doc/html-manual/counter.v b/doc/html-manual/counter.v
deleted file mode 100644
index 4920568889c..00000000000
--- a/doc/html-manual/counter.v
+++ /dev/null
@@ -1,10 +0,0 @@
-module top(input clk);
-
- reg [3:0] counter;
-
- initial counter=0;
-
- always @(posedge clk)
- counter=counter+1;
-
-endmodule
diff --git a/doc/html-manual/cover.shtml b/doc/html-manual/cover.shtml
deleted file mode 100644
index 3665121f0b9..00000000000
--- a/doc/html-manual/cover.shtml
+++ /dev/null
@@ -1,276 +0,0 @@
-
-
-
-
-
-
-
-
-Further Reading
-
--
-
- Understanding Loop Unwinding -
- - Hardware Verification using ANSI-C Programs as a Reference -
- - Behavioral Consistency of C and Verilog Programs Using Bounded Model - Checking -
- A - Tool for Checking ANSI-C Programs -
-We also have a list of -interesting applications of CBMC.
- -Automatic Test Suite Generation with CBMC
- -A Small Tutorial with A Case Study
- --We assume that CBMC is installed on your system. If not so, follow -these instructions.
- --CBMC can be used to automatically generate test cases that satisfy a certain code coverage -criterion. Common coverage criteria include branch coverage, condition -coverage and Modified -Condition/Decision Coverage (MC/DC). Among others, MC/DC is required -by several avionics software development guidelines to ensure adequate testing -of safety critical software. Briefly, in order to satisfy MC/DC, -for every conditional statement containing boolean decisions, each Boolean -variable should be evaluated one time to "true" and one time to "false", -in a way that affects the outcome of the decision. -
- --In the following, we are going to demonstrate how to apply the test suite -generation functionality in CBMC, by means of a case study. The program -pid.c is an excerpt from a real-time embedded benchmark PapaBench, -and implements part of a fly-by-wire autopilot for an Unmanned Aerial Vehicle (UAV). -It is adjusted mildly for our purposes. -
- -
-The aim of function climb_pid_run is to control the vertical climb of the UAV.
-Details on the theory behind this operation are documented in the wiki for the Paparazzi UAV project.
-The behaviour of this simple controller, supposing that the desired speed is 0.5 meters per second,
-is plotted in the Figure below.
-
-
-01: // CONSTANTS:
-02: #define MAX_CLIMB_SUM_ERR 10
-03: #define MAX_CLIMB 1
-04:
-05: #define CLOCK 16
-06: #define MAX_PPRZ (CLOCK*600)
-07:
-08: #define CLIMB_LEVEL_GAZ 0.31
-09: #define CLIMB_GAZ_OF_CLIMB 0.75
-10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
-11: #define CLIMB_PGAIN -0.03
-12: #define CLIMB_IGAIN 0.1
-13:
-14: const float pitch_of_vz_pgain=CLIMB_PITCH_OF_VZ_PGAIN;
-15: const float climb_pgain=CLIMB_PGAIN;
-16: const float climb_igain=CLIMB_IGAIN;
-17: const float nav_pitch=0;
-18:
-19: /** PID function INPUTS */
-20: // The user input: target speed in vertical direction
-21: float desired_climb;
-22: // Vertical speed of the UAV detected by GPS sensor
-23: float estimator_z_dot;
-24:
-25: /** PID function OUTPUTS */
-26: float desired_gaz;
-27: float desired_pitch;
-28:
-29: /** The state variable: accumulated error in the control */
-30: float climb_sum_err=0;
-31:
-32: /** Computes desired_gaz and desired_pitch */
-33: void climb_pid_run()
-34: {
-35:
-36: float err=estimator_z_dot-desired_climb;
-37:
-38: float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
-39:
-40: float pprz=fgaz*MAX_PPRZ;
-41: desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
-42:
-43: /** pitch offset for climb */
-44: float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
-45: desired_pitch=nav_pitch+pitch_of_vz;
-46:
-47: climb_sum_err=err+climb_sum_err;
-48: if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
-49: if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
-50:
-51: }
-52:
-53: int main()
-54: {
-55:
-56: while(1)
-57: {
-58: /** Non-deterministic input values */
-59: desired_climb=nondet_float();
-60: estimator_z_dot=nondet_float();
-61:
-62: /** Range of input values */
-63: __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
-64: __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
-65:
-66: __CPROVER_input("desired_climb", desired_climb);
-67: __CPROVER_input("estimator_z_dot", estimator_z_dot);
-68:
-69: climb_pid_run();
-70:
-71: __CPROVER_output("desired_gaz", desired_gaz);
-72: __CPROVER_output("desired_pitch", desired_pitch);
-73:
-74: }
-75:
-76: return 0;
-77: }
-
-In order to test the PID controller, we construct a main control loop,
-which repeatedly invokes the function climb_pid_run (line 69).
-This PID function has two input variables: the desired speed desired_climb
-and the estimated speed estimated_z_dot.
-In the beginning of each loop iteration, values of the inputs are assigned non-deterministically.
-Subsequently, the __CPROVER_assume statement in lines 63 and 64 guarantees that
-both values are bounded within a valid range.
-The __CPROVER_input and __CPROVER_output will help clarify the inputs
-and outputs of interest for generating test suites.
-
-To demonstrate the automatic test suite generation in CBMC, -we call the following command and we are going to explain the command line options one by one. -
- -cbmc pid.c --cover mcdc --unwind 6 --xml-ui
-
-The option --cover mcdc specifies the code coverage criterion.
-There are four conditional statements in the PID function: in line 41, line 44,
-line 48 and line 49.
-To satisfy MC/DC, the test suite has to meet multiple requirements.
-For instance, each conditional statement needs to evaluate to true and false.
-Consider the condition "pprz>=0 && pprz<=MAX_PPRZ" in line 41. CBMC
-instruments three coverage goals to control the respective evaluated results of "pprz>=0" and
-"pprz<=MAX_PPRZ".
-We list them in below and they satisfy the MC/DC rules.
-Note that MAX_PPRZ is defined as 16 * 600 in line 06 of the program.
-
-!(pprz >= (float)0) && pprz <= (float)(16 * 600) id="climb_pid_run.coverage.1"
-pprz >= (float)0 && !(pprz <= (float)(16 * 600)) id="climb_pid_run.coverage.2"
-pprz >= (float)0 && pprz <= (float)(16 * 600) id="climb_pid_run.coverage.3"
-
-
-
-The "id" of each coverage goal is automatically assigned by CBMC. For every
-coverage goal, a test suite (if there exists) that
-satisfies such a goal is printed out in XML format, as the parameter
---xml-ui is given. Multiple coverage goals can share a
-test suite, when the corresponding execution of the program satisfies all these
-goals at the same time.
-
-In the end, the following test suites are automatically generated for testing the PID controller.
-A test suite consists of a sequence of input parameters that are
-passed to the PID function climb_pid_run at each loop iteration.
-For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
-The complete output from CBMC is in
-pid_test_suites.xml, where every test suite and the coverage goals it is for
-are clearly described.
-
-
Test suite:
-Test 1.
- (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-
-Test 2.
- (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
- (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-
-Test 3.
- (iteration 1) desired_climb=0.000000f, estimator_z_dot=-1.000000f
- (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-
-Test 4.
- (iteration 1) desired_climb=1.000000f, estimator_z_dot=-1.000000f
- (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
- (iteration 3) desired_climb=1.000000f, estimator_z_dot=-1.000000f
- (iteration 4) desired_climb=1.000000f, estimator_z_dot=-1.000000f
- (iteration 5) desired_climb=0.000000f, estimator_z_dot=-1.000000f
- (iteration 6) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-
-Test 5.
- (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
- (iteration 2) desired_climb=-1.000000f, estimator_z_dot=1.000000f
- (iteration 3) desired_climb=-1.000000f, estimator_z_dot=1.000000f
- (iteration 4) desired_climb=-1.000000f, estimator_z_dot=1.000000f
- (iteration 5) desired_climb=-1.000000f, estimator_z_dot=1.000000f
- (iteration 6) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-
-The option --unwind 6 unwinds the loop inside the main
-function body six times. In order to achieve the complete coverage on all the instrumented goals
-in the PID function climb_pid_run, the loop must be unwound sufficient enough times.
-For example, climb_pid_run needs to be called at least six times for evaluating the
-condition climb_sum_err>MAX_CLIMB_SUM_ERR in line 48 to true.
-This corresponds to the Test 5.
-An introduction to the use of loop unwinding can be found
-in Understanding Loop Unwinding.
-
-In this small tutorial, we present the automatic test suite generation
-functionality of CBMC, by applying the MC/DC code coverage criterion to a
-PID controller case study. In addition to --cover mcdc, other
-coverage criteria like branch, decision,
-path etc. are also available when calling CBMC.
-
Coverage Criteria
- --The table below summarizes the coverage criteria that CBMC supports. -
- -| Criterion | Definition |
|---|---|
| assertion | -For every assertion, generate a test that reaches it |
| location | -For every location, generate a test that reaches it |
| branch | -Generate a test for every branch outcome |
| decision | -Generate a test for both outcomes of every Boolean expression -that is not an operand of a propositional connective |
| condition | -Generate a test for both outcomes of every Boolean expression |
| mcdc | -Modified Condition/Decision Coverage (MC/DC) |
| path | -Bounded path coverage |
| cover | -Generate a test for every __CPROVER_cover statement
- |
The CPROVER Source Code Reference
- --The following sections provide an introduction for anybody who -wishes to modify CBMC or build new tools on top of the APIs used -by CBMC. They summarize key components, data structures and APIs -that are used to build the CPROVER tools. -
- -Source Code Availability and Compilation
- --The most recent source code of CBMC and the CPROVER infrastructure can be obtained -via git at https://github.com/diffblue/cbmc.git. -Tar balls for releases are available at https://github.com/diffblue/cbmc/releases. -
- --Detailed instructions on how to build CBMC from source are given -in the file COMPILING. -
- -Components
- -
-The sources of the C frontend are located in the "src/ansi-c" directory. It -uses a standard Flex/Bison setup for scanning and parsing the files. The -Flex scanner produces a token sequence, which is turned into a tree -representation of the input program using the Bison grammar. The -typechecker subsequently annotates this parse tree with types and generates -a symbol table. The symbol table is a map from identifiers (functions, -variables and types) to their definitions. -
- --The following example illustrates how to use the frontend for parsing files and -for translating them into a symbol table. A call to parse generates -the parse tree of the program. The conversion into the symbol table is -performed during type checking, which is done by a call to the -typecheck method. The symbol table is a map from identifiers to the -symbolt data structure. -
- -#include <iostream>
-#include <fstream>
-#include <sstream>
-#include <string>
-
-#include <ansi-c/ansi_c_language.h>
-#include <util/cmdline.h>
-#include <util/config.h>
-
-int main(int argc, const char* argv[])
-{
- // Command line: parse -I incl_dir file1 ...
- cmdlinet cmdl;
- cmdl.parse(argc, argv, "I:");
-
- config.init();
-
- if(cmdl.isset('I'))
- config.ansi_c.include_paths=cmdl.get_values('I');
-
- // Set language to C
- std::auto_ptr<languaget> clang=new_ansi_c_language();
-
- // Symbol table
- symbol_tablet my_symbol_table;
-
- for(const auto & arg : cmdl.args)
- {
- // Source code stream
- std::ifstream in(arg.c_str());
-
- // Parse
- clang->parse(in, "", std::cerr);
-
- // Typecheck
- clang->typecheck(my_symbol_table, arg, std::cerr);
- }
-
- // Do some final adjustements
- clang->final(my_symbol_table, std::cerr);
-
- my_symbol_table.show(std::cout);
-
- return 0;
-}
--The parse trees are implemented using a class called irept. Its -declaration and definiton can be found in the files "src/util/irep.h" and -"src/util/irep.cpp", respectively. -
- --The excerpt below gives some details of the class irept: -
- -class irept
-{
-public:
- typedef std::vector<irept> subt;
- typedef std::map<irep_name_string, irept> named_subt;
- ...
-
-public:
- class dt
- {
- public:
- unsigned ref_count;
- dstring data;
- named_subt named_sub;
- named_subt comments;
- subt sub;
- ...
- };
-
-protected:
- dt *data;
- ...
-};
--Every node of any tree is an object of class irept. Each node has a -pointer to an object of class dt. The dt objects are used -for storing the actual content of nodes. Objects of class dt are -dynamically allocated and can be shared between nodes. A reference-counter -mechanism is implemented to automatically free unreachable dt -objects. A shallow copy of a tree is an O(1) operation. -
- --The field data of class dt is a (hashed) string -representing the label of the nodes. The fields named_sub, -comments and sub are links to childs. Edges are either -labeled with a string or ordered. The string-labeled edges are stored in the -map comments if their first character is '#'. Otherwise, they are -stored in the map named_sub. The labels of edges are unique for a -given node; however, their ordering is not preserved. The field sub -is a vector of nodes that is used for storing the ordered children. The order -of edges of this kind is preserved during copy. -
- -
Interface of Class irept
- -id
- -const irep_idt &id();
-void id(const irep_idt &_data);
--The first method returns a constant reference to the label of the node. The -second method sets the label of the node. -
- -is_nil and is_not_nil
- -virtual bool is_nil() const;
-virtual bool is_not_nil() const;
--The first method returns true if the label of the node is equal to "nil". -The second method returns false if the label of the node is equal to "nil". -
- -find, add and get
- -const irept &find(const irep_namet &name) const;
-irept &add(const irep_namet &name);
-const irep_idt &get(const irep_namet &name) const;
--
-
-
- The first method looks for an edge with label name -and returns the corresponding child. If no edge with label name -is found, then nil_rep is returned. - -
- The second method does the same as the first except that if -no edge with label name if found, then a new child is created -and returned. - - -
- The third method does the same as the first except that the label -of the child is returned (instead of a reference). -If no edge with label name is found, then an empty -string is returned. - - -
set
- -void set(const irep_namet &name,
- const irep_idt &value);
-void set(const irep_namet &name, const long value);
-void set(const irep_namet &name, const irept &irep);
--These methods create a new edge with label name. -
- --If the second argument is an object of class irept, then it is -assigned to the new child. - -
-If the second argument is a string, then it is set as node-label of the new child. - -
-If the second argument is a number, then it is converted to a -string and set as node-label of the new child. - -
remove
- -void remove(const irep_namet &name);
--This method looks for an edge with label name -and removes it. - -
move_to_sub and move_to_named_sub
- -void move_to_sub(irept &irep);
-void move_to_named_sub(const irep_namet &name, irept &irep);
--The first method creates a new ordered edge with a child equal to -irep. Then it sets irep to nil. The index of the -edge is equal to the size of vector sub before the call. -
- --The second method does the same but for labeled edges. -
- -swap
- -void swap(irept &irep);
--Exchange the content of the invoked node with the one of irep. -
- -make_nil
- -void make_nil();
--Set the label of the node to "nil" and remove all outgoing edges. -
- -get_sub and get_named_sub and get_comments
- -const subt &get_sub();
-const named_subt &get_named_sub();
-const named_subt &get_comments();
--Return a constant reference to -sub, named_sub, and comments, respectively. -
- -Types
- --The class typet inherits from irept. Types may have -subtypes. This is modeled with two edges named "subtype" and "subtypes". The -class typet only add specialized methods for accessing the subtype -information to the interface of irept. -
- -Interface of class typet
- -has_subtype and has_subtypes
- -bool has_subtype() const;
-bool has_subtypes() const;
--The first method returns true if the a subtype node exists. is not -nil. The second method returns true is a subtypes node exists. -
- -subtype and subtypes
- -typet &subtype();
-typest &subtypes();
--The first method returns a reference to the 'subtype' node. -The second method returns a reference to the vector of subtypes. -
- -Subtypes of typet
- -
-A number of subtypes of typet exist which allow convenient
-creation and manipulation of typet objects for special types.
-
| Class | Description |
|---|---|
bool_typet |
-Boolean type |
symbol_typet |
-Symbol type. Has edge "identifier" to a string value, which can be accessed with get_identifier and set_identifier. |
struct_typet, union_typet |
-Represent a struct, resp. union types. Convenience functions to access components components(). |
code_typet |
-The type of a function/procedure. Convenience functions to access arguments() and return_type(). |
array_typet |
-Convenience function size() to access size of the array. |
pointer_typet |
-Pointer type, subtype stores the type of the object pointed to. |
reference_typet |
-Represents a reference type, subtype stores the type of the object referenced to. |
bv_typet |
-Represents a bit vector type with variable width. |
fixed_bv_typet |
-Represents a bit vector that encodes a fixed-point number. |
floatbv_typet |
-Represents a bit vector that encodes a floating-point number. |
string_typet |
-Represents a string type. |
Source Locations
- --The class source_locationt inherits from the class irept. It -is used to store locations in text files. It adds specialized methods to -manipulate the edges named "file", "line", "column", "function". -
- -Expressions
- --The class exprt inherits from class irept. Expressions -have operands and a type. This is modeled with ordered edges for the -operands and an edge labeled"type", respectively. The class exprt -only adds specialized methods for accessing operands and type information -to the interface of irept. -
- -
Interface of class exprt
- -constructors
- -explicit exprt(const irep_idt &id);
--Creates an exprt object with a given label and no type. -
- -exprt(const irep_idt &id, const typet &type);
--Creates an exprt object with a given label and type. -
- -type
- -const typet &type() const;
-typet &type();
--Return a reference to the 'type' node -
- -has_operands
- -bool has_operands() const;
--Return true if the expression has at least one operand. -
- -operands
- -const operandst &operands() const;
--Return a reference to the vector of operands. -
- -const exprt &op0();
-const exprt &op1();
-const exprt &op2();
-const exprt &op3();
-exprt &op0();
-exprt &op1();
-exprt &op2();
-exprt &op3();
--Return a reference to a specific operand. Avoid calling -if the operand does not exist. -
- -Constructing common expressions
- -void make_true();
-void make_false();
-void make_bool(bool value);
--Turn the current exprt instance into a expression of type "bool" -with label "constant" and a single edge labeled "value", which points to -a new node with label either "true" or "false". -
- -void make_typecast(const typet &_type);
--Turns the current exprt instance into a typecast. The old value of -the instance is appended as the single operand of the typecast, i.e., the -result is a typecast-expression of the old expression to the indicated type. -
- -void make_not();
--Turns the current exprt instance into an expression with label -"not" of the same type as the original expression. The old value of the -instance is appended as the operand of the "not"-node. If the original -expression is of type "bool", the result represents the negation of the -original expression with the following simplifications possibly applied: -
- --
-
- ¬ ¬ f = f -
- ¬ true = false -
- ¬ false = true -
-void negate(); -- -
-Turns the current exprt instance into a negation of itself, depending -on its type: -
- --
-
-
- For boolean expressions,
make_notis called.
-
- - For integers, the current instance is turned into a numeric negation -expression "unary-" of its old value. Chains of "unary-" nodes and -negations of integer constants are simplified. - -
- For all other types,
irept::make_nilis called.
-
-
bool sum(const exprt &expr);
-bool mul(const exprt &expr);
-bool subtract(const exprt &expr);
-
-Expect the "this" object and the function argument to be constants of the
-same numeric type. Turn the current exprt instance into a
-constant expression of the same type, whose "value" edge points to the
-result of the sum, product, or difference of the two expressions. If the
-operation fails for some reason (e.g., the types are different),
-true is returned.
-
Testing common expressions
- -bool is_constant() const;
--Returns true if the expression label is "constant". -
- -bool is_boolean() const;
--Returns true if the label of the type is "bool". - -
bool is_false() const;
-bool is_true() const;
--The first function returns true if the expression is a boolean constant with -value "false". The second function returns true for any boolean constant -that is not of value "false". -
- -bool is_zero() const;
-bool is_one() const;
--The first function returns true if the expression represents a zero numeric -constant, or if the expression represents a null pointer. The second -function returns true if the expression represents a numeric constant with -value "1". -
- -Subtypes of exprt
- -
-A number of subtypes of exprt provide further convenience functions
-for edge access or other specialized behaviour:
-
| Class | Description |
|---|---|
transt |
-Represents an SMV-style transition system with invariants
-invar(), initial state init() and transition
-function trans(). |
-
true_exprt |
-Boolean constant true expression. | -
false_exprt |
-Boolean constant false expression. | -
symbol_exprt |
-Represents a symbol (e.g., a variable occurrence), convenience function for manipulating "identifier"-edge set_identifier and get_identifier |
-
predicate_exprt |
-Convenience constructors to create expressions of type "bool". | -
binary_relation_exprt : predicate_exprt |
-Convenience functions to create and manipulate binary expressions of type "bool". | -
equality_exprt : binary_relation_exprt |
-Convenience functions to create and manipulate equality expressions such as "a == b". | -
ieee_float_equal_exprt : binary_relation_exprt |
-Convenience functions to create and manipulate equality expressions between floating-point numbers. - | -
index_exprt |
-Represents an array access expression such as "a[i]". Convenience functions array() and index() for accessing the array expressions and indexing expression. |
-
typecast_exprt |
-Represents a cast to the type of the expression. | -
-and_exprt,
-implies_exprt,
-or_exprt,
-not_exprt |
-Representations of logical operators with convenience constructors. | -
address_of_exprt |
-Representation of a C-style &a address-of operation. Convenience function object() for accessing operand. |
-
dereference_exprt |
-Representation of a C-style *a pointer-dereference operation. Convenience function object() for accessing operand. |
-
if_exprt |
-Representation of a conditional expresion, with convenience functions cond(), true_case() and false_case() for accessing operands. |
-
member_exprt |
-Represents a some_struct.some_field member access. |
-
codet |
-Represents a segment of code. | -
Symbols and the Symbol Table
- -Symbol
- -
-A symbol is an object of class symbolt. This class
-is declared in "util/symbol.h". The code below shows a partial
-declaration of the interface:
-
class symbolt
-{
-public:
- typet type;
- exprt value;
- std::string name;
- std::string base_name;
- ...
-};
--Symbol names are unique. Scopes are handled by adding prefixes -to symbols: -
- -int main(int argc, char* argv[]) {
-
- // Symbol name: c::main::0::alice
- char alice = 0; // Symbol base: alice
-
- {
- // Symbol name: c::main::1::alice
- int alice = 0; // Symbol base: alice
- }
-}Symbol Table
- -
-A symbol table is an object of class contextt. This class
-is declared in "util/context.h". The code below shows a partial
-declaration of the interface:
-
class symbol_tablett
-{
-public:
- // Insert the symbol
- bool add(const symbolt &symb);
- // Insert symb into the
- // table and erase it.
- // New_symbol points to the
- // newly inserted element.
- bool move(symbolt &symbol, symbolt *&new_symbol);
-
- // Insert symb into the
- // table. Then symb is erased.
- bool move(symbolt &syb);
-
- // Return the entry of the
- // symbol with given name.
- const irept &value(const std::string &name) const;
-};
-Goto Programs
- --Goto programs are a representation of the control flow graph of a program -that uses only guarded goto and assume statements to model non-sequential -flow. The main definition can be found in -"src/goto-programs/goto_program_template.h", which is a template class. The -concrete instantiation of the template that is used in the framework can be -found in "src/goto-programs/goto_program.h". A single instruction in a goto -program is represented by the class goto_programt::instructiont -whose definition can be found again in -"goto-programs/goto_program_template.h". -
- -
-In the class goto_programt, the control flow graph is represented
-as a mixture of sequential transitions between nodes, and non-sequential
-transitions at goto-nodes. The sequential flow of the program is captured
-by the list instructions that is a field of the class
-goto_programt. Transitions via goto statements are represented in
-the list targets, which is a field of the class
-goto_programt::instructiont, i.e., each goto-instruction carries a
-list of possible jump destinations. The latter list targets is a
-list of iterators which point to elements of the list instructions.
-An illustration is given in the figure below.
-
-Instructions can have a number of different types as represented by
-enum goto_program_instruction_typet and can be accessed via the
-field type in instructiont. These include:
-
GOTO |
-Represents a non-deterministic branch to the instructions given in the
-list targets. Goto statements are guarded, i.e., the
-non-deterministic branch is only taken if the expression in
-guard evaluates to true, otherwise the program continues
-sequentially. Guarded gotos can be used, for example, to model if
-statements. The guard is then set to the negated condition of the
-statement, and goto target is set to bypass the conditionally executed code
-if this guard evaluates to true.
- |
-
ASSUME |
-An assumption statement that restricts viable paths reaching the
-instruction location to the ones that make the expression guard
-evaluate to true. |
-
ASSERT |
-An assertion whose guard is checked for validity when the instruction is
-reached. |
-
RETURN |
-A return statement in a function. | -
END_FUNCTION |
-Denotes the end of a function. | -
ASSIGN |
-A variable assignment. | -
SKIP |
-No operation. | -
OTHER |
-Any operation not covered by enum
-goto_program_instruction_typet. |
-
-A number of convenience functions in instructiont, such as
-is_goto(), is_assume(), etc., simplify type queries.
-The following code segment gives a partial interface declaration of
-goto_program_template and instructiont.
-
template <class codeT, class guardT>
-class goto_program_templatet
-{
-public:
- //list of instruction type
- typedef std::list<class instructiont> instructionst;
-
- //a reference to an instruction in the list
- typedef typename
- std::list::iterator targett;
-
- //Sequential list of instructions,
- //representing sequential program flow
- instructionst instructions;
-
- typedef typename
- std::map<const_targett, unsigned> target_numberst;
-
- //A map containing the unique number of each target
- target_numberst target_numbers;
-
- //Get the successors of a given instruction
- void get_successors(targett target, targetst &successors);
-
- ...
-
-
- class instructiont
- {
- public:
- codeT code;
-
- //identifier of enclosing function
- irep_idt function;
-
- //location in the source file
- locationt location;
-
- //type of instruction?
- goto_program_instruction_typet type;
-
- //Guard statement for gotos, assume, assert
- guardT guard;
-
- //targets for gotos
- targetst targets;
-
- //set of all predecessors (sequential, and gotos)
- std::set<targett> incoming_edges;
-
- // a globally unique number to identify a
- // program location. It is guaranteed to be
- // ordered in program order within one
- // goto_program
- unsigned location_number;
-
- // a globally unique number to identify loops
- unsigned loop_number;
-
- // true if this is a goto jumping back to an
- // earlier instruction in the sequential program
- // flow
- bool is_backwards_goto() const;
- };
-
-}
-