I wanted to reproduce the Case study of Coreutils. But the version of Coreutils in the OSDI 2008' paper was too old (version 6.11), so I applied the newest version(version 8.9) using information described in KLEE Mailing list.
This is the link. http://keeda.stanford.edu/pipermail/klee-dev/2011-February/000572.html But I do not understand why the options are needed. For example, --max-memory=1000 --max-sym-array-size=4096 --batch-instructions=10000 --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 I would like to know why max-memory=1000 and max-sym-array-size=4096 like that. And for other options similarly. Especially, I cannot find the meaning of --simplify-sym-indices. But when I applied the option, the branch coverage with gcov was dramatically increased. So I analyzed the source code of KLEE, but I could not understand the exact meaning and the effect. I attached the options I applied. 1 --simplify-sym-indices \ 2 --write-cvcs \ 3 --write-cov \ 4 --write-sym-paths \ 5 --write-paths \ 6 --max-memory=1000 \ 7 --disable-inlining \ 8 --optimize \ 9 --use-forked-stp \ 10 --libc=uclibc \ 11 --posix-runtime \ 12 --allow-external-sym-calls \ 13 --only-output-states-covering-new \ 14 --output-dir=klee-out-file \ 15 --max-time=300 \ 16 ?-watchdog \ 17 --max-sym-array-size=4096 \ 18 --max-instruction-time=10. \ 19 --max-memory-inhibit=false \ 20 --switch-type=internal \ 21 --randomize-fork \ 22 --use-random-path \ 23 --use-interleaved-covnew-NURS \ 24 --use-batching-search \ 25 --batch-instructions=10000 \ 26 --init-env \ 27 /~/coreutils-8.9/obj-llvm/src/file.bc \ 28 --sym-args 0 1 10 \ 29 --sym-args 0 2 2 \ 30 --sym-files 1 8 \ 31 --sym-stdout Thanks. -YJ -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110629/6d62844a/attachment.html
