What are the inputs to the KLEE core-utils experiment discussed in the paper?

Question

I'm having trouble reproducing the results in Figure 7 of this paper:

http://www.stanford.edu/~engler/klee-osdi-2008.pdf

Specifically, I tried to test the core util's "tac" command doing so:

klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./tac.bc -r -sym-files 20 1 

However I do not see any error messages reported by KLEE, although the paper claims there should be a bug.

On the other hand, if I test core util's "md5sum" command like so:

klee.cde -max-time=60 --optimize --libc=uclibc --posix-runtime ./md5sum.bc -c -sym-files 1 10

KLEE reports the following error:

: /root/coreutils-6.10/obj-llvm/src/../../src/md5sum.c:212: memory error: out of bound pointer

Can somebody point me in the right direction to discover the bug in either "tac" or "pr" commands? Both if these require files "t2.txt" and "t3.txt" which are defined "\b\b\b\b\b\b\b\t" and "\n" respectively in the paper.

Would appreciate all / any advise.

Answer 1

You can try with a larger value for --max-time, which sets a time limit for KLEE.