[klee-dev] Testing Structures with klee

[Saikat Dutta]

Thanks.
But what about linked lists? If there exists a next pointer in a structure,
will it be taken care of by klee?Or do i need to fix the length of linked
list and declare every instance of that structure symbolically?I m a bit
confused.


On Thu, Oct 3, 2013 at 9:04 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> KLEE models memory at the bytes level so you can things like this...
>
> include <stdio.h>
>
> int main(int argc, char** argv)
> {
>     typedef struct
>     {
>         int a;
>         int b;
>     } A;
>
>     A instance;
>
>     klee_make_symbolic(&instance, sizeof(A));
>
>     if ( instance.a > 0 )
>         printf("instance.a >0\n");
>     else
>         printf("instance.a <=0\n");
>
> }
>
> As for "Normally big application have..." that totally depends on what
> sort of programs you are talking about. KLEE has built-in support for
> declaring symbolic command line arguments and symbolic files as
> command line arguments for convenience. You can get info on the is by
> running
>
> $ klee --posix-runtime <program>.bc --help
>
> usage: (klee_init_env) [options] [program arguments]
>   -sym-arg <N>              - Replace by a symbolic argument with length N
>   -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most
>                               MAX arguments, each with maximum length N
>   -sym-files <NUM> <N>      - Make stdin and up to NUM symbolic files, each
>                               with maximum size N.
>   -sym-stdout               - Make stdout symbolic.
>   -max-fail <N>             - Allow up to <N> injected failures
>   -fd-fail                  - Shortcut for '-max-fail 1'
>
> See the Coreutils webpage
> (http://ccadar.github.io/klee/TestingCoreutils.html) for an example of
> how to use these
>
> On 3 October 2013 15:46, Saikat Dutta <saikatdutta.pro2011 at gmail.com>
> wrote:
> > Hi,
> > Normally big application have structures and linked lists or arrays of
> such
> > structures as inputs to functions. Is there an easy way to symbolically
> > declare them using klee? Or does one have to declare each of their
> component
> > primitive variables?
> > Thanks.
> > -Saikat
>
-------------- next part --------------
HTML attachment scrubbed and removed