klee::ExprPPrinter Class Reference

#include <ExprPPrinter.h>

Inheritance diagram for klee::ExprPPrinter:

[legend]

List of all members.

Public Member Functions
virtual	~ExprPPrinter ()
virtual void	setNewline (const std::string &newline)=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 (std::ostream &os)
static void	printOne (std::ostream &os, const char *message, const ref< Expr > &e)
static void	printSingleExpr (std::ostream &os, const ref< Expr > &e)
static void	printConstraints (std::ostream &os, const ConstraintManager &constraints)
static void	printQuery (std::ostream &os, const ConstraintManager &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)
Protected Member Functions
	ExprPPrinter ()

---

Detailed Description

Definition at line 18 of file ExprPPrinter.h.

---

Constructor & Destructor Documentation

klee::ExprPPrinter::ExprPPrinter

(

)

[inline, protected]

Definition at line 20 of file ExprPPrinter.h.

virtual klee::ExprPPrinter::~ExprPPrinter

(

)

[inline, virtual]

Definition at line 25 of file ExprPPrinter.h.

---

Member Function Documentation

ExprPPrinter * klee::ExprPPrinter::create

(

std::ostream &

os

)

[static]

Definition at line 468 of file ExprPPrinter.cpp.

Referenced by klee::PTree::dump(), PPrinter::hasOrderedReads(), and PPrinter::isReadExprAtOffset().

Here is the caller graph for this function:

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

Implemented in PPrinter.

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

Here is the caller graph for this function:

void ExprPPrinter::printConstraints	(	std::ostream &	os,
		const ConstraintManager &	constraints
	)			[static]

Definition at line 496 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:

void ExprPPrinter::printOne	(	std::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 472 of file ExprPPrinter.cpp.

References PrintContext::breakLine(), 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:

void ExprPPrinter::printQuery	(	std::ostream &	os,
		const ConstraintManager &	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
	)			[static]

Definition at line 502 of file ExprPPrinter.cpp.

References klee::ConstraintManager::begin(), PrintContext::breakLine(), klee::ConstraintManager::empty(), klee::ConstraintManager::end(), PrintContext::pos, PPrinter::print(), PPrinter::printSeparator(), and PPrinter::scan().

Referenced by klee::expr::QueryCommand::dump(), klee::Executor::getSymbolicSolution(), printConstraints(), and PCLoggingSolver::startQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

void ExprPPrinter::printSingleExpr	(	std::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 486 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:

virtual void klee::ExprPPrinter::reset

(

)

[pure virtual]

Implemented in PPrinter.

template<class InputIterator >

void klee::ExprPPrinter::scan	(	InputIterator	it,
		InputIterator	end
	)			[inline]

Definition at line 40 of file ExprPPrinter.h.

References scan().

Here is the call graph for this function:

template<class Container >

void klee::ExprPPrinter::scan

(

Container

c

)

[inline]

Definition at line 35 of file ExprPPrinter.h.

References scan().

Here is the call graph for this function:

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:

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:

• include/klee/util/ExprPPrinter.h
• lib/Expr/ExprPPrinter.cpp