goto-cc Homepage Compiling GOTO-Programs
About -- Download -- Examples -- Documentation

Instructions to compile sendmail to a GOTO-object

Latest version of example sources known to work: 8.13.8
Latest version of goto-cc known to work on this example: 2.5
  1. Download the sendmail sources and unpack the files.

    tar xfz sendmail.8.13.8.tar.gz

  2. Switch to the sendmail-8.13.8 directory:

    cd sendmail-8.13.8

    and configure the build like this:
  3. sendmail does not have a configure script, instead a build configuration file must be created in devtools/Site/site.config.m4. To extract a goto-object for the Linux version, it should look like this:

    include(confBUILDTOOLSDIR`/OS/Linux')
    define(`confDEPEND_TYPE', `generic')

    define(`confCC', `goto-cc --i386-linux')
    define(`confLD', `goto-ld')
    define(`confCCOPTS', `-DSM_ALIGN_SIZE=4')

  4. Build it!

    ./Build -c

    This will result in multiple (goto-) binaries and libraries in a subdirectory corresponding to your operating system and architecture, e.g., obj.Linux.2.6.17-10-generic.i686.

  5. Try to verify the program by using the final object file in CBMC or SATABS:

    cbmc --binary obj.Linux.2.6.17-10-generic.i686/sendmail/sendmail

    Of course you will need different options if you want to check the program for a special claim or if you're using a different tool.