[klee-dev] symbolic array size

[Eva May]

Dear all,

I would like to know whether KLEE can handle array sizes symbolically.

In 2009 Mauro asked why the following code crashes with a "concretized
symbolic size" error.

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

Back then Daniel Dunbar suggested "Currently the best option is to use an
arbitrary upper bound, and assert (or klee_assume) that N is less than that
bound."

So I tried to use klee_assume:

int main(){
  int n;
  klee_make_symbolic(&n, sizeof(n), "n");
  klee_assume(n >= 0);
  klee_assume(n <= 10); // my upper bound
  int a[n];
  klee_make_symbolic(a, sizeof(a), "a");
  return actual_method(n);
}

int actual_method(int n){
  if(n == 4)
  \\ the interesting branch!
    return 0;
  else:
    return 1;
}

The klee_assume  now makes sure that the array size is between 0 and 10.
However, I still get a "concretized symbolic size" error and KLEE does not
reach the branch where n equals 4.

I had hoped that KLEE would be able to deduce that n has to be 4 (and the
array would thus be of size 4). As this is not the case, I assume that
array sizes are never really symbolic - or am I missing something?

Thank you for your help,

Eva
-------------- next part --------------
HTML attachment scrubbed and removed