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

Instructions to compile inn to a GOTO-object

Latest version of example sources known to work: 2.4.3
Latest version of goto-cc known to work on this example: 2.5.1
  1. Download the inn sources and unpack the files.

    tar xfz inn-2.4.3.tar.gz

  2. Switch to the inn-2.4.3 directory

    cd inn-2.4.3

    and configure the build like this:

    1. Create a site configuration file called config.site containing this:

      CC=goto-cc
      CFLAGS=--i386-linux
      LD=goto-ld
      ac_cv_search_dbm_open=no
      inn_cv_func_mmap=yes
      inn_cv_struct_sockaddr_sa_len=no
      inn_cv_macro_iov_max=1024
      ac_cv_func_strlcpy=no
      ac_cv_func_strlcat=no
      ac_cv_func_pread=no
      ac_cv_func_pwrite=no
      inn_cv_sa_len_macro=no
      ac_cv_search_setproctitle=no
      ac_cv_func_pstat=no

      (These are some options that configure can't find out when cross-compiling.)

    2. Configure it!

      export CONFIG_SITE=config.site;
      ./configure --host=none-none-none

  3. Make it!

    make

    The result will be a file called innd/innd (the main server application) and bunch of support binaries in the various directories.

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

    cbmc --binary innd/innd

    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.