klee
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 ReadExprhasOrderedReads (ref< Expr > e)
 
static ref< ExprcreateSubExpr (const ref< Expr > &l, ref< Expr > &r)
 
static ref< ExprcreateAddExpr (const ref< Expr > &l, ref< Expr > &r)
 
static ref< ExprcreateMulExpr (const ref< Expr > &l, ref< Expr > &r)
 
static ref< ExprcreateDivExpr (const ref< Expr > &l, ref< Expr > &r, bool sign)
 
static ref< ExprcreateDivRem (const ref< Expr > &l, ref< Expr > &r, bool sign)
 
static ref< ExprcreateShlExpr (const ref< Expr > &l, ref< Expr > &r)
 
static ref< ExprcreateLShrExpr (const ref< Expr > &l, ref< Expr > &r)
 
static ref< ExprcreateAndExpr (const ref< Expr > &l, ref< Expr > &r)
 
static ref< ExprcreateExtractExpr (const ref< Expr > &l, ref< Expr > &r)
 
static ref< ExprcreateExtendExpr (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

◆ helperGenerateAssignment()

◆ 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: