[klee-dev] symbolic aggregate data structures?

[Cristian Cadar]

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
>