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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
