[klee-dev] Query about searcher.cpp file

[Thuan Pham]

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