On 6 Dec 2013 01:21, "jingde liu" <[email protected]> wrote: > > Hi everyone, > > I have two questions: > > 1) The first one is about state backtracking in KLEE. I want to backtrace the current state to "n" steps before instead of the last step. How should I do it?
AFAIK KLEE does not support this. Stepping backwards is not straightforward. Things to consider: - how does Klee unfork? - how does klee know what the inverse operation of an instruction is? I think it would be possible to implement but it would be challenging! A simpler alternative is if you know what state you would need to step back to is to keep two copies of ExecutionState. The first copy you execute as normal ( forwards ). The second copy is left untouched. If you find the need to jump back then delete the first copy and then use the second copy. > 2) The second one is about path condition. I want to know the constraint of each step in the current path. How should I get this information from the current data structure? Look at the ConstraintManager inside ExecutionState. Hope that helps, Dan Liew
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
