[klee-dev] symbolic aggregate data structures?

[Mark R. Tuttle]

Thanks, that's great.  I'm also seeking assurance, I guess, that I'm not
missing semantic or performance distinctions of significance among

  int a[2];
  klee_make_symbolic(&a,sizeof(a),"a");

and

  int a[2];
  a[0] = klee_int("a0");
  a[1] = klee_int("a1");

and

  int a[2];
  for (int i=0; i<2; i++) { a[i] = klee_int("a"); }

Thanks,
Mark



On Mon, Mar 31, 2014 at 11:22 AM, Cristian Cadar <c.cadar at imperial.ac.uk>wrote:

> This is a presentation issue, so the best solution would be to extend the
> ktest-tool (a small program written in Python) to output data in the
> desired format.  I would be happy to consider such a patch.
>
> Best,
> Cristian
>
>
> On 31/03/14 02:57, Mark R. Tuttle wrote:
>
>> What is the "right" way to assign symbolic values to aggregate data
>> structures like arrays?
>>
>> If I run klee on
>>
>> main() {
>>    int a[2];
>>    klee_make_symbolic(&a,sizeof(a),"a");
>>    return 0;
>> }
>>
>> then "ktest-tool --write-ints" displays the array in a rather
>> user-unfriendly way:
>>
>> num objects: 1
>> object    0: name: 'a'
>> object    0: size: 8
>> object    0: data: '\x00\x00\x00\x00\x00\x00\x00\x00'
>>
>> If I run klee on
>>
>> main(){
>>    int a[2];
>>    klee_make_symbolic(&a[0],sizeof(a[0]),"a0");
>>    klee_make_symbolic(&a[1],sizeof(a[1]),"a1");
>>    return 0;
>> }
>>
>> then klee seems to complain that I'm calling klee_make_symbolic with a
>> pointer into an array and a size that is not the size of the array:
>>
>> KLEE: ERROR: /nfs/site/home/mrtuttle/shr/uefi/ddt/q1/demo2.c:3: wrong
>> size given to klee_make_symbolic[_name]
>>
>> If I run klee on
>>
>> main(){
>>    int a[2];
>>    a[0] = klee_int("a0");
>>    a[1] = klee_int("a1");
>>    return 0;
>> }
>>
>> then "ktest-tool --write-ints" displays the array fairly nicely,
>>
>> num objects: 2
>> object    0: name: 'a0'
>> object    0: size: 4
>> object    0: data: 0
>> object    1: name: 'a1'
>> object    1: size: 4
>> object    1: data: 0
>>
>> This seems the best solution.  But is there a way to extend this to
>> integers of size other than four bytes, to characters, character strings
>> (so that strings print as strings), etc?
>>
>> Thanks,
>> Mark
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed