Hi Ott,
I'm pretty sure optimizations are not the problem.
First, "storage" has external linkage -- the compiler cannot infer that it
is not subsequently used.
Second, llvm-gcc's output for this code (even with optimizations turned
on) is a pretty obvious translation of the C code.
John
On Tue, 24 Jan 2012, Ott Tinn wrote:
Hi John,
The most obvious problem I see is that the code sample is too simple -
the compiler optimizations could also see that the value you are
storing to the storage array is never used. Since accessing array
elements that are out of bounds is undefined in C then the compiler
can optimize this away by assuming that it isn't out of bounds. To
make this example work you could try compiling without any
optimizations and without using KLEE's -optimize flag or otherwise
making sure the dangerous operations can't be optimized away.
Ott
On Tue, Jan 24, 2012 at 9:18 PM, John Regehr <[email protected]> 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
