klee::ConstantExpr Class Reference

#include <Expr.h>

Inheritance diagram for klee::ConstantExpr:

[legend]

Collaboration diagram for klee::ConstantExpr:

[legend]

List of all members.

Public Member Functions
	~ConstantExpr ()
Width	getWidth () const
Kind	getKind () const
unsigned	getNumKids () const
ref< Expr >	getKid (unsigned i) const
uint64_t	getConstantValue () const
int	compareContents (const Expr &b) const
virtual ref< Expr >	rebuild (ref< Expr > kids[]) const
virtual unsigned	computeHash ()
void	toMemory (void *address)
Static Public Member Functions
static ref< Expr >	fromMemory (void *address, Width w)
static ref< ConstantExpr >	alloc (uint64_t v, Width w)
static ref< ConstantExpr >	create (uint64_t v, Width w)
static bool	classof (const Expr *E)
static bool	classof (const ConstantExpr *)
Public Attributes
Width	width
Static Public Attributes
static const Kind	kind = Constant
static const unsigned	numKids = 0
Private Member Functions
	ConstantExpr (uint64_t v, Width w)
Private Attributes
uint64_t	value

---

Detailed Description

Definition at line 294 of file Expr.h.

---

Constructor & Destructor Documentation

klee::ConstantExpr::ConstantExpr	(	uint64_t	v,
		Width	w
	)			[inline, private]

Definition at line 302 of file Expr.h.

Referenced by alloc().

Here is the caller graph for this function:

klee::ConstantExpr::~ConstantExpr

(

)

[inline]

Definition at line 308 of file Expr.h.

---

Member Function Documentation

static ref<ConstantExpr> klee::ConstantExpr::alloc	(	uint64_t	v,
		Width	w
	)			[inline, static]

Definition at line 340 of file Expr.h.

References ConstantExpr().

Referenced by klee::Executor::addConstraint(), klee::ImpliedValue::checkForImpliedValues(), create(), klee::Expr::createTempRead(), EqExpr_create(), klee::Executor::evalConstantExpr(), klee::ExprEvaluator::evalRead(), klee::Assignment::evaluate(), klee::Executor::executeAlloc(), klee::Executor::executeInstruction(), klee::MemoryObject::getBoundsCheckOffset(), klee::Executor::getConstraintLog(), klee::TimingSolver::getInitialValues(), klee::Executor::getSymbolicSolution(), klee::ExecutionState::merge(), klee::SeedInfo::patchSeed(), klee::ExprPPrinter::printConstraints(), klee::ConstraintManager::simplifyExpr(), SubExpr_create(), TryConstArrayOpt(), and klee::Query::withFalse().

Here is the call graph for this function:

Here is the caller graph for this function:

static bool klee::ConstantExpr::classof

(

const ConstantExpr *

)

[inline, static]

Definition at line 356 of file Expr.h.

static bool klee::ConstantExpr::classof

(

const Expr *

E

)

[inline, static]

Reimplemented from klee::Expr.

Definition at line 353 of file Expr.h.

References klee::Expr::Constant, and klee::Expr::getKind().

Here is the call graph for this function:

int klee::ConstantExpr::compareContents

(

const Expr &

b

)

const [inline, virtual]

Reimplemented from klee::Expr.

Definition at line 318 of file Expr.h.

References value, and width.

unsigned ConstantExpr::computeHash

(

)

[virtual]

(Re)computes the hash of the current expression. Returns the hash value.

Reimplemented from klee::Expr.

Definition at line 167 of file Expr.cpp.

References klee::Expr::hashValue, klee::Expr::MAGIC_HASH_CONSTANT, value, and width.

static ref<ConstantExpr> klee::ConstantExpr::create	(	uint64_t	v,
		Width	w
	)			[inline, static]

Definition at line 347 of file Expr.h.

References alloc(), and klee::bits64::truncateToNBits().

Referenced by klee::Expr::createIsZero(), klee::Expr::createPointer(), EqExpr_createPartialR(), klee::ObjectState::flushRangeForRead(), klee::ObjectState::flushRangeForWrite(), fromMemory(), klee::MemoryObject::getBaseExpr(), klee::Solver::getRange(), klee::MemoryObject::getSizeExpr(), klee::ObjectState::read16(), klee::ObjectState::read32(), klee::ObjectState::read64(), klee::ObjectState::read8(), SRemExpr_create(), SubExpr_createPartial(), URemExpr_create(), klee::ObjectState::write16(), klee::ObjectState::write32(), klee::ObjectState::write64(), and XorExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > ConstantExpr::fromMemory	(	void *	address,
		Width	w
	)			[static]

Definition at line 328 of file Expr.cpp.

References klee::Expr::Bool, create(), klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, and klee::Expr::Int8.

Here is the call graph for this function:

uint64_t klee::ConstantExpr::getConstantValue

(

)

const [inline]

Definition at line 316 of file Expr.h.

References value.

Referenced by klee::Assignment::satisfies(), and TryConstArrayOpt().

Here is the caller graph for this function:

ref<Expr> klee::ConstantExpr::getKid

(

unsigned

i

)

const [inline, virtual]

Implements klee::Expr.

Definition at line 314 of file Expr.h.

Kind klee::ConstantExpr::getKind

(

)

const [inline, virtual]

Implements klee::Expr.

Definition at line 311 of file Expr.h.

References klee::Expr::Constant.

unsigned klee::ConstantExpr::getNumKids

(

)

const [inline, virtual]

Implements klee::Expr.

Definition at line 313 of file Expr.h.

Width klee::ConstantExpr::getWidth

(

)

const [inline, virtual]

Implements klee::Expr.

Definition at line 310 of file Expr.h.

References width.

virtual ref<Expr> klee::ConstantExpr::rebuild

(

ref< Expr >

kids[]

)

const [inline, virtual]

Implements klee::Expr.

Definition at line 330 of file Expr.h.

void ConstantExpr::toMemory

(

void *

address

)

Definition at line 339 of file Expr.cpp.

References klee::Expr::Bool, klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, klee::Expr::Int8, value, and width.

---

Member Data Documentation

const Kind klee::ConstantExpr::kind = Constant [static]

Definition at line 296 of file Expr.h.

const unsigned klee::ConstantExpr::numKids = 0 [static]

Definition at line 297 of file Expr.h.

uint64_t klee::ConstantExpr::value [private]

Definition at line 300 of file Expr.h.

Referenced by compareContents(), computeHash(), getConstantValue(), and toMemory().

Width klee::ConstantExpr::width

Definition at line 305 of file Expr.h.

Referenced by compareContents(), computeHash(), getWidth(), and toMemory().

---

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

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