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

#include <Memory.h>

Collaboration diagram for klee::MemoryObject:

Public Member Functions

 MemoryObject (const MemoryObject &b)
 
MemoryObjectoperator= (const MemoryObject &b)
 
 MemoryObject (uint64_t _address)
 
 MemoryObject (uint64_t _address, unsigned _size, bool _isLocal, bool _isGlobal, bool _isFixed, const llvm::Value *_allocSite, MemoryManager *_parent)
 
 ~MemoryObject ()
 
void getAllocInfo (std::string &result) const
 Get an identifying string for this allocation. More...
 
void setName (std::string name) const
 
ref< ConstantExprgetBaseExpr () const
 
ref< ConstantExprgetSizeExpr () const
 
ref< ExprgetOffsetExpr (ref< Expr > pointer) const
 
ref< ExprgetBoundsCheckPointer (ref< Expr > pointer) const
 
ref< ExprgetBoundsCheckPointer (ref< Expr > pointer, unsigned bytes) const
 
ref< ExprgetBoundsCheckOffset (ref< Expr > offset) const
 
ref< ExprgetBoundsCheckOffset (ref< Expr > offset, unsigned bytes) const
 

Public Attributes

unsigned id
 
uint64_t address
 
unsigned size
 size in bytes More...
 
std::string name
 
bool isLocal
 
bool isGlobal
 
bool isFixed
 
bool fake_object
 true if created by us. More...
 
bool isUserSpecified
 
MemoryManagerparent
 
const llvm::Value * allocSite
 
std::vector< ref< Expr > > cexPreferences
 

Private Attributes

unsigned refCount
 

Static Private Attributes

static int counter = 0
 

Friends

class STPBuilder
 
class ObjectState
 
class ExecutionState
 

Detailed Description

Definition at line 31 of file Memory.h.

Constructor & Destructor Documentation

klee::MemoryObject::MemoryObject ( const MemoryObject b)
klee::MemoryObject::MemoryObject ( uint64_t  _address)
inlineexplicit

Definition at line 76 of file Memory.h.

klee::MemoryObject::MemoryObject ( uint64_t  _address,
unsigned  _size,
bool  _isLocal,
bool  _isGlobal,
bool  _isFixed,
const llvm::Value *  _allocSite,
MemoryManager _parent 
)
inline

Definition at line 86 of file Memory.h.

MemoryObject::~MemoryObject ( )

Definition at line 72 of file Memory.cpp.

References klee::MemoryManager::markFreed(), and parent.

Here is the call graph for this function:

Member Function Documentation

void MemoryObject::getAllocInfo ( std::string &  result) const

Get an identifying string for this allocation.

Definition at line 77 of file Memory.cpp.

References allocSite, and size.

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

Here is the caller graph for this function:

ref<ConstantExpr> klee::MemoryObject::getBaseExpr ( ) const
inline
ref<Expr> klee::MemoryObject::getBoundsCheckOffset ( ref< Expr offset) const
inline

Definition at line 129 of file Memory.h.

References klee::ConstantExpr::alloc(), klee::Context::get(), getSizeExpr(), and size.

Referenced by klee::Executor::executeMemoryOperation(), and getBoundsCheckPointer().

Here is the call graph for this function:

Here is the caller graph for this function:

ref<Expr> klee::MemoryObject::getBoundsCheckOffset ( ref< Expr offset,
unsigned  bytes 
) const
inline

Definition at line 137 of file Memory.h.

References klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::Context::get(), and size.

Here is the call graph for this function:

ref<Expr> klee::MemoryObject::getBoundsCheckPointer ( ref< Expr pointer) const
inline

Definition at line 122 of file Memory.h.

References getBoundsCheckOffset(), and getOffsetExpr().

Referenced by klee::Executor::executeMemoryOperation(), klee::AddressSpace::resolve(), and klee::AddressSpace::resolveOne().

Here is the call graph for this function:

Here is the caller graph for this function:

ref<Expr> klee::MemoryObject::getBoundsCheckPointer ( ref< Expr pointer,
unsigned  bytes 
) const
inline

Definition at line 125 of file Memory.h.

References getBoundsCheckOffset(), and getOffsetExpr().

Here is the call graph for this function:

ref<Expr> klee::MemoryObject::getOffsetExpr ( ref< Expr pointer) const
inline

Definition at line 119 of file Memory.h.

References getBaseExpr().

Referenced by klee::Executor::executeMemoryOperation(), and getBoundsCheckPointer().

Here is the call graph for this function:

Here is the caller graph for this function:

ref<ConstantExpr> klee::MemoryObject::getSizeExpr ( ) const
inline

Definition at line 116 of file Memory.h.

References klee::ConstantExpr::create(), klee::Context::get(), and size.

Referenced by getBoundsCheckOffset().

Here is the call graph for this function:

Here is the caller graph for this function:

MemoryObject& klee::MemoryObject::operator= ( const MemoryObject b)
void klee::MemoryObject::setName ( std::string  name) const
inline

Definition at line 109 of file Memory.h.

References name.

Friends And Related Function Documentation

friend class ExecutionState
friend

Definition at line 34 of file Memory.h.

friend class ObjectState
friend

Definition at line 33 of file Memory.h.

friend class STPBuilder
friend

Definition at line 32 of file Memory.h.

Member Data Documentation

const llvm::Value* klee::MemoryObject::allocSite

"Location" for which this memory object was allocated. This should be either the allocating instruction or the global object it was allocated for (or whatever else makes sense).

Definition at line 61 of file Memory.h.

Referenced by getAllocInfo().

std::vector< ref<Expr> > klee::MemoryObject::cexPreferences
mutable

A list of boolean expressions the user has requested be true of a counterexample. Mutable since we play a little fast and loose with allowing it to be added to during execution (although should sensibly be only at creation time).

Definition at line 67 of file Memory.h.

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

int MemoryObject::counter = 0
staticprivate

Definition at line 37 of file Memory.h.

bool klee::MemoryObject::fake_object

true if created by us.

Definition at line 53 of file Memory.h.

unsigned klee::MemoryObject::id

Definition at line 41 of file Memory.h.

bool klee::MemoryObject::isFixed

Definition at line 50 of file Memory.h.

Referenced by klee::MemoryManager::markFreed(), and klee::MemoryManager::~MemoryManager().

bool klee::MemoryObject::isGlobal
mutable

Definition at line 49 of file Memory.h.

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

bool klee::MemoryObject::isLocal

Definition at line 48 of file Memory.h.

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

bool klee::MemoryObject::isUserSpecified
std::string klee::MemoryObject::name
mutable
MemoryManager* klee::MemoryObject::parent

Definition at line 56 of file Memory.h.

Referenced by ~MemoryObject().

unsigned klee::MemoryObject::refCount
mutableprivate

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