[klee-dev] Set precondition for symbolic execution

[Daniel Guo]

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 <shaotian330 at gmail.com> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed