[klee-dev] Simple getopt example

[Loi Luu]

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 <
pablo.aledo at gmail.com> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>


-- 
Loi, Luu The.
-------------- next part --------------
HTML attachment scrubbed and removed