On Sun, May 2, 2010 at 12:14 PM, Cristian Zamfir <cristian.zamfir at epfl.ch> wrote: > > I sometimes see states terminated with the error message "concretized > symbolic size". Since this produces a test*.err file in Klee's output, I > assumed it could be related to a possible bug found by Klee. However, when > reading the source code in Executor::executeAlloc() I see that in case a > large symbolic value is possible, the execution will fork and will create one > state in which malloc() returns 0 and another state which is terminated with > this error. > > My question is what is the purpose of the second state? Does it mean there > could be a possible bug or just to highlight that there was a case in which a > symbolic size was concretized?
No, there is no possible bug. The intent is: (1) it highlights that we are getting incomplete results. (2) it records the path condition of the states that aren't going to be explored. That said, it is possible that it indicates a real bug in cases where the source probably shouldn't end up malloc'ing very large amounts of memory (e.g., using a negative signed count). - Daniel > > Thanks, > Cristi > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
