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.

[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 <

Post by Pablo González de Aledo
Hi.
int main (int argc, char **argv) {
int aflag = 0;
int c;
while ((c = getopt (argc, argv, "abc:")) != -1)
switch (c)
{
aflag = 1;
break;
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Pablo González de Aledo]

I am actually using this parameter, and I want to avoid paths regardless of
the fact that they have been visited before or not. I suppose the "problem"
might be related with the function getopt not detecting effectively the
number of parameters given from command line, but I don't know how to avoid
this.

Thanks.

Post by 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 <

Post by Pablo González de Aledo
Hi.
int main (int argc, char **argv) {
int aflag = 0;
int c;
while ((c = getopt (argc, argv, "abc:")) != -1)
switch (c)
{
aflag = 1;
break;
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

--
Loi, Luu The.