[klee-dev] Testing Structures with klee

[Daniel Liew]

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