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

Instructions to compile bchunk to a GOTO-object

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

    tar xfz bchunk-1.2.0.tar.gz

  2. Switch to the bchunk-1.2.0 directory

    cd bchunk-1.2.0

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

    change
    CC=gcc
    to
    CC=goto-cc

    change
    LD=gcc
    to
    LD=goto-cc

    change
    CFLAGS = -Wall -Wstrict-prototypes -O2
    to
    CFLAGS = --i386-linux

  4. Make it!

    make

    This will result in a final object called bchunk.

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

    cbmc --binary bchunk

    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.