[klee-dev] Simple getopt example

Pablo González de Aledo pablo.aledo at gmail.com
Wed Dec 4 08:10:45 GMT 2013


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.


2013/12/4 Loi Luu <loi.luuthe at gmail.com>

> 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


More information about the klee-dev mailing list