Hi,

I tried to repeat KLEE's coreutils experiment described in 
http://klee.llvm.org/TestingCoreutils.html 
, and found it very easy to follow!

May I ask the following:

1. I modified the command line options listed in 
http://keeda.stanford.edu/pipermail/klee-dev/2009-October/000139.html 
  to use with KLEE r124536, and I'm wondering if the changes are  
correct (see below). In particular, I omitted --environ, as I don't  
know how to generate *.env. (I found 9 coreutils programs that have  
coverages below 60%, which makes me wonder if I got the command line  
options right.)

2. I have problem running klee-replay on some coreutils commands,   
e.g., the replay of "yes" does not stop at all, and it generates lots  
of output (which is expected, but the fact that it doesn't stop makes  
this a problem). Is there a way to bound the replay?

3. I tried to calculate coverages by (say paste is the program)

        cat test*.cov | grep paste | sort -u

which gives me 115 lines, instead of 88.24% of 187 given by gcov. Any  
idea about the difference?

Thanks!

Kin



Command line options:

klee \
     --simplify-sym-indices \
     --write-cvcs \
     --write-cov \
     --output-module \
     --max-memory=1000 \
     --disable-inlining \
     --optimize \
     --use-forked-stp \
     --use-cex-cache \
     --libc=uclibc \
     --posix-runtime \
     --allow-external-sym-calls \
     --only-output-states-covering-new \
     --run-in=klee-sandbox \
     --output-dir=klee-out \
     --max-sym-array-size=4096 \
     --max-instruction-time=10. \
     --max-time=3600. \
     --watchdog \
     --max-memory-inhibit=false \
     --max-static-fork-pct=1 \
     --max-static-solve-pct=1 \
     --max-static-cpfork-pct=1 \
     --switch-type=internal \
     --randomize-fork \
     --use-random-path \
     --use-interleaved-covnew-NURS \
     --use-batching-search \
     --batch-instructions 10000 \
     --init-env paste.bc \
     --sym-args 0 1 10 \
     --sym-args 0 2 2 \
     --sym-files 1 8 \
     --sym-stdout

Reply via email to