Hello, let me first congratulate again on your good work here. From your answers and my experience with KLEE, your tool seems to be based upon lots of experience and deep analysis of the domain.
I'm working on comparing different implementations of functions, but in my case, each function has a whole "state" in their back (global variables, different data types and variables, etc.). As far as I understood, there is only one state for each path in KLEE. That means, however, that functional equivalence checking, as proposed in your paper, operates on the same memory, which might cause some nasty side effects. It would be good to fork the whole state for each implementation and then join again and check the differences in the two branches. Does KLEE offer a functionality to join or to compare different states? Keep up the good work, Henning
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
