klee::Assignment Class Reference

#include <Assignment.h>

List of all members.

Public Types
typedef std::map< const Array *, std::vector< unsigned char > >	bindings_ty
Public Member Functions
	Assignment (bool _allowFreeValues=false)
	Assignment (std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool _allowFreeValues=false)
ref< Expr >	evaluate (const Array *mo, unsigned index) const
ref< Expr >	evaluate (ref< Expr > e)
template<typename InputIterator >
bool	satisfies (InputIterator begin, InputIterator end)
Public Attributes
bool	allowFreeValues
bindings_ty	bindings

---

Detailed Description

Definition at line 22 of file Assignment.h.

---

Member Typedef Documentation

typedef std::map<const Array*, std::vector<unsigned char> > klee::Assignment::bindings_ty

Definition at line 24 of file Assignment.h.

---

Constructor & Destructor Documentation

klee::Assignment::Assignment

(

bool

_allowFreeValues = false

)

[inline]

Definition at line 30 of file Assignment.h.

klee::Assignment::Assignment	(	std::vector< const Array * > &	objects,
		std::vector< std::vector< unsigned char > > &	values,
		bool	_allowFreeValues = false
	)			[inline]

Definition at line 32 of file Assignment.h.

References bindings.

---

Member Function Documentation

ref< Expr > klee::Assignment::evaluate

(

ref< Expr >

e

)

[inline]

Definition at line 83 of file Assignment.h.

References klee::ExprVisitor::visit().

Here is the call graph for this function:

ref< Expr > klee::Assignment::evaluate	(	const Array *	mo,
		unsigned	index
	)			const [inline]

Definition at line 68 of file Assignment.h.

References klee::ConstantExpr::alloc(), allowFreeValues, bindings, klee::ReadExpr::create(), klee::Expr::Int32, and klee::Expr::Int8.

Referenced by CexCachingSolver::computeValidity(), STPSolverImpl::computeValue(), CexCachingSolver::computeValue(), klee::AssignmentEvaluator::getInitialValue(), and klee::SeedInfo::patchSeed().

Here is the call graph for this function:

Here is the caller graph for this function:

template<typename InputIterator >

bool klee::Assignment::satisfies	(	InputIterator	begin,
		InputIterator	end
	)			[inline]

Definition at line 89 of file Assignment.h.

References klee::ConstantExpr::getConstantValue(), and klee::ExprVisitor::visit().

Referenced by CexCachingSolver::getAssignment(), NullOrSatisfyingAssignment::operator()(), and CexCachingSolver::searchForAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

---

Member Data Documentation

bool klee::Assignment::allowFreeValues

Definition at line 26 of file Assignment.h.

Referenced by evaluate().

bindings_ty klee::Assignment::bindings

Definition at line 27 of file Assignment.h.

Referenced by Assignment(), CexCachingSolver::computeInitialValues(), evaluate(), klee::Executor::executeMakeSymbolic(), AssignmentLessThan::operator()(), and klee::SeedInfo::patchSeed().

---

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

• include/klee/util/Assignment.h