I think you can use the argument -only-output-states-covering-new to generate only new paths. It doesn't prevent KLEE from exploring visited paths but from printing them again.
Thanks, On Tue, Dec 3, 2013 at 11:37 PM, Pablo González de Aledo < [email protected]> wrote: > Hi. > > I'm trying a simple example with getopt and klee: > > int main (int argc, char **argv) { > int aflag = 0; > int c; > > while ((c = getopt (argc, argv, "abc:")) != -1) > switch (c) > { > case 'a': > aflag = 1; > break; > default: > fprintf (stderr, "Unknown option character.\n"); > } > > return 0; > } > > > When I run this program with > > klee --only-output-states-covering-new --optimize --libc=uclibc > --posix-runtime ./file.bc --sym-args 0 2 4 > > I would expect to obtain a number of paths in the order of less than a > hundred (from 0 to 2 arguments, being each of them -a or different to -a). > However, after 5 minutes running, klee has generated more than 2000 paths > and It seems nothing prevents him to continue exploring new ones. > > I understand that the internals of getopt are complex, and the number of > paths grows so much because of this, but is there any way to reduce the > number of paths generated in this example?. > If not, can I at least avoid the infinite loop, which will probably not > produce any useful error, and concentrate on the code that comes after it?. > As most part of the coreutils examples starts getting the options from > command line, this behavior looks really strange for me. > > Thanks. > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > -- Loi, Luu The.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
