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
