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

Instructions to compile jhead to a GOTO-object

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

    tar xfz jhead-2.6.tar.gz

  2. Switch to the jhead-2.6 directory

    cd jhead-2.6

  3. Make it (with a few variables set):

    export CC="goto-cc --i386-linux"
    make

    This will result in a final object called jhead.

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

    cbmc --binary jhead

    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.