[klee-dev] symbolic aggregate data structures?

[Mark R. Tuttle]

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
-------------- next part --------------
HTML attachment scrubbed and removed