Hi Shiyu, I'm not sure, whether that would be helpful, but I've noticed that dumping states takes some time. I personally use --dump-states-on-halt=false option. Maybe that would make your execution time closer to --max-time?
Hope that helps, Best regards, Tomek On 04/10/13 15:53, Shiyu Dong wrote: > 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 > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
