Inheritance diagram for PPrinter:

Collaboration diagram for PPrinter:

Public Member Functions
	PPrinter (llvm::raw_ostream &_os)

void	setNewline (const std::string &_newline)

void	setForceNoLineBreaks (bool _forceNoLineBreaks)

void	reset ()

void	scan (const ref< Expr > &e)

void	print (const ref< Expr > &e, unsigned level=0)

void	printConst (const ref< ConstantExpr > &e, PrintContext &PC, bool printWidth)

void	print (const ref< Expr > &e, PrintContext &PC, bool printConstWidth=false)

void	printSeparator (PrintContext &PC, bool simple, unsigned indent)

Public Member Functions inherited from klee::ExprPPrinter
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)

Public Attributes
std::set< const Array * >	usedArrays

Private Member Functions
bool	shouldPrintWidth (ref< Expr > e)

bool	isVerySimple (const ref< Expr > &e)

bool	isVerySimpleUpdate (const UpdateNode *un)

bool	isSimple (const ref< Expr > &e)

bool	hasSimpleKids (const Expr *ep)

void	scanUpdate (const UpdateNode *un)

void	scan1 (const ref< Expr > &e)

void	printUpdateList (const UpdateList &updates, PrintContext &PC)

void	printWidth (PrintContext &PC, ref< Expr > e)

bool	isReadExprAtOffset (ref< Expr > e, const ReadExpr *base, ref< Expr > offset)

const ReadExpr *	hasOrderedReads (ref< Expr > e, int stride)

void	printRead (const ReadExpr *re, PrintContext &PC, unsigned indent)

void	printExtract (const ExtractExpr *ee, PrintContext &PC, unsigned indent)

void	printExpr (const Expr *ep, PrintContext &PC, unsigned indent, bool printConstWidth=false)

Private Attributes
std::map< ref< Expr >, unsigned >	bindings

std::map< const UpdateNode *, unsigned >	updateBindings

std::set< ref< Expr > >	couldPrint

std::set< ref< Expr > >	shouldPrint

std::set< const UpdateNode * >	couldPrintUpdates

std::set< const UpdateNode * >	shouldPrintUpdates

llvm::raw_ostream &	os

unsigned	counter

unsigned	updateCounter

bool	hasScan

bool	forceNoLineBreaks

std::string	newline

Additional Inherited Members
Static Public Member Functions inherited from klee::ExprPPrinter
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 inherited from klee::ExprPPrinter
	ExprPPrinter ()

Detailed Description

Definition at line 58 of file ExprPPrinter.cpp.

Constructor & Destructor Documentation

◆ PPrinter()

PPrinter::PPrinter ( llvm::raw_ostream & _os )

inline

Definition at line 320 of file ExprPPrinter.cpp.

References reset().

Here is the call graph for this function:

Member Function Documentation

◆ hasOrderedReads()

const ReadExpr * PPrinter::hasOrderedReads	(	ref< Expr >	e,
		int	stride
	)

inlineprivate

hasOrderedReads:

e must be a ConcatExpr,
stride must be 1 or -1.

If all children of this Concat are reads or concats of reads with consecutive offsets according to the given

stride, it returns the base ReadExpr according to
stride: first Read for 1 (MSB), last Read for -1 (LSB). Otherwise, it returns null.

Definition at line 241 of file ExprPPrinter.cpp.

References klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getKind(), klee::ReadExpr::getWidth(), klee::Expr::getWidth(), klee::ReadExpr::index, and isReadExprAtOffset().

Referenced by print().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ hasSimpleKids()

bool PPrinter::hasSimpleKids ( const Expr * ep )

inlineprivate

Definition at line 106 of file ExprPPrinter.cpp.

References klee::Expr::getKid(), klee::Expr::getNumKids(), and isSimple().

Referenced by printExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isReadExprAtOffset()

bool PPrinter::isReadExprAtOffset	(	ref< Expr >	e,
		const ReadExpr *	base,
		ref< Expr >	offset
	)

inlineprivate

Definition at line 216 of file ExprPPrinter.cpp.

References klee::ref< T >::get(), klee::ReadExpr::getWidth(), and klee::ReadExpr::index.

Referenced by hasOrderedReads().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isSimple()

bool PPrinter::isSimple ( const ref< Expr > & e )

inlineprivate

Definition at line 91 of file ExprPPrinter.cpp.

References klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getNumKids(), isVerySimple(), and isVerySimpleUpdate().

Referenced by hasSimpleKids().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isVerySimple()

bool PPrinter::isVerySimple ( const ref< Expr > & e )

inlineprivate

Definition at line 81 of file ExprPPrinter.cpp.

References bindings.

Referenced by isSimple(), and printRead().

Here is the caller graph for this function:

◆ isVerySimpleUpdate()

bool PPrinter::isVerySimpleUpdate ( const UpdateNode * un )

inlineprivate

Definition at line 85 of file ExprPPrinter.cpp.

References updateBindings.

Referenced by isSimple().

Here is the caller graph for this function:

◆ print() [1/2]

void PPrinter::print	(	const ref< Expr > &	e,
		PrintContext &	PC,
		bool	printConstWidth = `false`
	)

inline

Definition at line 380 of file ExprPPrinter.cpp.

References bindings, counter, klee::ref< T >::get(), klee::Expr::getKind(), hasOrderedReads(), hasScan, PrintContext::pos, printConst(), printExpr(), printExtract(), printRead(), printWidth(), and shouldPrint.

Here is the call graph for this function:

◆ print() [2/2]

void PPrinter::print	(	const ref< Expr > &	e,
		unsigned	level = `0`
	)

inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 350 of file ExprPPrinter.cpp.

References os, PrintContext::pos, and print().

Referenced by print(), printExpr(), printExtract(), klee::ExprPPrinter::printOne(), klee::ExprPPrinter::printQuery(), printRead(), klee::ExprPPrinter::printSingleExpr(), and printUpdateList().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printConst()

void PPrinter::printConst	(	const ref< ConstantExpr > &	e,
		PrintContext &	PC,
		bool	printWidth
	)

inline

Definition at line 356 of file ExprPPrinter.cpp.

References printWidth().

Referenced by print().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printExpr()

void PPrinter::printExpr	(	const Expr *	ep,
		PrintContext &	PC,
		unsigned	indent,
		bool	printConstWidth = `false`
	)

inlineprivate

Definition at line 309 of file ExprPPrinter.cpp.

References klee::Expr::getKid(), klee::Expr::getNumKids(), hasSimpleKids(), print(), and printSeparator().

Referenced by print().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printExtract()

void PPrinter::printExtract	(	const ExtractExpr *	ee,
		PrintContext &	PC,
		unsigned	indent
	)

inlineprivate

Definition at line 304 of file ExprPPrinter.cpp.

References klee::ExtractExpr::expr, klee::ExtractExpr::offset, and print().

Referenced by print().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printRead()

void PPrinter::printRead	(	const ReadExpr *	re,
		PrintContext &	PC,
		unsigned	indent
	)

inlineprivate

Definition at line 298 of file ExprPPrinter.cpp.

References klee::ReadExpr::index, isVerySimple(), print(), printSeparator(), printUpdateList(), and klee::ReadExpr::updates.

Referenced by print().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printSeparator()

void PPrinter::printSeparator	(	PrintContext &	PC,
		bool	simple,
		unsigned	indent
	)

inline

Definition at line 437 of file ExprPPrinter.cpp.

References PrintContext::breakLine(), and forceNoLineBreaks.

Referenced by printExpr(), klee::ExprPPrinter::printQuery(), printRead(), and printUpdateList().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printUpdateList()

void PPrinter::printUpdateList	(	const UpdateList &	updates,
		PrintContext &	PC
	)

inlineprivate

Definition at line 142 of file ExprPPrinter.cpp.

References PrintContext::breakLine(), hasScan, klee::UpdateList::head, klee::Array::name, PrintContext::pos, print(), printSeparator(), klee::UpdateList::root, shouldPrintUpdates, updateBindings, and updateCounter.

Referenced by printRead().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printWidth()

void PPrinter::printWidth	(	PrintContext &	PC,
		ref< Expr >	e
	)

inlineprivate

Definition at line 202 of file ExprPPrinter.cpp.

References klee::Expr::getWidth(), and shouldPrintWidth().

Referenced by print(), and printConst().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reset()

void PPrinter::reset ( )

inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 332 of file ExprPPrinter.cpp.

References bindings, couldPrint, couldPrintUpdates, counter, forceNoLineBreaks, hasScan, shouldPrint, shouldPrintUpdates, updateBindings, and updateCounter.

Referenced by PPrinter().

Here is the caller graph for this function:

◆ scan()

void PPrinter::scan ( const ref< Expr > & e )

inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 345 of file ExprPPrinter.cpp.

References hasScan, and scan1().

Referenced by klee::ExprPPrinter::printOne(), klee::ExprPPrinter::printQuery(), and klee::ExprPPrinter::printSingleExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ scan1()

void PPrinter::scan1 ( const ref< Expr > & e )

inlineprivate

Definition at line 126 of file ExprPPrinter.cpp.

References couldPrint, klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getNumKids(), scan1(), scanUpdate(), shouldPrint, and usedArrays.

Referenced by scan(), scan1(), and scanUpdate().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ scanUpdate()

void PPrinter::scanUpdate ( const UpdateNode * un )

inlineprivate

Definition at line 113 of file ExprPPrinter.cpp.

References couldPrintUpdates, klee::UpdateNode::index, klee::UpdateNode::next, scan1(), scanUpdate(), shouldPrintUpdates, and klee::UpdateNode::value.

Referenced by scan1(), and scanUpdate().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setForceNoLineBreaks()

void PPrinter::setForceNoLineBreaks ( bool _forceNoLineBreaks )

inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 328 of file ExprPPrinter.cpp.

References forceNoLineBreaks.

◆ setNewline()

void PPrinter::setNewline ( const std::string & _newline )

inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 324 of file ExprPPrinter.cpp.

References newline.

◆ shouldPrintWidth()

bool PPrinter::shouldPrintWidth ( ref< Expr > e )

inlineprivate

shouldPrintWidth - Predicate for whether this expression should be printed with its width.

Definition at line 75 of file ExprPPrinter.cpp.

References klee::Expr::getWidth().

Referenced by printWidth().

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

◆ bindings

std::map<ref<Expr>, unsigned> PPrinter::bindings

private

Definition at line 62 of file ExprPPrinter.cpp.

Referenced by isVerySimple(), print(), and reset().

◆ couldPrint

std::set< ref<Expr> > PPrinter::couldPrint

private

Definition at line 64 of file ExprPPrinter.cpp.

Referenced by reset(), and scan1().

◆ couldPrintUpdates

std::set<const UpdateNode*> PPrinter::couldPrintUpdates

private

Definition at line 65 of file ExprPPrinter.cpp.

Referenced by reset(), and scanUpdate().

◆ counter

unsigned PPrinter::counter

private

Definition at line 67 of file ExprPPrinter.cpp.

Referenced by print(), and reset().

◆ forceNoLineBreaks

bool PPrinter::forceNoLineBreaks

private

Definition at line 70 of file ExprPPrinter.cpp.

Referenced by printSeparator(), reset(), and setForceNoLineBreaks().

◆ hasScan

bool PPrinter::hasScan

private

Definition at line 69 of file ExprPPrinter.cpp.

Referenced by print(), printUpdateList(), reset(), and scan().

◆ newline

std::string PPrinter::newline

private

Definition at line 71 of file ExprPPrinter.cpp.

Referenced by setNewline().

◆ os

llvm::raw_ostream& PPrinter::os

private

Definition at line 66 of file ExprPPrinter.cpp.

Referenced by print().

◆ shouldPrint

std::set< ref<Expr> > PPrinter::shouldPrint

private

Definition at line 64 of file ExprPPrinter.cpp.

Referenced by print(), reset(), and scan1().

◆ shouldPrintUpdates

std::set<const UpdateNode*> PPrinter::shouldPrintUpdates

private

Definition at line 65 of file ExprPPrinter.cpp.

Referenced by printUpdateList(), reset(), and scanUpdate().

◆ updateBindings

std::map<const UpdateNode*, unsigned> PPrinter::updateBindings

private

Definition at line 63 of file ExprPPrinter.cpp.

Referenced by isVerySimpleUpdate(), printUpdateList(), and reset().

◆ updateCounter

unsigned PPrinter::updateCounter

private

Definition at line 68 of file ExprPPrinter.cpp.

Referenced by printUpdateList(), and reset().

◆ usedArrays

std::set<const Array*> PPrinter::usedArrays

Definition at line 60 of file ExprPPrinter.cpp.

Referenced by klee::ExprPPrinter::printQuery(), and scan1().

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

/Users/cristic/klee/lib/Expr/ExprPPrinter.cpp

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ PPrinter()

Member Function Documentation

◆ hasOrderedReads()

◆ hasSimpleKids()

◆ isReadExprAtOffset()

◆ isSimple()

◆ isVerySimple()

◆ isVerySimpleUpdate()

◆ print() [1/2]

◆ print() [2/2]

◆ printConst()

◆ printExpr()

◆ printExtract()

◆ printRead()

◆ printSeparator()

◆ printUpdateList()

◆ printWidth()

◆ reset()

◆ scan()

◆ scan1()

◆ scanUpdate()

◆ setForceNoLineBreaks()

◆ setNewline()

◆ shouldPrintWidth()

Member Data Documentation

◆ bindings

◆ couldPrint

◆ couldPrintUpdates

◆ counter

◆ forceNoLineBreaks

◆ hasScan

◆ newline

◆ os

◆ shouldPrint

◆ shouldPrintUpdates

◆ updateBindings

◆ updateCounter

◆ usedArrays