klee
 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 > > 
constantValues
 
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 
)
inline

Array - Construct a new array object.

Parameters
_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
inline

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
inline

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
inline

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
private

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: