CPROVER Manual TOC
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
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.
This example assumes a Unix-like machine.
Download the sources of wu-ftpd from here.
Unpack the sources by running
tar xfz wu-ftpd-current.tar.gz
Change to the source directory, by entering, e.g.,
Configure the project for verification by running
./configure YACC=byacc CC=goto-cc --host=none-none-none
Build the project by running
This creates multiple model files in the
src directory. Among
them is a model for the main executable
Run a model-checker, e.g., CBMC, on the model file:
CBMC automatically recognizes that the file is a goto binary.
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
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
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
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.
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
ld tool present on most Unix (-based) systems and
link tool on Windows.
The default linker may need to be replaced by
goto-link.exe in the build
script, which can be achieved in much the same way as replacing the compiler.