klee::UpdateNode Class Reference

Class representing a byte update of an array. More...

#include <Expr.h>

Collaboration diagram for klee::UpdateNode:

[legend]

List of all members.

Public Member Functions
	UpdateNode (const UpdateNode *_next, const ref< Expr > &_index, const ref< Expr > &_value)
unsigned	getSize () const
int	compare (const UpdateNode &b) const
unsigned	hash () const
Public Attributes
const UpdateNode *	next
ref< Expr >	index
ref< Expr >	value
Private Member Functions
	UpdateNode ()
	~UpdateNode ()
unsigned	computeHash ()
Private Attributes
unsigned	refCount
void *	stpArray
unsigned	hashValue
unsigned	size
	size of this update sequence, including this update
Friends
class	UpdateList
class	STPBuilder

---

Detailed Description

Class representing a byte update of an array.

Definition at line 439 of file Expr.h.

---

Constructor & Destructor Documentation

UpdateNode::UpdateNode	(	const UpdateNode *	_next,
		const ref< Expr > &	_index,
		const ref< Expr > &	_value
	)

Definition at line 18 of file Updates.cpp.

References computeHash(), klee::Expr::Int8, next, refCount, and size.

Here is the call graph for this function:

klee::UpdateNode::UpdateNode

(

)

[inline, private]

Definition at line 468 of file Expr.h.

UpdateNode::~UpdateNode

(

)

[private]

Definition at line 38 of file Updates.cpp.

References stpArray, and vc_DeleteExpr().

Here is the call graph for this function:

---

Member Function Documentation

int UpdateNode::compare

(

const UpdateNode &

b

)

const

Definition at line 44 of file Updates.cpp.

References klee::ref< T >::compare(), index, and value.

Referenced by klee::UpdateList::compare().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned UpdateNode::computeHash

(

)

[private]

Definition at line 50 of file Updates.cpp.

References hash(), hashValue, index, next, and value.

Referenced by UpdateNode().

Here is the call graph for this function:

Here is the caller graph for this function:

unsigned klee::UpdateNode::getSize

(

)

const [inline]

Definition at line 462 of file Expr.h.

References size.

Referenced by klee::UpdateList::getSize().

Here is the caller graph for this function:

unsigned klee::UpdateNode::hash

(

)

const [inline]

Definition at line 465 of file Expr.h.

References hashValue.

Referenced by computeHash(), and klee::UpdateList::hash().

Here is the caller graph for this function:

---

Friends And Related Function Documentation

friend class STPBuilder [friend]

Definition at line 441 of file Expr.h.

friend class UpdateList [friend]

Definition at line 440 of file Expr.h.

---

Member Data Documentation

unsigned klee::UpdateNode::hashValue [private]

Definition at line 447 of file Expr.h.

Referenced by computeHash(), and hash().

ref<Expr> klee::UpdateNode::index

Definition at line 451 of file Expr.h.

Referenced by compare(), computeHash(), klee::ReadExpr::create(), klee::STPBuilder::getArrayForUpdate(), and PPrinter::scanUpdate().

const UpdateNode* klee::UpdateNode::next

Definition at line 450 of file Expr.h.

Referenced by ObjectFinder::addUpdates(), klee::UpdateList::compare(), computeHash(), klee::ReadExpr::create(), klee::ExprEvaluator::evalRead(), klee::ExprRangeEvaluator< T >::evalRead(), klee::STPBuilder::getArrayForUpdate(), klee::ObjectState::print(), PPrinter::printUpdateList(), PPrinter::scanUpdate(), TryConstArrayOpt(), UpdateNode(), klee::SymbolicObjectFinder::visitRead(), and klee::UpdateList::~UpdateList().

unsigned klee::UpdateNode::refCount [mutable, private]

Definition at line 443 of file Expr.h.

Referenced by klee::UpdateList::extend(), klee::UpdateList::operator=(), klee::UpdateList::UpdateList(), UpdateNode(), and klee::UpdateList::~UpdateList().

unsigned klee::UpdateNode::size [private]

size of this update sequence, including this update

Definition at line 455 of file Expr.h.

Referenced by getSize(), and UpdateNode().

void* klee::UpdateNode::stpArray [mutable, private]

Definition at line 445 of file Expr.h.

Referenced by klee::STPBuilder::getArrayForUpdate(), and ~UpdateNode().

ref<Expr> klee::UpdateNode::value

Definition at line 451 of file Expr.h.

Referenced by compare(), computeHash(), klee::ReadExpr::create(), klee::STPBuilder::getArrayForUpdate(), and PPrinter::scanUpdate().

---

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

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