On Wed, Mar 17, 2010 at 10:35 AM, Stefan Bucur <stefan.bucur at epfl.ch> wrote: > Hello, > > I'm trying to track klee::Array object creation in Klee by printing > some output from the Array constructor. I was surprised to notice that > constant arrays (the ones that get a const_arr* name) show up in my > output only when Klee is compiled as Release. 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.
Nope, I don't know why this would happen, unless your code to print them has some kind of undefined behavior. In general I don't conditionalize code based on the mode it is built in, except for occasional performance tradeoffs. Note that compiling the *runtime* library Debug vs Release will of course have some impact on how the programs execute. > Do you have any idea why is this happening? More over, what is the > reason for having lazy initialization for constant arrays? (this is > what happens as far as I studied the code) Lazy initialization is done because KLEE is optimized assuming that many objects will never become symbolic. In that case, its useful to avoid the overhead of worrying about symbolic values. At least at one point in time, KLEE was actually a faster LLVM interpreter (i.e., just running regular code, without symbolic values) than the LLVM interpreter 'lli' (although that isn't particularly hard to do). - Daniel > Many thanks, > Stefan Bucur > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
