[klee-dev] Set precondition for symbolic execution

[Pengfei Sun]

Hi Daniel,

Great! This is very useful for me. I still have some questions about your
solution. For example, I can mark several paths "important", and then make
klee only explore these "important" branch instructions. Whether there are
special functions for klee to recognize these "important" instructions and
then only explore these instructions?

Thank you very much!

Best Regards,
Pengfei


On Mon, Jul 20, 2015 at 1:31 PM, Daniel Guo <realdaniel2013 at gmail.com>
wrote:

> 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