[klee-dev] Reusing results of symbolic analysis

[Andreas Wilhelm]

Hi,

I was wondering whether there is a way to reuse the results of symbolic analysis within the same program run.
Concretely, I would like to do following:

	1. Collect a set of function pointers from the user. The corresponding functions may contain klee_make_symbolic instructions.
	2. Execute each function in the set with usage of symbolic analysis. This gives me some test-runs with different input values.
	3. Execute the set of functions again with the concrete input values, but now in parallel (pthreads usage enabled by cloud9).

Do I have to use different execution states for this?
In case of I have to modify the klee/cloud9 implementation, where would be a good start-point?

Thank you in advance,

Andreas