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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
