These benchmarks were generated from busybox 1.22.0 using the script provided
below. It uses object files generated by building busybox using goto-cc.


#!/bin/bash

set -e

get_line()
{
  local dest=$1
  local pat=$2

  shift 2

  for l in `grep -n "$pat" $dest | cut -f1 -d:` ; do
    for o in $@ ; do
      RM_LINES+=";$(($l + $o))d;$(($l + $o + 1))s/^/ /"
    done
  done
}

mkdir -p done
shopt -s extglob

for f in *.o ; do
  bn=`basename $f .o`
  fn=$bn.c
  if [ -e done/${bn}_unknown-unreach-call.c ] ; then
    continue
  elif \
       [ x$bn = xdf ] || \
       [ x$bn = xfalse ] || \
       [ x$bn = xmd5_sha1_sum ] || \
       [ x$bn = xmknod ] || \
       [ x$bn = xsort ] || \
       [ x$bn = xtest_ptr_hack ] || \
       [ x$bn = xtr ] || \
       [ x$bn = xtrue ] \
        ; then
    continue
  fi

  /srv/mt/cbmc-trunk/src/goto-instrument/goto-instrument \
    --bounds-check --div-by-zero-check --pointer-check \
    $f $f.instr
  /srv/mt/cbmc-trunk/src/goto-instrument/goto-instrument \
    --dump-c $f.instr $fn
  
  RM_LINES=""

  get_line $fn 'assert(.*INVALID-POINTER' 0 -1
  get_line $fn 'assert(.*POINTER_OBJECT' 0 -1
  get_line $fn 'assert(.*POINTER_OFFSET' 0 -1
  get_line $fn '__CPROVER_dead_object =' 0
  
  sed -i "$RM_LINES" $fn
  
  sed -i '/^struct _IO_FILE$/,/^};$/d' $fn
  sed -i '/^struct _IO_marker$/,/^};$/d' $fn
  sed -i '/^struct tm$/,/^};$/d' $fn
  sed -i '/^struct timespec$/,/^};$/d' $fn
  sed -i '/^struct stat$/,/^};$/d' $fn
  sed -i '/^struct __jmp_buf_tag$/,/^};$/d' $fn
  sed -i '/^struct option$/,/^};$/d' $fn
  sed -i '/^struct passwd$/,/^};$/d' $fn
  sed -i '/^struct mntent$/,/^};$/d' $fn
  sed -i '/^struct dirent$/,/^};$/d' $fn
  sed -i '/^union sigval$/,/^};$/d' $fn
  sed -i '/^struct sigaction$/,/^};$/d' $fn
  sed -i '/^struct re_pattern_buffer$/,/^};$/d' $fn
  sed -i '/^struct group$/,/^};$/d' $fn
  sed -i '/^struct termios$/,/^};$/d' $fn
  sed -i '/^struct winsize$/,/^};$/d' $fn
  sed -i '/^struct timeval$/,/^};$/d' $fn
  sed -i '/^struct utsname$/,/^};$/d' $fn
  sed -i '/^struct exit_status$/,/^};$/d' $fn
  sed -i '/^struct utmp$/,/^};$/d' $fn
  
  sed -i '/^struct llist_t$/,/^};$/d' $fn
  sed -i '/^struct suffix_mult$/,/^};$/d' $fn
  sed -i '/^struct uni_stat_t$/,/^};$/d' $fn

  sed -i 's/^\/\/ file \(.*\) line \(.*\)/# \2 "\1"/' $fn

  # libbb-dump.i is generated by dump-c from ../libbb/[b-z]*.o and manual modifications:
  # all symbols marked static,
  # // file ... markers replaced by # <line> "<file>",
  # inlined functions from /usr/include removed
  # sed -i 's/\<anonymous/libbb_anonymous/g'
  /srv/mt/cbmc-trunk/src/goto-cc/goto-cc \
    --function ${bn}_main -funsigned-char -include libbb-dump.i $fn -o $f.linked
  /srv/mt/cbmc-trunk/src/goto-instrument/goto-instrument \
    --dump-c $f.linked $fn
  rm $f.instr $f.linked
  
  RM_LINES=""

  get_line $fn '^// c::' 0

  get_line $fn '^#define FENCE' -1 0 1
  get_line $fn '^#define IEEE' -1 0 1
  get_line $fn '^#include <assert.h>$' 0

  sed -i "s/^signed int ${bn}_main(signed int argc, char \*\*argv)$/signed int main(signed int argc, char **argv)/" $fn
  get_line $fn "${bn}_main(" 0 -1
  get_line $fn "^// main" 0 1

  cat > headers <<EOF
/*
   This package is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; version 2 dated June, 1991.

   This package is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this package; if not, write to the Free Software
   Foundation, Inc., 51 Franklin St, Fifth Floor, Boston,
   MA 02110-1301, USA.
*/
extern void __VERIFIER_error(void);
EOF

  for i in `grep "^// file /usr/include" $fn | awk '{ print $3 }'` ; do
    case $i in
      /usr/include/+([a-z]).h) echo "#include <`basename $i`>" ;;
      /usr/include/x86_64-linux-gnu/sys/+([a-z]).h) echo "#include <sys/`basename $i`>" ;;
      /usr/include/x86_64-linux-gnu/bits/dirent.h) echo "#include <dirent.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/fcntl2.h) echo "#include <fcntl.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/ioctl-types.h) echo "#include <sys/ioctl.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/sigset.h) echo "#include <signal.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/statfs.h) echo "#include <sys/stat.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/stat.h) echo "#include <sys/stat.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/stdio2.h) echo "#include <stdio.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/stdio.h) echo "#include <stdio.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/stdlib-float.h) echo "#include <stdlib.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/string2.h) echo "#include <string.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/string3.h) echo "#include <string.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/termios.h) echo "#include <termios.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/time.h) echo "#include <time.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/types.h) echo "#include <sys/types.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/unistd.h) echo "#include <unistd.h>" ;;
      /usr/include/x86_64-linux-gnu/bits/utmp.h) echo "#include <utmp.h>" ;;
    esac
  done | sort | uniq >> headers
  get_line $fn "^// file /usr/include/[a-z]*\.h" 0 1
  get_line $fn "^// file /usr/include/x86_64-linux-gnu/sys/[a-z]*\.h" 0 1
  get_line $fn "^// file /usr/include/x86_64-linux-gnu/bits/[a-z0-9]*\.h" 0 1

  sed -i 's/\<putchar_unlocked\>/putchar/' $fn
  sed -i 's/\<fputs_unlocked\>/fputs/' $fn
  sed -i 's/\<getc_unlocked\>/getc/' $fn

  sed -i "$RM_LINES" $fn
  cat $fn >> headers
  mv headers $fn

  sed -i '/^struct _IO_FILE$/,/^};$/d' $fn
  sed -i '/^struct _IO_marker$/,/^};$/d' $fn
  sed -i '/^struct tm$/,/^};$/d' $fn
  sed -i '/^struct timespec$/,/^};$/d' $fn
  sed -i '/^struct stat$/,/^};$/d' $fn
  sed -i '/^struct __jmp_buf_tag$/,/^};$/d' $fn
  sed -i '/^struct option$/,/^};$/d' $fn
  sed -i '/^struct passwd$/,/^};$/d' $fn
  sed -i '/^struct mntent$/,/^};$/d' $fn
  sed -i '/^struct dirent$/,/^};$/d' $fn
  sed -i '/^union sigval$/,/^};$/d' $fn
  sed -i '/^struct sigaction$/,/^};$/d' $fn
  sed -i '/^struct re_pattern_buffer$/,/^};$/d' $fn
  sed -i '/^struct group$/,/^};$/d' $fn
  sed -i '/^struct termios$/,/^};$/d' $fn
  sed -i '/^struct winsize$/,/^};$/d' $fn
  sed -i '/^struct timeval$/,/^};$/d' $fn
  sed -i '/^struct utsname$/,/^};$/d' $fn
  sed -i '/^struct exit_status$/,/^};$/d' $fn
  sed -i '/^struct utmp$/,/^};$/d' $fn

  sed -i '/^ {$/,/^}$/d' $fn
  sed -i 's/^ \/\//\/\//' $fn
  sed -i '/^ void main/,/^ }$/d' $fn
  sed -i 's/^[[:space:]]\+$//' $fn

  sed -i 's/\(vasprintf\|memmove\|strcpy\|syslog\|stat\)\$link[[:digit:]]\+/\1/g' $fn
  sed -i 's/\(memset\|getc\|open\|read\|memcpy\|putchar\)\$link[[:digit:]]\+/\1/g' $fn
  sed -i 's/\(sprintf\|fprintf\|atoi\)\$link[[:digit:]]\+/\1/g' $fn

  if gcc $fn ; then
    cat -s $fn | \
      sed '/^#include <assert.h>/d' | \
      sed 's/assert((_Bool)0)/__VERIFIER_error()/' \
      > done/${bn}_unknown-unreach-call.c
    rm $fn
  elif gcc -c $fn -o foo.o ; then
    cat -s $fn | \
      sed '/^#include <assert.h>/d' | \
      sed 's/assert((_Bool)0)/__VERIFIER_error()/' \
      > done/${bn}-incomplete_unknown-unreach-call.c
    rm $fn
  fi
  rm -f a.out foo.o
done