Hi Shiyu, For --max-forks=10 the number of completed paths is 42 due to a bug: klee still forks when encountering switch statements. A patch is available at https://github.com/paulmar/klee/commit/90601a60fb6a0f22337c46680f150ec04ad3c6cb . The output should now look similar to
KLEE: done: total instructions = 154095 KLEE: done: completed paths = 11 KLEE: done: generated tests = 9 For --stop-after-n-tests=10, KLEE does stop, but generates tests for the partially explored paths before exiting. These are included in the 'completed paths' count. Paul On 24 Sep 2013, at 23:51, Shiyu Dong <[email protected]> wrote: > Hi Cristian, > > I am still confused about these two flags. For example, when trying to run > the paste.bc as showed in the tutorial, if I use --max-forks=10 I got the > following: > > KLEE: done: total instructions = 421007 > KLEE: done: completed paths = 42 > KLEE: done: generated tests = 11 > > However, if I use --stop-after-n-tests=10, I got: > > KLEE: done: total instructions = 348114 > KLEE: done: completed paths = 238 > KLEE: done: generated tests = 35 > > For testing purpose I only give it 1 minute to run. However, none of those > "completed paths" is equal to 10, and for the second case the "generated > tests" is grater than 10 also. I'm wondering if there's anything that I did > wrong. Thanks. > > 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-cex-cache \ > --libc=uclibc \ > --posix-runtime \ > --allow-external-sym-calls \ > --only-output-states-covering-new \ > --environ=test.env \ > --run-in=/tmp/sandbox \ > # --stop-after-n-tests=10 or --max-forks=10, I put one of them here. > --max-sym-array-size=4096 \ > --max-instruction-time=30. \ > --max-time=60. \ > --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 \ > --search=random-path \ > --search=nurs:covnew \ > --use-batching-search \ > --batch-instructions=10000 \ > ./paste.bc \ > --sym-args 0 1 10 \ > --sym-args 0 2 2 \ > --sym-files 1 8 \ > --sym-stdout > > Best, > Shiyu > > > On Tue, Sep 24, 2013 at 4:24 PM, Cristian Cadar <[email protected]> > wrote: > Hi Shiyu, > > > On 24/09/2013 22:06, Shiyu Dong wrote: > One more question: does KLEE has any way to limit to the number of paths to > explore? From the --help command the only possible option I see is > "-stop-after-n-tests=<uint>" because I assume each test case corresponds to > one path by observing the test results that I already have. Is that a good > assumption? > At some level, yes, but this ignores the partial paths that have not resulted > in a test case yet. Also, to avoid excessive test case generation, it is > often a good idea to use the flag -only-output-states-covering-new, which > only generates a test case when new code is covered (note that the command > line discussed before includes this flag). > > > Are there better flags to use? > If I understand correctly, what you want is actually -max-forks=<uint>. > > Best, > Cristian > > _______________________________________________ > 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
