[klee-dev] Collect functions and values of parameters

[DAVID LIGHTSTONE]

I suspect not always. The reason being that the involving call may not be on the stack. 
Quite likely the library call will be somewhere between two KLEE branch fork invocations.

For your example where the involving call is in the conditional, the answer is yes.

This suggests that the library will need to be modified so as to output to a trace file the argument lists that you wish to capture ; A lot of work. The effort has a definite recursion to avoid; the various print procedures use the library also

There are code translation systems such as ROSE which probably can automate the modification effort, but there is a nontrivial effort needed to learn them. 

Dave Lightstone
-------------- next part --------------
HTML attachment scrubbed and removed