klee::UpdateList Class Reference

Class representing a complete list of updates into an array. More...

#include <Expr.h>

Collaboration diagram for klee::UpdateList:

Public Member Functions
	UpdateList (const Array *_root, const ref< UpdateNode > &_head)
	UpdateList (const UpdateList &b)=default
	~UpdateList ()=default
UpdateList &	operator= (const UpdateList &b)=default
unsigned	getSize () const
	size of this update list More...
void	extend (const ref< Expr > &index, const ref< Expr > &value)
int	compare (const UpdateList &b) const
unsigned	hash () const

Public Attributes
const Array *	root
ref< UpdateNode >	head
	pointer to the most recent update node More...

Friends
class	ReadExpr

Detailed Description

Class representing a complete list of updates into an array.

Definition at line 539 of file Expr.h.

Constructor & Destructor Documentation

UpdateList() [1/2]

UpdateList::UpdateList	(	const Array *	_root,
		const ref< UpdateNode > &	_head
	)

Definition at line 48 of file Updates.cpp.

UpdateList() [2/2]

klee::UpdateList::UpdateList ( const UpdateList &  b )

default

~UpdateList()

klee::UpdateList::~UpdateList ( )

default

Member Function Documentation

compare()

int UpdateList::compare

(

const UpdateList &

b

)

const

Definition at line 61 of file Updates.cpp.

References getSize(), head, klee::Array::name, and root.

Referenced by klee::ReadExpr::compareContents().

Here is the call graph for this function:

Here is the caller graph for this function:

extend()

void UpdateList::extend	(	const ref< Expr > &	index,
		const ref< Expr > &	value
	)

Definition at line 51 of file Updates.cpp.

References klee::Array::getDomain(), klee::Array::getRange(), klee::Expr::getWidth(), head, and root.

Referenced by klee::ObjectState::flushRangeForRead(), klee::ObjectState::flushRangeForWrite(), klee::ObjectState::getUpdates(), and klee::ObjectState::write8().

Here is the call graph for this function:

Here is the caller graph for this function:

getSize()

unsigned klee::UpdateList::getSize ( ) const

inline

size of this update list

Definition at line 556 of file Expr.h.

References head.

Referenced by compare(), and TryConstArrayOpt().

Here is the caller graph for this function:

hash()

unsigned UpdateList::hash

(

)

const

Definition at line 87 of file Updates.cpp.

References head, klee::Expr::MAGIC_HASH_CONSTANT, klee::Array::name, and root.

Referenced by klee::ReadExpr::computeHash().

Here is the caller graph for this function:

operator=()

UpdateList & klee::UpdateList::operator= ( const UpdateList &  b )

default

Friends And Related Function Documentation

ReadExpr

friend class ReadExpr

friend

Definition at line 540 of file Expr.h.

Member Data Documentation

head

ref<UpdateNode> klee::UpdateList::head

pointer to the most recent update node

Definition at line 546 of file Expr.h.

Referenced by compare(), klee::ReadExpr::create(), klee::ExprRangeEvaluator< T >::evalRead(), klee::ExprEvaluator::evalRead(), extend(), getSize(), klee::ObjectState::getUpdates(), hash(), IndependentElementSet::IndependentElementSet(), klee::ArrayReadExprVisitor::inspectRead(), klee::ObjectState::makeSymbolic(), klee::ObjectState::print(), PPrinter::printUpdateList(), CexData::propogateExactValues(), klee::ConstantArrayExprVisitor::visitConcat(), klee::ConstantArrayExprVisitor::visitRead(), klee::IndexCompatibilityExprVisitor::visitRead(), klee::ConstantArrayFinder::visitRead(), and klee::SymbolicObjectFinder::visitRead().

root

const Array* klee::UpdateList::root

Definition at line 543 of file Expr.h.

Referenced by klee::ImpliedValue::checkForImpliedValues(), compare(), klee::ReadExpr::create(), klee::ExprRangeEvaluator< T >::evalRead(), klee::ExprEvaluator::evalRead(), klee::ExprRangeEvaluator< T >::evaluate(), extend(), klee::ObjectState::getUpdates(), klee::ReadExpr::getWidth(), hash(), klee::AssignmentGenerator::helperGenerateAssignment(), IndependentElementSet::IndependentElementSet(), klee::ArrayReadExprVisitor::inspectRead(), klee::SeedInfo::patchSeed(), klee::ObjectState::print(), PPrinter::printUpdateList(), CexData::propogateExactValues(), CexData::propogatePossibleValues(), klee::ReadExpr::ReadExpr(), TryConstArrayOpt(), klee::ConstantArrayExprVisitor::visitConcat(), klee::ConstantArrayExprVisitor::visitRead(), klee::IndexCompatibilityExprVisitor::visitRead(), klee::ConstantArrayFinder::visitRead(), and klee::SymbolicObjectFinder::visitRead().

---

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

• /Users/cristic/klee/include/klee/Expr/Expr.h
• /Users/cristic/klee/lib/Expr/Updates.cpp