Hi Eva,
KLEE cannot handle arrays of symbolic size. However, what might help
(and I believe this is what Daniel was suggesting too) is to use an
upper bound for the array size, e.g, in your case use "int a[10]".
Cristian
On 02/04/13 14:41, Eva May wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
