Hi Denis, The non-deterministic behavior that you see in your runs is most likely caused by the addresses returned by malloc(). I think there was a previous thread on the list which discussed possible solutions to this, let me know if you have trouble finding it in the archives.
Best, Cristian On 01/09/10 16:37, Bueno, Denis wrote: > Hello, > > I'm trying to run some tests in Klee and I'd like to be able to get > deterministic runs of Klee. I think I've found all relevant sources of > non-determinism, and it appears to me that Klee should run deterministically, > but it doesn't. Essentially, I've verified that srand, srandom, and other > pseudo-random seeds are all constant. > > What are the other sources of non-determinism? Is it easy to remove them and > stick with pseudo-randomness? > > Thanks. > > -Denis > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
