klee
Public Member Functions | Protected Member Functions | Private Member Functions | Private Attributes | List of all members
klee::ArrayReadExprVisitor Class Reference

#include <ArrayExprVisitor.h>

Inheritance diagram for klee::ArrayReadExprVisitor:
Inheritance graph
[legend]
Collaboration diagram for klee::ArrayReadExprVisitor:
Collaboration graph
[legend]

Public Member Functions

 ArrayReadExprVisitor (std::vector< const ReadExpr * > &_reads, std::map< const ReadExpr *, std::pair< ref< Expr >, Expr::Width > > &_readInfo)
 
bool isIncompatible ()
 
bool containsSymbolic ()
 
- Public Member Functions inherited from klee::ExprVisitor
ref< Expr > visit (const ref< Expr > &e)
 

Protected Member Functions

Action visitConcat (const ConcatExpr &) override
 
Action visitRead (const ReadExpr &) override
 
- Protected Member Functions inherited from klee::ExprVisitor
 ExprVisitor (bool _recursive=false)
 
virtual ~ExprVisitor ()
 
virtual Action visitExpr (const Expr &)
 
virtual Action visitExprPost (const Expr &)
 
virtual Action visitNotOptimized (const NotOptimizedExpr &)
 
virtual Action visitRead (const ReadExpr &)
 
virtual Action visitSelect (const SelectExpr &)
 
virtual Action visitConcat (const ConcatExpr &)
 
virtual Action visitExtract (const ExtractExpr &)
 
virtual Action visitZExt (const ZExtExpr &)
 
virtual Action visitSExt (const SExtExpr &)
 
virtual Action visitAdd (const AddExpr &)
 
virtual Action visitSub (const SubExpr &)
 
virtual Action visitMul (const MulExpr &)
 
virtual Action visitUDiv (const UDivExpr &)
 
virtual Action visitSDiv (const SDivExpr &)
 
virtual Action visitURem (const URemExpr &)
 
virtual Action visitSRem (const SRemExpr &)
 
virtual Action visitNot (const NotExpr &)
 
virtual Action visitAnd (const AndExpr &)
 
virtual Action visitOr (const OrExpr &)
 
virtual Action visitXor (const XorExpr &)
 
virtual Action visitShl (const ShlExpr &)
 
virtual Action visitLShr (const LShrExpr &)
 
virtual Action visitAShr (const AShrExpr &)
 
virtual Action visitEq (const EqExpr &)
 
virtual Action visitNe (const NeExpr &)
 
virtual Action visitUlt (const UltExpr &)
 
virtual Action visitUle (const UleExpr &)
 
virtual Action visitUgt (const UgtExpr &)
 
virtual Action visitUge (const UgeExpr &)
 
virtual Action visitSlt (const SltExpr &)
 
virtual Action visitSle (const SleExpr &)
 
virtual Action visitSgt (const SgtExpr &)
 
virtual Action visitSge (const SgeExpr &)
 

Private Member Functions

Action inspectRead (ref< Expr > hash, Expr::Width width, const ReadExpr &)
 

Private Attributes

std::vector< const ReadExpr * > & reads
 
std::map< const ReadExpr *, std::pair< ref< Expr >, Expr::Width > > & readInfo
 
bool symbolic
 
bool incompatible
 

Detailed Description

Definition at line 91 of file ArrayExprVisitor.h.

Constructor & Destructor Documentation

◆ ArrayReadExprVisitor()

klee::ArrayReadExprVisitor::ArrayReadExprVisitor ( std::vector< const ReadExpr * > &  _reads,
std::map< const ReadExpr *, std::pair< ref< Expr >, Expr::Width > > &  _readInfo 
)
inline

Definition at line 105 of file ArrayExprVisitor.h.

Member Function Documentation

◆ containsSymbolic()

bool klee::ArrayReadExprVisitor::containsSymbolic ( )
inline

Definition at line 111 of file ArrayExprVisitor.h.

References symbolic.

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

Here is the caller graph for this function:

◆ inspectRead()

ExprVisitor::Action ArrayReadExprVisitor::inspectRead ( ref< Expr >  hash,
Expr::Width  width,
const ReadExpr &  re 
)
private

Definition at line 195 of file ArrayExprVisitor.cpp.

References klee::ExprVisitor::Action::doChildren(), klee::UpdateList::head, incompatible, klee::ReadExpr::index, klee::Array::isSymbolicArray(), readInfo, reads, klee::UpdateList::root, klee::ExprVisitor::Action::skipChildren(), symbolic, and klee::ReadExpr::updates.

Referenced by visitConcat(), and visitRead().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isIncompatible()

bool klee::ArrayReadExprVisitor::isIncompatible ( )
inline

Definition at line 110 of file ArrayExprVisitor.h.

References incompatible.

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

Here is the caller graph for this function:

◆ visitConcat()

ExprVisitor::Action ArrayReadExprVisitor::visitConcat ( const ConcatExpr &  ce)
overrideprotectedvirtual

Reimplemented from klee::ExprVisitor.

Definition at line 183 of file ArrayExprVisitor.cpp.

References klee::ExprVisitor::Action::doChildren(), klee::ConcatExpr::getWidth(), klee::ArrayExprHelper::hasOrderedReads(), and inspectRead().

Here is the call graph for this function:

◆ visitRead()

ExprVisitor::Action ArrayReadExprVisitor::visitRead ( const ReadExpr &  re)
overrideprotectedvirtual

Reimplemented from klee::ExprVisitor.

Definition at line 190 of file ArrayExprVisitor.cpp.

References klee::ReadExpr::getWidth(), and inspectRead().

Here is the call graph for this function:

Member Data Documentation

◆ incompatible

bool klee::ArrayReadExprVisitor::incompatible
private

Definition at line 96 of file ArrayExprVisitor.h.

Referenced by inspectRead(), and isIncompatible().

◆ readInfo

std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width> >& klee::ArrayReadExprVisitor::readInfo
private

Definition at line 94 of file ArrayExprVisitor.h.

Referenced by inspectRead().

◆ reads

std::vector<const ReadExpr *>& klee::ArrayReadExprVisitor::reads
private

Definition at line 93 of file ArrayExprVisitor.h.

Referenced by inspectRead().

◆ symbolic

bool klee::ArrayReadExprVisitor::symbolic
private

Definition at line 95 of file ArrayExprVisitor.h.

Referenced by containsSymbolic(), and inspectRead().

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