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

Instructions to compile wu-ftpd to a GOTO-object

Latest version of example sources known to work: 2.6.2
Latest version of goto-cc known to work on this example: 2.5
  1. Warning: wu-ftpd requires BYACC. Recent versions of YACC or BISON will not work! Before trying to compile wu-ftpd, make sure you have BYACC installed.
  2. Download the wu-ftpd sources and unpack the files.

    tar xfz wu-ftpd-current.tar.gz

  3. Switch to the wu-ftpd-2.6.2 directory

    cd wu-ftpd-2.6.2

    and configure the build like this:

    ./configure YACC=byacc CC="goto-cc --i386-linux" LD=goto-ld --host=none-none-none

  4. Make it!

    make

    The result will be a file called ftpd (the main server application) and support binaries called ftpshut, ftpcount, ftprestart and ckconfig in the src directory.

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

    cbmc --binary src/ftpd

    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.