On Fri, Mar 19, 2010 at 5:01 PM, Stefan Bucur <stefan.bucur at epfl.ch> wrote: > On Wed, Mar 17, 2010 at 6:35 PM, Stefan Bucur <stefan.bucur at epfl.ch> wrote: >> Hello, >> >> When I run the Debug >> version of the executable, constant arrays are not reported as being >> created anymore, even though printing the symbolic state constraints >> show them as being existent. > [...] > > Another question is whether there is a straightforward way to > pretty-print the entire contents of a symbolic state (that is, its > symbolic memory), instead of printing only the constraints. That would > also be helpful in tracing the writes in the symbolic memory that lead > to the lazy-initialization of the constant concrete arrays.
Not currently. ObjectState objects do have a ::print method, but there is no way to hit it out-side a debugger, IIRC. The way I personally would like to see this done is to allow KLEE to serialize its entire state, and then have extra tools for poking around inside a serialized state. - Daniel > Stefan > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
