[klee-dev] Set precondition for symbolic execution

[Pengfei Sun]

Hi All,

I wonder how to set precondition for klee to do symbolic execution?

For example, I firstly choose several interesting paths of one application
by static analysis, and make one profile based on these paths. And then I
can make klee to run this application based on the profile, which means
klee will only explore the limited paths in the profile. Now I cannot find
out how to make the klee to choose paths based on the profile?

Can you give me any hints which functions help klee to choose different
paths? How is it possible to make klee to choose paths based on my profile
which includes several paths?

Thank you very much!


Best Regards,
Pengfei Sun
-------------- next part --------------
HTML attachment scrubbed and removed