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

Instructions to compile limmat to a GOTO-object

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

    tar xfz limmat-1.3.tar.gz

  2. Switch to the limmat-1.3 directory

    cd limmat-1.3

    and configure the build for a debug build:

    ./configure -g

  3. Switching the build to goto-cc requires the Makefile to be changed:

    change
    CC=gcc
    to
    CC=goto-cc --i386-linux

  4. Make it!

    make

    This will produce a few warnings about long string constants, which is not a problem. The result is a final object called limmat.

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

    cbmc --binary limmat

    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.