[klee-dev] Query about searcher.cpp file

Thuan Pham thuanpv at comp.nus.edu.sg
Mon Sep 21 02:36:17 BST 2015


Hi Shaila,
To know which search strategy is chosen, you can check the file "info"
generated by KLEE. If you don't specify a specific strategy (using the
--search command line option), the default one of KLEE is the interleaving
between a random path search and a weighted random search aiming to cover
new code.
Regards,
Thuan

On Fri, Sep 18, 2015 at 12:16 AM, Zaman, Tarannum <tsza223 at g.uky.edu> wrote:

> Hi Thuan,
>
> Thanks a lot for your reply.
>
> I am struggling in another point also. Many searcher strategies are
> implemented in klee. If I run a code with klee, then how can klee select
> which searcher strategy is used for that code?
>
> Thanks
> Shaila
>
> On Thu, Sep 17, 2015 at 4:28 AM, Thuan Pham <thuanpv at comp.nus.edu.sg>
> wrote:
>
>> Hi,
>>
>> Basically, any search strategy needs to handle two tasks that are 1)
>> manage a work list of execution states, and 2) select next state to run. To
>> implement a new search strategy (new searcher) in KLEE, we need to modify
>> the two files Searcher.h and Searcher.cpp in lib/Core directory. In
>> Searcher.h, we need to define new class that inherits Searcher class. In
>> addition, we have to declare three important methods which are 1) update
>> (update the work list), 2) selectState (select the state to be executed)
>> and 3) empty (check if the work list is empty). There are some search
>> strategies are implemented in Searcher.cpp, you can read the code first.
>>
>> I hope it helps.
>>
>> Regards,
>>
>> Thuan
>>
>>
>> On Wed, Sep 16, 2015 at 5:05 AM, Zaman, Tarannum <tsza223 at g.uky.edu>
>> wrote:
>>
>>> Hi,
>>>
>>> I am a new user of Klee. I am trying to understand the searcher.cpp file
>>> of the Klee code base. I want to implement a new type of search with the
>>> help of Klee, for which I have to modify Klee's searcher.cpp file.
>>>
>>> But before modifying the code I need to understand it properly. If
>>> anyone can give me any idea about searcher.cpp or share individuals
>>> experience about this file, then it will be really very helpful for me.
>>>
>>> Thanks
>>> Shaila
>>>
>>> _______________________________________________
>>> 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


More information about the klee-dev mailing list