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
