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