klee
Public Member Functions | Static Public Member Functions | Protected Member Functions | List of all members
klee::ExprPPrinter Class Referenceabstract

#include <ExprPPrinter.h>

Inheritance diagram for klee::ExprPPrinter:
Inheritance graph
[legend]

Public Member Functions

virtual ~ExprPPrinter ()
 
virtual void setNewline (const std::string &newline)=0
 
virtual void setForceNoLineBreaks (bool forceNoLineBreaks)=0
 
virtual void reset ()=0
 
virtual void scan (const ref< Expr > &e)=0
 
virtual void print (const ref< Expr > &e, unsigned indent=0)=0
 
template<class Container >
void scan (Container c)
 
template<class InputIterator >
void scan (InputIterator it, InputIterator end)
 

Static Public Member Functions

static ExprPPrinter * create (llvm::raw_ostream &os)
 
static void printOne (llvm::raw_ostream &os, const char *message, const ref< Expr > &e)
 
static void printSingleExpr (llvm::raw_ostream &os, const ref< Expr > &e)
 
static void printConstraints (llvm::raw_ostream &os, const ConstraintSet &constraints)
 
static void printQuery (llvm::raw_ostream &os, const ConstraintSet &constraints, const ref< Expr > &q, const ref< Expr > *evalExprsBegin=0, const ref< Expr > *evalExprsEnd=0, const Array *const *evalArraysBegin=0, const Array *const *evalArraysEnd=0, bool printArrayDecls=true)
 

Protected Member Functions

 ExprPPrinter ()
 

Detailed Description

Definition at line 21 of file ExprPPrinter.h.

Constructor & Destructor Documentation

◆ ExprPPrinter()

klee::ExprPPrinter::ExprPPrinter ( )
inlineprotected

Definition at line 23 of file ExprPPrinter.h.

◆ ~ExprPPrinter()

virtual klee::ExprPPrinter::~ExprPPrinter ( )
inlinevirtual

Definition at line 28 of file ExprPPrinter.h.

Member Function Documentation

◆ create()

ExprPPrinter * klee::ExprPPrinter::create ( llvm::raw_ostream &  os)
static

Definition at line 446 of file ExprPPrinter.cpp.

Referenced by klee::PTree::dump().

Here is the caller graph for this function:

◆ print()

virtual void klee::ExprPPrinter::print ( const ref< Expr > &  e,
unsigned  indent = 0 
)
pure virtual

Implemented in PPrinter.

◆ printConstraints()

void ExprPPrinter::printConstraints ( llvm::raw_ostream &  os,
const ConstraintSet &  constraints 
)
static

Definition at line 474 of file ExprPPrinter.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Bool, and printQuery().

Referenced by klee::Executor::getConstraintLog().

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

◆ printOne()

void ExprPPrinter::printOne ( llvm::raw_ostream &  os,
const char *  message,
const ref< Expr > &  e 
)
static

printOne - Pretty print a single expression prefixed by a message and followed by a line break.

Definition at line 450 of file ExprPPrinter.cpp.

References PrintContext::breakLine(), message, PPrinter::print(), and PPrinter::scan().

Referenced by klee::Executor::executeAlloc().

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

◆ printQuery()

void ExprPPrinter::printQuery ( llvm::raw_ostream &  os,
const ConstraintSet &  constraints,
const ref< Expr > &  q,
const ref< Expr > *  evalExprsBegin = 0,
const ref< Expr > *  evalExprsEnd = 0,
const Array *const *  evalArraysBegin = 0,
const Array *const *  evalArraysEnd = 0,
bool  printArrayDecls = true 
)
static

Definition at line 488 of file ExprPPrinter.cpp.

References klee::ConstraintSet::begin(), PrintContext::breakLine(), klee::ConstraintSet::empty(), klee::ConstraintSet::end(), klee::Expr::isFalse(), PrintContext::pos, PPrinter::print(), PPrinter::printSeparator(), PPrinter::scan(), and PPrinter::usedArrays.

Referenced by klee::expr::QueryCommand::dump(), klee::Executor::getSymbolicSolution(), printConstraints(), and KQueryLoggingSolver::printQuery().

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

◆ printSingleExpr()

void ExprPPrinter::printSingleExpr ( llvm::raw_ostream &  os,
const ref< Expr > &  e 
)
static

printSingleExpr - Pretty print a single expression.

The expression will not be followed by a line break.

Note that if the output stream is not positioned at the beginning of a line then printing will not resume at the correct position following any output line breaks.

Definition at line 464 of file ExprPPrinter.cpp.

References PPrinter::print(), and PPrinter::scan().

Referenced by klee::Expr::print().

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

◆ reset()

virtual void klee::ExprPPrinter::reset ( )
pure virtual

Implemented in PPrinter.

◆ scan() [1/3]

virtual void klee::ExprPPrinter::scan ( const ref< Expr > &  e)
pure virtual

Implemented in PPrinter.

Referenced by scan().

Here is the caller graph for this function:

◆ scan() [2/3]

template<class Container >
void klee::ExprPPrinter::scan ( Container  c)
inline

Definition at line 39 of file ExprPPrinter.h.

References scan().

Here is the call graph for this function:

◆ scan() [3/3]

template<class InputIterator >
void klee::ExprPPrinter::scan ( InputIterator  it,
InputIterator  end 
)
inline

Definition at line 44 of file ExprPPrinter.h.

References scan().

Here is the call graph for this function:

◆ setForceNoLineBreaks()

virtual void klee::ExprPPrinter::setForceNoLineBreaks ( bool  forceNoLineBreaks)
pure virtual

Implemented in PPrinter.

◆ setNewline()

virtual void klee::ExprPPrinter::setNewline ( const std::string &  newline)
pure virtual

Implemented in PPrinter.

Referenced by klee::PTree::dump().

Here is the caller graph for this function:
The documentation for this class was generated from the following files: