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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
