[klee-dev] question about -max-time flag

[Shiyu Dong]

Hello,

I have a question about how the -max-time flag should be used. I ran the
coreutil test using the following command and set the max time to 600
seconds. However, when I tried to print out the result using klee-stats the
time cost is 717.57 seconds. I'm wondering where does the extra time come
from? Is that costed by generating the test cases, or simply by halting the
program?

Here's the command that I used:

klee \

--simplify-sym-indices \
--write-cvcs \
--write-cov \
--output-module \
--max-memory=1000 \
--disable-inlining \
--use-forked-solver \
--use-cache=false \
--use-cex-cache=false \
--libc=uclibc \
--posix-runtime \
--allow-external-sym-calls \
--only-output-states-covering-new \
--environ=../test.env \
--run-in=/tmp/sandbox \
--max-sym-array-size=4096 \
--max-instruction-time=30. \
--watchdog \
--max-time=600. \
--max-memory-inhibit=false \
--max-static-fork-pct=1 \
--max-static-solve-pct=1 \
--max-static-cpfork-pct=1 \
--switch-type=internal \
--randomize-fork \
--search=random-path \
--search=nurs:covnew \
--use-batching-search \
--batch-instructions=10000" \
base64.bc \
--sym-args 0 1 10 \
--sym-args 0 2 2 \
--sym-files 1 8 \
--sym-stdout"

Thanks,
Shiyu
-------------- next part --------------
HTML attachment scrubbed and removed