[klee-dev] symbolic array size

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>