Build Systems and Libraries

Example: Extracting Models from the Apache HTTPD

The Apache HTTPD is still the most frequently used web server. Together with the relevant libraries, it consists of around 0.4 million lines of C code. In the following, we show how to extract models from Apache HTTPD 2.4.2.

  1. First of all, we download the sources of Apache HTTPD and two supporting libraries and uncompress them:

      lwp-download http://www.mirrorservice.org/sites/ftp.apache.org/apr/apr-1.4.6.tar.bz2
      lwp-download http://www.mirrorservice.org/sites/ftp.apache.org/apr/apr-util-1.4.1.tar.bz2
      lwp-download http://mirror.catn.com/pub/apache/httpd/httpd-2.4.2.tar.bz2

      bunzip2 < apr-1.4.6.tar.bz2 | tar x
      bunzip2 < apr-util-1.4.1.tar.bz2 | tar x
      bunzip2 < httpd-2.4.2.tar.bz2 | tar x

  2. 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.

  3. We now build the sources with gcc:

      (cd apr-1.4.6; ./configure; make CC=gcc-wrap)
      (cd apr-util-1.4.1; ./configure --with-apr=../apr-1.4.6 ; make CC=gcc-wrap)
      (cd httpd-2.4.2; ./configure --with-apr=../apr-1.4.6 --with-apr-util=../apr-util-1.4.1 ; make CC=gcc-wrap)

  4. You can now compile the preprocessed source files with goto-cc as follows:

      find ./ -name *.i > source-file-list
      for a in `cat source-file-list` ; do
        goto-cc -c $a -o $a.gb

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