All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::Array Class Reference

#include <Expr.h>

Public Member Functions

 Array (const std::string &_name, uint64_t _size, const ref< ConstantExpr > *constantValuesBegin=0, const ref< ConstantExpr > *constantValuesEnd=0, Expr::Width _domain=Expr::Int32, Expr::Width _range=Expr::Int8)
 ~Array ()
bool isSymbolicArray () const
bool isConstantArray () const
Expr::Width getDomain () const
Expr::Width getRange () const
unsigned computeHash ()
unsigned hash () const

Public Attributes

const std::string name
unsigned size
const std::vector< ref
< ConstantExpr > > 
Expr::Width domain
Expr::Width range

Private Attributes

unsigned hashValue

Detailed Description

Definition at line 601 of file Expr.h.

Constructor & Destructor Documentation

klee::Array::Array ( const std::string &  _name,
uint64_t  _size,
const ref< ConstantExpr > *  constantValuesBegin = 0,
const ref< ConstantExpr > *  constantValuesEnd = 0,
Expr::Width  _domain = Expr::Int32,
Expr::Width  _range = Expr::Int8 

Array - Construct a new array object.

_name- The name for this array. Names should generally be unique across an application, but this is not necessary for correctness, except when printing expressions. When expressions are printed the output will not parse correctly since two arrays with the same name cannot be distinguished once printed.

Definition at line 622 of file Expr.h.

References computeHash(), constantValues, getRange(), isSymbolicArray(), and size.

Here is the call graph for this function:

Array::~Array ( )

Definition at line 486 of file Expr.cpp.

Member Function Documentation

unsigned Array::computeHash ( )

Definition at line 489 of file Expr.cpp.

References klee::Expr::MAGIC_HASH_CONSTANT.

Referenced by Array().

Here is the caller graph for this function:

unsigned klee::Array::hash ( ) const

Definition at line 648 of file Expr.h.

References hashValue.

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

Here is the caller graph for this function:

bool klee::Array::isConstantArray ( ) const

Definition at line 642 of file Expr.h.

References isSymbolicArray().

Referenced by klee::ExprEvaluator::evalRead(), klee::STPBuilder::getInitialArray(), CexRangeEvaluator::getInitialReadRange(), IndependentElementSet::IndependentElementSet(), and klee::ExprSMTLIBPrinter::printArrayDeclarations().

Here is the call graph for this function:

Here is the caller graph for this function:

bool klee::Array::isSymbolicArray ( ) const

Definition at line 641 of file Expr.h.

References constantValues.

Referenced by Array(), klee::expr::ArrayDecl::dump(), isConstantArray(), klee::ExprPPrinter::printQuery(), TryConstArrayOpt(), and klee::SymbolicObjectFinder::visitRead().

Here is the caller graph for this function:

Member Data Documentation

const std::vector< ref<ConstantExpr> > klee::Array::constantValues

constantValues - The constant initial values for this array, or empty for a symbolic array. If non-empty, this size of this array is equivalent to the array size.

Definition at line 610 of file Expr.h.

Referenced by Array(), klee::expr::ArrayDecl::dump(), klee::ExprEvaluator::evalRead(), klee::STPBuilder::getInitialArray(), CexRangeEvaluator::getInitialReadRange(), isSymbolicArray(), klee::ExprSMTLIBPrinter::printArrayDeclarations(), klee::ExprPPrinter::printQuery(), and TryConstArrayOpt().

Expr::Width klee::Array::domain

Definition at line 612 of file Expr.h.

Referenced by getDomain().

unsigned klee::Array::hashValue

Definition at line 651 of file Expr.h.

Referenced by hash().

Expr::Width klee::Array::range

Definition at line 612 of file Expr.h.

Referenced by klee::ExprRangeEvaluator< T >::evaluate(), and getRange().

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