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 # "", # inlined functions from /usr/include removed # sed -i 's/\$' 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 <" ;; /usr/include/x86_64-linux-gnu/sys/+([a-z]).h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/dirent.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/fcntl2.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/ioctl-types.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/sigset.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/statfs.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/stat.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/stdio2.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/stdio.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/stdlib-float.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/string2.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/string3.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/termios.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/time.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/types.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/unistd.h) echo "#include " ;; /usr/include/x86_64-linux-gnu/bits/utmp.h) echo "#include " ;; 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/' $fn sed -i 's/\/fputs/' $fn sed -i 's/\/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 /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 /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