klee::AssignmentGenerator Class Reference

#include <AssignmentGenerator.h>

Static Public Member Functions
static bool	generatePartialAssignment (const ref< Expr > &e, ref< Expr > &val, Assignment *&a)

Static Private Member Functions
static bool	helperGenerateAssignment (const ref< Expr > &e, ref< Expr > &val, Assignment *&a, Expr::Width width, bool sign)
static bool	isReadExprAtOffset (ref< Expr > e, const ReadExpr *base, ref< Expr > offset)
static ReadExpr *	hasOrderedReads (ref< Expr > e)
static ref< Expr >	createSubExpr (const ref< Expr > &l, ref< Expr > &r)
static ref< Expr >	createAddExpr (const ref< Expr > &l, ref< Expr > &r)
static ref< Expr >	createMulExpr (const ref< Expr > &l, ref< Expr > &r)
static ref< Expr >	createDivExpr (const ref< Expr > &l, ref< Expr > &r, bool sign)
static ref< Expr >	createDivRem (const ref< Expr > &l, ref< Expr > &r, bool sign)
static ref< Expr >	createShlExpr (const ref< Expr > &l, ref< Expr > &r)
static ref< Expr >	createLShrExpr (const ref< Expr > &l, ref< Expr > &r)
static ref< Expr >	createAndExpr (const ref< Expr > &l, ref< Expr > &r)
static ref< Expr >	createExtractExpr (const ref< Expr > &l, ref< Expr > &r)
static ref< Expr >	createExtendExpr (const ref< Expr > &l, ref< Expr > &r)
static std::vector< unsigned char >	getByteValue (ref< Expr > &val)
static std::vector< unsigned char >	getIndexedValue (const std::vector< unsigned char > &c_val, ConstantExpr &index, const unsigned int size)

Detailed Description

Definition at line 27 of file AssignmentGenerator.h.

Member Function Documentation

createAddExpr()

ref< Expr > AssignmentGenerator::createAddExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 265 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

createAndExpr()

ref< Expr > AssignmentGenerator::createAndExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 298 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

createDivExpr()

ref< Expr > AssignmentGenerator::createDivExpr ( const ref< Expr > &  l, ref< Expr > &  r, bool  sign  )

staticprivate

Definition at line 281 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

createDivRem()

ref< Expr > AssignmentGenerator::createDivRem ( const ref< Expr > &  l, ref< Expr > &  r, bool  sign  )

staticprivate

Definition at line 273 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

createExtendExpr()

ref< Expr > AssignmentGenerator::createExtendExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 307 of file AssignmentGenerator.cpp.

References klee::ref< T >::get(), klee::Expr::getKind(), klee::Expr::getWidth(), and klee::Expr::ZExt.

Referenced by helperGenerateAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

createExtractExpr()

ref< Expr > AssignmentGenerator::createExtractExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 302 of file AssignmentGenerator.cpp.

References klee::ExtractExpr::create(), klee::ref< T >::get(), and klee::Expr::getWidth().

Referenced by helperGenerateAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

createLShrExpr()

ref< Expr > AssignmentGenerator::createLShrExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 293 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

createMulExpr()

ref< Expr > AssignmentGenerator::createMulExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 269 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

createShlExpr()

ref< Expr > AssignmentGenerator::createShlExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 289 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

createSubExpr()

ref< Expr > AssignmentGenerator::createSubExpr ( const ref< Expr > &  l, ref< Expr > &  r  )

staticprivate

Definition at line 261 of file AssignmentGenerator.cpp.

Referenced by helperGenerateAssignment().

Here is the caller graph for this function:

generatePartialAssignment()

bool AssignmentGenerator::generatePartialAssignment ( const ref< Expr > &  e, ref< Expr > &  val, Assignment *&  a  )

static

Definition at line 30 of file AssignmentGenerator.cpp.

References klee::Expr::getWidth(), and helperGenerateAssignment().

Referenced by klee::ExprOptimizer::computeIndexes().

Here is the call graph for this function:

Here is the caller graph for this function:

getByteValue()

std::vector< unsigned char > AssignmentGenerator::getByteValue ( ref< Expr > &  val )

staticprivate

Definition at line 316 of file AssignmentGenerator.cpp.

References klee::ref< T >::get(), and klee::Expr::Int8.

Referenced by helperGenerateAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

getIndexedValue()

std::vector< unsigned char > AssignmentGenerator::getIndexedValue ( const std::vector< unsigned char > &  c_val, ConstantExpr &  index, const unsigned int  size  )

staticprivate

Definition at line 330 of file AssignmentGenerator.cpp.

References klee::ConstantExpr::getAPValue().

Referenced by helperGenerateAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

hasOrderedReads()

ReadExpr * AssignmentGenerator::hasOrderedReads ( ref< Expr >  e )

staticprivate

Definition at line 229 of file AssignmentGenerator.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Concat, klee::ConstantExpr::create(), klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getKind(), klee::ReadExpr::getWidth(), klee::Expr::getWidth(), klee::ReadExpr::index, klee::Expr::Int8, and isReadExprAtOffset().

Referenced by helperGenerateAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

helperGenerateAssignment()

bool AssignmentGenerator::helperGenerateAssignment ( const ref< Expr > &  e, ref< Expr > &  val, Assignment *&  a, Expr::Width  width, bool  sign  )

staticprivate

Definition at line 36 of file AssignmentGenerator.cpp.

References klee::Expr::Add, klee::Expr::And, klee::Assignment::bindings, klee::Expr::Concat, klee::ExtractExpr::create(), createAddExpr(), createAndExpr(), createDivExpr(), createDivRem(), createExtendExpr(), createExtractExpr(), createLShrExpr(), createMulExpr(), createShlExpr(), createSubExpr(), klee::Expr::Extract, klee::ref< T >::get(), getByteValue(), getIndexedValue(), klee::Expr::getKid(), klee::Expr::getKind(), klee::Expr::getWidth(), hasOrderedReads(), helperGenerateAssignment(), klee::ReadExpr::index, klee::Array::isSymbolicArray(), klee::Expr::isZero(), klee::klee_warning(), klee::Expr::LShr, klee::Expr::Mul, klee::Expr::Not, klee::Expr::printKind(), klee::Expr::Read, klee::UpdateList::root, klee::Expr::SDiv, klee::Expr::SExt, klee::Expr::Shl, klee::Array::size, klee::Expr::Sub, klee::Expr::UDiv, klee::ReadExpr::updates, and klee::Expr::ZExt.

Referenced by generatePartialAssignment(), and helperGenerateAssignment().

Here is the call graph for this function:

Here is the caller graph for this function:

isReadExprAtOffset()

bool AssignmentGenerator::isReadExprAtOffset ( ref< Expr >  e, const ReadExpr *  base, ref< Expr >  offset  )

staticprivate

Definition at line 221 of file AssignmentGenerator.cpp.

References klee::ref< T >::get(), klee::ReadExpr::getWidth(), klee::ReadExpr::index, and klee::Expr::Int8.

Referenced by hasOrderedReads().

Here is the call graph for this function:

Here is the caller graph for this function:

---

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

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