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

Instructions to compile nanosat 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 nanosat sources and unpack the files.

    tar xfz nanosat-1.3.tar.gz

  2. Switch to the nanosat-1.3 directory

    cd nanosat-1.3

    and configure the build for debug:

    ./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 result in a final object called nanosat and a test suite called test.

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

    cbmc --binary nanosat

    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.