CPROVER Manual TOC
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
exists 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.