CPROVER Manual TOC

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.

  1. First of all, you will need to make sure you have around 100 GB of free disc space available.

  2. Download the Kernel sources at http://www.kernel.org/pub/linux/kernel/v2.6/linux-2.6.39.tar.bz2 .

  3. Now do

      bunzip2 linux-2.6.39.tar.bz2
      tar xvf linux-2.6.39.tar
      cd linux-2.6.39

  4. Now ensure that you can actually compile a kernel by doing

      make defconfig
      make

    These steps need to succeed before you can try to extract models from the kernel.

  5. Now compile gcc-wrap.c and put the resulting binary into a directory that is in your PATH variable:

      lwp-download http://www.cprover.org/cprover-manual/gcc-wrap.c
      gcc gcc-wrap.c -o gcc-wrap
      cp gcc-wrap ~/bin/

    This assumes that the directory ~/bin exists and is in your PATH variable.

  6. Now change the variable CC in the kernel Makefile as follows:

      CC = ~/bin/gcc-wrap

  7. Now do

      make clean
      make

    This will re-compile the kernel, but this time retaining the preprocessed source files.

  8. 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
      done

    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 --64 to goto-cc.

The resulting .gb files can be passed to any of the CPROVER tools.