btw, PEX(symbolic unit test framework for MS .net family) can handle the
similar case.
Try the following code snippet from http://www.pexfun.com.
using System;
public class Program {
public static int Puzzle(int i, int v) {
int[] indices = {0,2,1,5,3,0,-77,0,3,6};
int[] storage = new int[7];
int index = indices[i];
storage[index] = v;
return index;
}
}
On Jan 24, 2012, at 4:18 PM, John Regehr wrote:
> Perhaps interesting to people here:
>
> http://blog.regehr.org/archives/672
>
> While writing this up I discovered that when "i" is symbolic Klee cannot
> find a value for i that makes this code access an OOB array element:
>
> int indices[] = { 0,2,1,5,3,0,-77,0,3,6 };
>
> value_t storage[7];
>
> void stash (int i, value_t v)
> {
> if (i<0 || i>=10) {
> error();
> } else {
> int index = indices[i];
> // assert (index>=0);
> // assert (index<7);
> storage[index] = v;
> }
> }
>
> On the other hand, given the assertions, Klee generates the test case where
> i==6.
>
> I infer that Klee does not automatically assert in-boundedness of array
> accesses. But these assertions seem obviously desirable, so I'm trying to
> figure out why not. Maybe Klee doesn't have enough runtime information to
> make this happen?
>
> John
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
