Build Systems and Libraries
Example: Extracting Models from the Linux Kernel
The Linux kernel code consists of more than 11 million lines of low-level C and is frequently used to evaluate static analysis techniques. In the following, we show how to extract models from Linux 2.6.39.
First of all, you will need to make sure you have around 100 GB of free disc space available.
Download the Kernel sources at http://www.kernel.org/pub/linux/kernel/v2.6/linux-2.6.39.tar.bz2 .
tar xvf linux-2.6.39.tar
Now ensure that you can actually compile a kernel by doing
These steps need to succeed before you can try to extract models from the kernel.
Now compile gcc-wrap.c and put the resulting binary into a directory that is in your PATH variable:
gcc gcc-wrap.c -o gcc-wrap
cp gcc-wrap ~/bin/
This assumes that the directory
~/binexists and is in your PATH variable.
Now change the variable CC in the kernel Makefile as follows:
CC = ~/bin/gcc-wrap
This will re-compile the kernel, but this time retaining the preprocessed source files.
You can now compile the preprocessed source files with goto-cc as follows:
find ./ -name .tmp_*.i > source-file-list
for a in `cat source-file-list` ; do
goto-cc -c $a -o $a.gb
Note that it is important that the word-size of the kernel configuration matches that of goto-cc. Otherwise, compile-time assertions will fail, generating the error message "bit field size is negative". For a kernel configured for a 64-bit word-width, pass the option
.gb files can be passed to any
of the CPROVER tools.