klee::Searcher Class Reference

#include <Searcher.h>

Inheritance diagram for klee::Searcher:

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

Public Member Functions
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...

Detailed Description

A Searcher implements an exploration strategy for the Executor by selecting states for further exploration using different strategies or heuristics.

Definition at line 40 of file Searcher.h.

Member Enumeration Documentation

CoreSearchType

enum klee::Searcher::CoreSearchType : std::uint8_t

Enumerator
DFS
BFS
RandomState
RandomPath
NURS_CovNew
NURS_MD2U
NURS_Depth
NURS_RP
NURS_ICnt
NURS_CPICnt
NURS_QC

Definition at line 63 of file Searcher.h.

Constructor & Destructor Documentation

~Searcher()

virtual klee::Searcher::~Searcher ( )

virtualdefault

Member Function Documentation

empty()

virtual bool klee::Searcher::empty ( )

pure virtual

Returns

True if no state left for exploration, False otherwise

Implemented in klee::DFSSearcher, klee::BFSSearcher, klee::RandomSearcher, klee::WeightedRandomSearcher, klee::RandomPathSearcher, klee::MergingSearcher, klee::BatchingSearcher, klee::IterativeDeepeningTimeSearcher, and klee::InterleavedSearcher.

printName()

virtual void klee::Searcher::printName ( llvm::raw_ostream &  os )

pure virtual

Prints name of searcher as a klee_message().

Implemented in klee::DFSSearcher, klee::BFSSearcher, klee::RandomSearcher, klee::WeightedRandomSearcher, klee::RandomPathSearcher, klee::MergingSearcher, klee::BatchingSearcher, klee::IterativeDeepeningTimeSearcher, and klee::InterleavedSearcher.

Referenced by klee::constructUserSearcher().

Here is the caller graph for this function:

selectState()

virtual ExecutionState & klee::Searcher::selectState ( )

pure virtual

Selects a state for further exploration.

Returns

The selected state.

Implemented in klee::DFSSearcher, klee::BFSSearcher, klee::RandomSearcher, klee::WeightedRandomSearcher, klee::RandomPathSearcher, klee::MergingSearcher, klee::BatchingSearcher, klee::IterativeDeepeningTimeSearcher, and klee::InterleavedSearcher.

Referenced by klee::Executor::run(), and klee::InterleavedSearcher::selectState().

Here is the caller graph for this function:

update()

virtual void klee::Searcher::update ( ExecutionState *  current, const std::vector< ExecutionState * > &  addedStates, const std::vector< ExecutionState * > &  removedStates  )

pure virtual

Notifies searcher about new or deleted states.

Parameters

current	The currently selected state for exploration.
addedStates	The newly branched states with current as common ancestor.
removedStates	The states that will be terminated.

Implemented in klee::DFSSearcher, klee::BFSSearcher, klee::RandomSearcher, klee::WeightedRandomSearcher, klee::RandomPathSearcher, klee::MergingSearcher, klee::BatchingSearcher, klee::IterativeDeepeningTimeSearcher, and klee::InterleavedSearcher.

Referenced by klee::Executor::run(), and klee::Executor::updateStates().

Here is the caller graph for this function:

---

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

• /Users/cristic/klee/lib/Core/Searcher.h