Hello All,
I'm studying the source code and now get a confusing question.
Does KLEE need to run the concrete execution when running symbolic
execution? If so, is it right that the concrete value which STP computes
is taken as the input of the next state? Well, if it's right, how does
KLEE get the concrete value, in which function?
Maybe What I said is not clear. Allow me to take a simple example.
if (x == 1) {...}
else {...}
KLEE will generate a condition to query STP, then does it store the
concrete value which STP backs and take it as an input to execute
else-branch or then-branch?
I'm really confused and hope someone can help me. Thanks very much!
Regards,
--
Lu Huizhi
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
