klee
|
#include <Searcher.h>
Public Member Functions | |
ExecutionState & | selectState () override |
void | update (ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override |
bool | empty () override |
void | printName (llvm::raw_ostream &os) override |
Prints name of searcher as a klee_message() . More... | |
![]() | |
virtual | ~Searcher ()=default |
virtual ExecutionState & | selectState ()=0 |
virtual void | update (ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates)=0 |
virtual bool | empty ()=0 |
virtual void | printName (llvm::raw_ostream &os)=0 |
Prints name of searcher as a klee_message() . More... | |
Private Attributes | |
std::deque< ExecutionState * > | states |
Additional Inherited Members | |
![]() | |
enum | CoreSearchType : std::uint8_t { DFS , BFS , RandomState , RandomPath , NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP , NURS_ICnt , NURS_CPICnt , NURS_QC } |
BFSSearcher implements breadth-first exploration. When KLEE branches multiple times for a single instruction, all new states have the same depth. Keep in mind that the process tree (PTree) is a binary tree and hence the depth of a state in that tree and its branch depth during BFS are different.
Definition at line 96 of file Searcher.h.
|
overridevirtual |
Implements klee::Searcher.
Definition at line 108 of file Searcher.cpp.
References states.
|
overridevirtual |
Prints name of searcher as a klee_message()
.
Implements klee::Searcher.
Definition at line 112 of file Searcher.cpp.
|
overridevirtual |
Selects a state for further exploration.
Implements klee::Searcher.
Definition at line 75 of file Searcher.cpp.
References states.
|
overridevirtual |
Notifies searcher about new or deleted states.
current | The currently selected state for exploration. |
addedStates | The newly branched states with current as common ancestor. |
removedStates | The states that will be terminated. |
Implements klee::Searcher.
Definition at line 79 of file Searcher.cpp.
References states.
|
private |
Definition at line 97 of file Searcher.h.
Referenced by empty(), selectState(), and update().