[klee-dev] Testing Structures with klee

[Daniel Liew]

KLEE isn't great with completely symbolic link lists. The pointer
could point to **anything** so in order to be complete KLEE must
consider every object allocated in memory. This does not scale very
well.



On 3 October 2013 18:06, Saikat Dutta <saikatdutta.pro2011 at gmail.com> wrote:
> 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
>
>