Hi, KLEE forks new states at branching points, which makes it can explore different paths. The detailed code is in Executor::executeInstruction(...) function (Executor.cpp, i guess). You can add some meta data to the llvm IR instruction, to mark it "important" (by a llvm pass), then just fully explore the two outgoing states of "important" branch instructions by klee.
Daniel. On Mon, Jul 20, 2015 at 10:58 AM, Pengfei Sun <[email protected]> wrote: > 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 > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
