klee::Array Class Reference

#include <Expr.h>

Public Member Functions

bool isSymbolicArray () const
bool isConstantArray () const
const std::string getName () const
unsigned getSize () const
Expr::Width getDomain () const
Expr::Width getRange () const
unsigned computeHash ()
 ComputeHash must take into account the name, the size, the domain, and the range. More...
unsigned hash () const

Public Attributes

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

Private Member Functions

 Array (const Array &array)
Arrayoperator= (const Array &array)
 ~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)

Private Attributes

unsigned hashValue


class ArrayCache

Detailed Description

Definition at line 483 of file Expr.h.

Constructor & Destructor Documentation

◆ Array() [1/2]

klee::Array::Array ( const Array array)

◆ ~Array()

Array::~Array ( )

Definition at line 525 of file Expr.cpp.

◆ Array() [2/2]

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 507 of file Expr.cpp.

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

Here is the call graph for this function:

Member Function Documentation

◆ computeHash()

unsigned Array::computeHash ( )

ComputeHash must take into account the name, the size, the domain, and the range.

Definition at line 528 of file Expr.cpp.

References hashValue, klee::Expr::MAGIC_HASH_CONSTANT, name, and size.

Referenced by Array().

Here is the caller graph for this function:

◆ getDomain()

◆ getName()

const std::string klee::Array::getName ( ) const

Definition at line 527 of file Expr.h.

References name.

◆ getRange()

Expr::Width klee::Array::getRange ( ) const

◆ getSize()

unsigned klee::Array::getSize ( ) const

Definition at line 528 of file Expr.h.

References size.

◆ hash()

unsigned klee::Array::hash ( ) const

Definition at line 534 of file Expr.h.

References hashValue.

Referenced by klee::ArrayHashFn::operator()(), and klee::IndexTransformationExprVisitor::visitConcat().

Here is the caller graph for this function:

◆ isConstantArray()

◆ isSymbolicArray()

◆ operator=()

Array & klee::Array::operator= ( const Array array)

Friends And Related Function Documentation

◆ ArrayCache

friend class ArrayCache

Definition at line 535 of file Expr.h.

Member Data Documentation

◆ constantValues

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 498 of file Expr.h.

Referenced by Array(), klee::ExprOptimizer::computeIndexes(), klee::ReadExpr::create(), klee::expr::ArrayDecl::dump(), klee::ExprEvaluator::evalRead(), CexRangeEvaluator::getInitialReadRange(), isSymbolicArray(), klee::ExprSMTLIBPrinter::printArrayDeclarations(), CexData::propogateExactValues(), and TryConstArrayOpt().

◆ domain

const Expr::Width klee::Array::domain

Domain is how many bits can be used to access the array [32 bits] Range is the size (in bits) of the number stored there (array of bytes -> 8)

Definition at line 493 of file Expr.h.

Referenced by getDomain().

◆ hashValue

unsigned klee::Array::hashValue

Definition at line 501 of file Expr.h.

Referenced by computeHash(), and hash().

◆ name

◆ range

const Expr::Width klee::Array::range

◆ size

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