David, Thank you for the hint! Indeed, ASLR was the cause of discrepancies between assembly.ll files. Now the files are perfectly identical from one Klee run to another. Unfortunately, this doesn't solve my problem with broken replays, so I'll have to dig deeper in the file model code and see what are the real causes.
Cheers, Stefan On Tue, Mar 16, 2010 at 6:05 PM, David A. Ramos <daramos at stanford.edu> wrote: > Hi Stefan, > > There are variations in the linking process from run to run based on Linux > address space layout randomization. I think the issue is actually on the LLVM > side. Try turning ASLR off (setarch `arch` -R klee ...) and see if that > resolves your issue. > > -David > > On Mar 16, 2010, at 6:53 AM, Stefan Bucur wrote: > >> Greetings, >> >> While trying to figure out some path replay problems that I mentioned >> in a previous mail, I discovered that Klee, run twice with the same >> program input, generates different assembly.ll files. The differences >> lie mostly in the LLVM debugging information, the ordering of some >> functions in the file, and the name of some constant strings. Does >> that mean that the generated Module objects are different? If so, does >> it affect the shape of the symbolic tree (in my case, it might explain >> the replay problems)? >> >> Thanks, >> Stefan >> _______________________________________________ >> klee-dev mailing list >> klee-dev at keeda.stanford.edu >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
