CPROVER Manual TOC

Build Systems and Libraries

Integration into Build Systems with goto-cc

Existing software projects usually do not come in a single source file that may simply be passed to a model checker. They rather come in a multitude of source files in different directories and refer to external libraries and system-wide options. A build system then collects the configuration options from the system and compiles the software according to build rules.

The most prevalent build tool on Unix (-based) systems surely is the make utility. This tool uses build rules given in a Makefile that comes with the software sources. Running software verification tools on projects like these is greatly simplified by a compiler that first collects all the necessary models into a single model file. goto-cc is such a model file extractor, which can seamlessly replace gcc and cl.exe in Makefiles. The normal build system for the project may be used to build the software, but the outcome will be a model file with suitable detail for verification, as opposed to a flat executable program. Note that goto-cc comes in different variants depending on the compilation environment. These variants are described here.

Example: Building wu-ftpd

This example assumes a Unix-like machine.

  1. Download the sources of wu-ftpd from here.

  2. Unpack the sources by running tar xfz wu-ftpd-current.tar.gz

  3. Change to the source directory, by entering, e.g., cd wu-ftpd-2.6.2

  4. Configure the project for verification by running

    ./configure YACC=byacc CC=goto-cc --host=none-none-none
  5. Build the project by running make. This creates multiple model files in the src directory. Among them is a model for the main executable ftpd.

  6. Run a model-checker, e.g., CBMC, on the model file:

    cbmc src/ftpd

    CBMC automatically recognizes that the file is a goto binary.

Important Notes

More elaborate build or configuration scripts often make use of features of the compiler or the system library to detect configuration options automatically, e.g., in a configure script. Replacing gcc by goto-cc at this stage may confuse the script, or detect wrong options. For example, missing library functions do not cause goto-cc to throw an error (only to issue a warning). Because of this, configuration scripts sometimes falsely assume the availability of a system function or library.

In the case of this or similar problems, it is more advisable to configure the project using the normal routine, and replacing the compiler setting manually in the generated Makefiles, e.g., by replacing lines like CC=gcc by CC=goto-cc.

A helpful command that accomplishes this task successfully for many projects is the following:

for i in `find . -name Makefile`; do
  sed -e 's/^\(\s*CC[ \t]*=\)\(.*$\)/\1goto-cc/g' -i $i
done

Here are additional examples on how to use goto-cc:

A description of how to integrate goto-cc into Microsoft's Visual Studio is here.

Linking Libraries

Some software projects come with their own libraries; also, the goal may be to analyze a library by itself. For this purpose it is possible to use goto-cc to link multiple model files into a library of model files. An object file can then be linked against this model library. For this purpose, goto-cc also features a linker mode.

To enable this linker mode, create a link to the goto-cc binary by the name of goto-ld (Linux and Mac) or copy the goto-cc binary to goto-link.exe (Windows). The goto-ld tool can now be used as a seamless replacement for the ld tool present on most Unix (-based) systems and for the link tool on Windows.

The default linker may need to be replaced by goto-ld or goto-link.exe in the build script, which can be achieved in much the same way as replacing the compiler.