klee
klee::BFSSearcher Class Referencefinal

#include <Searcher.h>

Inheritance diagram for klee::BFSSearcher:
Collaboration diagram for klee::BFSSearcher:

Public Member Functions

ExecutionStateselectState () 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...
 
- Public Member Functions inherited from klee::Searcher
virtual ~Searcher ()=default
 
virtual ExecutionStateselectState ()=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

- Public Types inherited from klee::Searcher
enum  CoreSearchType : std::uint8_t {
  DFS , BFS , RandomState , RandomPath ,
  NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP ,
  NURS_ICnt , NURS_CPICnt , NURS_QC
}
 

Detailed Description

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.

Member Function Documentation

◆ empty()

bool BFSSearcher::empty ( )
overridevirtual
Returns
True if no state left for exploration, False otherwise

Implements klee::Searcher.

Definition at line 108 of file Searcher.cpp.

References states.

◆ printName()

void BFSSearcher::printName ( llvm::raw_ostream &  os)
overridevirtual

Prints name of searcher as a klee_message().

Implements klee::Searcher.

Definition at line 112 of file Searcher.cpp.

◆ selectState()

ExecutionState & BFSSearcher::selectState ( )
overridevirtual

Selects a state for further exploration.

Returns
The selected state.

Implements klee::Searcher.

Definition at line 75 of file Searcher.cpp.

References states.

◆ update()

void BFSSearcher::update ( ExecutionState current,
const std::vector< ExecutionState * > &  addedStates,
const std::vector< ExecutionState * > &  removedStates 
)
overridevirtual

Notifies searcher about new or deleted states.

Parameters
currentThe currently selected state for exploration.
addedStatesThe newly branched states with current as common ancestor.
removedStatesThe states that will be terminated.

Implements klee::Searcher.

Definition at line 79 of file Searcher.cpp.

References states.

Member Data Documentation

◆ states

std::deque<ExecutionState*> klee::BFSSearcher::states
private

Definition at line 97 of file Searcher.h.

Referenced by empty(), selectState(), and update().


The documentation for this class was generated from the following files: