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
