[klee-dev] Simple getopt example

[Pablo González de Aledo]

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.
-------------- next part --------------
HTML attachment scrubbed and removed