klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::ExecutionState Class Reference

#include <ExecutionState.h>

Collaboration diagram for klee::ExecutionState:

Public Types

typedef std::vector< StackFramestack_ty
 

Public Member Functions

std::string getFnAlias (std::string fn)
 
void addFnAlias (std::string old_fn, std::string new_fn)
 
void removeFnAlias (std::string fn)
 
 ExecutionState (KFunction *kf)
 
 ExecutionState (const std::vector< ref< Expr > > &assumptions)
 
 ExecutionState (const ExecutionState &state)
 
 ~ExecutionState ()
 
ExecutionStatebranch ()
 
void pushFrame (KInstIterator caller, KFunction *kf)
 
void popFrame ()
 
void addSymbolic (const MemoryObject *mo, const Array *array)
 
void addConstraint (ref< Expr > e)
 
bool merge (const ExecutionState &b)
 
void dumpStack (llvm::raw_ostream &out) const
 

Public Attributes

bool fakeState
 
unsigned underConstrained
 
unsigned depth
 
KInstIterator pc
 
KInstIterator prevPC
 
stack_ty stack
 
ConstraintManager constraints
 
double queryCost
 
double weight
 
AddressSpace addressSpace
 
TreeOStream pathOS
 
TreeOStream symPathOS
 
unsigned instsSinceCovNew
 
bool coveredNew
 
bool forkDisabled
 Disables forking, set by user code. More...
 
std::map< const std::string
*, std::set< unsigned > > 
coveredLines
 
PTreeNodeptreeNode
 
std::vector< std::pair< const
MemoryObject *, const Array * > > 
symbolics
 ordered list of symbolics: used to generate test cases. More...
 
std::set< std::string > arrayNames
 Set of used array names. Used to avoid collisions. More...
 
MemoryMap shadowObjects
 
unsigned incomingBBIndex
 

Private Member Functions

ExecutionStateoperator= (const ExecutionState &)
 
 ExecutionState ()
 

Private Attributes

std::map< std::string,
std::string > 
fnAliases
 

Detailed Description

Definition at line 64 of file ExecutionState.h.

Member Typedef Documentation

Definition at line 66 of file ExecutionState.h.

Constructor & Destructor Documentation

klee::ExecutionState::ExecutionState ( )
inlineprivate

Definition at line 116 of file ExecutionState.h.

Referenced by branch().

Here is the caller graph for this function:

ExecutionState::ExecutionState ( KFunction kf)

Definition at line 69 of file ExecutionState.cpp.

References pushFrame().

Here is the call graph for this function:

ExecutionState::ExecutionState ( const std::vector< ref< Expr > > &  assumptions)

Definition at line 84 of file ExecutionState.cpp.

ExecutionState::ExecutionState ( const ExecutionState state)

Definition at line 105 of file ExecutionState.cpp.

References symbolics.

ExecutionState::~ExecutionState ( )

Definition at line 92 of file ExecutionState.cpp.

References popFrame(), klee::MemoryObject::refCount, stack, and symbolics.

Here is the call graph for this function:

Member Function Documentation

void klee::ExecutionState::addConstraint ( ref< Expr e)
inline

Definition at line 135 of file ExecutionState.h.

References klee::ConstraintManager::addConstraint(), and constraints.

Referenced by klee::Executor::addConstraint(), klee::Executor::getSymbolicSolution(), and klee::Executor::replaceReadWithSymbolic().

Here is the call graph for this function:

Here is the caller graph for this function:

void ExecutionState::addFnAlias ( std::string  old_fn,
std::string  new_fn 
)

Definition at line 171 of file ExecutionState.cpp.

References fnAliases.

void ExecutionState::addSymbolic ( const MemoryObject mo,
const Array array 
)

Definition at line 158 of file ExecutionState.cpp.

References klee::MemoryObject::refCount, and symbolics.

Referenced by klee::Executor::executeMakeSymbolic().

Here is the caller graph for this function:

ExecutionState * ExecutionState::branch ( )

Definition at line 133 of file ExecutionState.cpp.

References coveredLines, coveredNew, depth, ExecutionState(), and weight.

Referenced by klee::Executor::branch(), and klee::Executor::fork().

Here is the call graph for this function:

Here is the caller graph for this function:

void ExecutionState::dumpStack ( llvm::raw_ostream &  out) const
std::string ExecutionState::getFnAlias ( std::string  fn)

Definition at line 164 of file ExecutionState.cpp.

References fnAliases.

Referenced by klee::Executor::getTargetFunction().

Here is the caller graph for this function:

ExecutionState& klee::ExecutionState::operator= ( const ExecutionState )
private
void ExecutionState::popFrame ( )

Definition at line 150 of file ExecutionState.cpp.

References addressSpace, klee::StackFrame::allocas, stack, and klee::AddressSpace::unbindObject().

Referenced by klee::Executor::executeInstruction(), and ~ExecutionState().

Here is the call graph for this function:

Here is the caller graph for this function:

void ExecutionState::pushFrame ( KInstIterator  caller,
KFunction kf 
)

Definition at line 146 of file ExecutionState.cpp.

References stack.

Referenced by klee::Executor::executeCall(), and ExecutionState().

Here is the caller graph for this function:

void ExecutionState::removeFnAlias ( std::string  fn)

Definition at line 175 of file ExecutionState.cpp.

References fnAliases.

Member Data Documentation

std::set<std::string> klee::ExecutionState::arrayNames

Set of used array names. Used to avoid collisions.

Definition at line 103 of file ExecutionState.h.

Referenced by klee::Executor::executeMakeSymbolic().

std::map<const std::string*, std::set<unsigned> > klee::ExecutionState::coveredLines
unsigned klee::ExecutionState::depth

Definition at line 78 of file ExecutionState.h.

Referenced by branch().

bool klee::ExecutionState::fakeState

Definition at line 74 of file ExecutionState.h.

std::map< std::string, std::string > klee::ExecutionState::fnAliases
private

Definition at line 71 of file ExecutionState.h.

Referenced by addFnAlias(), getFnAlias(), and removeFnAlias().

bool klee::ExecutionState::forkDisabled

Disables forking, set by user code.

Definition at line 92 of file ExecutionState.h.

Referenced by klee::Executor::fork().

unsigned klee::ExecutionState::incomingBBIndex
unsigned klee::ExecutionState::instsSinceCovNew
TreeOStream klee::ExecutionState::pathOS
MemoryMap klee::ExecutionState::shadowObjects

Definition at line 107 of file ExecutionState.h.

std::vector< std::pair<const MemoryObject*, const Array*> > klee::ExecutionState::symbolics

ordered list of symbolics: used to generate test cases.

Definition at line 100 of file ExecutionState.h.

Referenced by addSymbolic(), ExecutionState(), klee::Executor::getSymbolicSolution(), merge(), and ~ExecutionState().

TreeOStream klee::ExecutionState::symPathOS
unsigned klee::ExecutionState::underConstrained

Definition at line 77 of file ExecutionState.h.

double klee::ExecutionState::weight

Definition at line 85 of file ExecutionState.h.

Referenced by branch(), and klee::WeightedRandomSearcher::getWeight().


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