klee::UpdateNode Class Reference

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

#include <Expr.h>

Collaboration diagram for klee::UpdateNode:

Public Member Functions
	UpdateNode (const ref< UpdateNode > &_next, const ref< Expr > &_index, const ref< Expr > &_value)
unsigned	getSize () const
int	compare (const UpdateNode &b) const
unsigned	hash () const
	UpdateNode ()=delete
	~UpdateNode ()=default
unsigned	computeHash ()

Public Attributes
const ref< UpdateNode >	next
ref< Expr >	index
ref< Expr >	value
class ReferenceCounter	_refCount
	Required by klee::ref-managed objects. More...

Private Attributes
unsigned	hashValue
unsigned	size
	size of this update sequence, including this update More...

Friends
class	UpdateList

Detailed Description

Class representing a byte update of an array.

Definition at line 451 of file Expr.h.

Constructor & Destructor Documentation

UpdateNode() [1/2]

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

Definition at line 18 of file Updates.cpp.

References computeHash(), next, and size.

Here is the call graph for this function:

UpdateNode() [2/2]

klee::UpdateNode::UpdateNode ( )

delete

~UpdateNode()

klee::UpdateNode::~UpdateNode ( )

default

Member Function Documentation

compare()

int UpdateNode::compare

(

const UpdateNode &

b

)

const

Definition at line 33 of file Updates.cpp.

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

Here is the call graph for this function:

computeHash()

unsigned UpdateNode::computeHash

(

)

Definition at line 39 of file Updates.cpp.

References klee::Expr::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:

getSize()

unsigned klee::UpdateNode::getSize ( ) const

inline

Definition at line 472 of file Expr.h.

References size.

hash()

unsigned klee::UpdateNode::hash ( ) const

inline

Definition at line 475 of file Expr.h.

References hashValue.

Referenced by klee::UpdateNodeHashFn::operator()().

Here is the caller graph for this function:

Friends And Related Function Documentation

UpdateList

friend class UpdateList

friend

Definition at line 452 of file Expr.h.

Member Data Documentation

_refCount

class ReferenceCounter klee::UpdateNode::_refCount

Required by klee::ref-managed objects.

Definition at line 462 of file Expr.h.

hashValue

unsigned klee::UpdateNode::hashValue

private

Definition at line 455 of file Expr.h.

Referenced by computeHash(), and hash().

index

ref<Expr> klee::UpdateNode::index

Definition at line 459 of file Expr.h.

Referenced by compare(), computeHash(), klee::ExprOptimizer::getSelectOptExpr(), klee::ExprSMTLIBPrinter::printUpdatesAndArray(), PPrinter::scanUpdate(), and klee::ExprSMTLIBPrinter::scanUpdates().

next

const ref<UpdateNode> klee::UpdateNode::next

Definition at line 458 of file Expr.h.

Referenced by computeHash(), klee::ExprOptimizer::getSelectOptExpr(), klee::ExprSMTLIBPrinter::printUpdatesAndArray(), PPrinter::scanUpdate(), klee::ExprSMTLIBPrinter::scanUpdates(), and UpdateNode().

size

unsigned klee::UpdateNode::size

private

size of this update sequence, including this update

Definition at line 466 of file Expr.h.

Referenced by getSize(), and UpdateNode().

value

ref<Expr> klee::UpdateNode::value

Definition at line 459 of file Expr.h.

Referenced by compare(), computeHash(), klee::ExprOptimizer::getSelectOptExpr(), klee::ExprSMTLIBPrinter::printUpdatesAndArray(), PPrinter::scanUpdate(), and klee::ExprSMTLIBPrinter::scanUpdates().

---

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