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

Instructions to compile libssh2 to a GOTO-object

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

    tar xfz libssh2-0.14.tar.gz

  2. Switch to the libssh2-0.14 directory

    cd libssh2-0.14

    and configure the build like this:

    ./configure CC="goto-cc --i386-linux" --without-libz LIBSSH2_LIBZ_DIR="" --host=none-none-none

    Note: The configure script for libssh2 has a bug, it puts an excess /usr/include into the CFLAGS. Open Makefile and src/Makefile: Line 10 reads
    CFLAGS = -c /usr/include -I/usr/include -Iinclude/ -Wall
    Remove the excess path to make it read
    CFLAGS = -c -I/usr/include -Iinclude/ -Wall
  3. Make it!

    make

    The result will be a file called libssh2.so which contains all the libssh2 code in goto-object form.

  4. Make the example code that comes with libssh2

    make sample

    This compiles the libssh2 sample. The result is again a goto-object, this time called ssh2_sample. This binary can be verified for bugs by passing it to tools like CBMC or SATABS.

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

    cbmc --binary ssh2_sample

    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.