klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::StackFrame Struct Reference

#include <ExecutionState.h>

Collaboration diagram for klee::StackFrame:

Public Member Functions

 StackFrame (KInstIterator caller, KFunction *kf)
 
 StackFrame (const StackFrame &s)
 
 ~StackFrame ()
 

Public Attributes

KInstIterator caller
 
KFunctionkf
 
CallPathNodecallPathNode
 
std::vector< const MemoryObject * > allocas
 
Celllocals
 
unsigned minDistToUncoveredOnReturn
 
MemoryObjectvarargs
 

Detailed Description

Definition at line 37 of file ExecutionState.h.

Constructor & Destructor Documentation

StackFrame::StackFrame ( KInstIterator  caller,
KFunction kf 
)

Definition at line 45 of file ExecutionState.cpp.

References kf, locals, and klee::KFunction::numRegisters.

StackFrame::StackFrame ( const StackFrame s)

Definition at line 51 of file ExecutionState.cpp.

References kf, locals, and klee::KFunction::numRegisters.

StackFrame::~StackFrame ( )

Definition at line 63 of file ExecutionState.cpp.

References locals.

Member Data Documentation

std::vector<const MemoryObject*> klee::StackFrame::allocas

Definition at line 42 of file ExecutionState.h.

Referenced by klee::ExecutionState::popFrame().

KInstIterator klee::StackFrame::caller
unsigned klee::StackFrame::minDistToUncoveredOnReturn

Minimum distance to an uncovered instruction once the function returns. This is not a good place for this but is used to quickly compute the context sensitive minimum distance to an uncovered instruction. This value is updated by the StatsTracker periodically.

Definition at line 50 of file ExecutionState.h.

Referenced by klee::StatsTracker::framePushed(), and klee::Executor::processTimers().

MemoryObject* klee::StackFrame::varargs

Definition at line 57 of file ExecutionState.h.

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


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