Commit dc391fc6 authored by Cristian Cadar's avatar Cristian Cadar Committed by Dan Liew
Browse files

Patch by Dan Liew: "Moved PrintContext class out of ExprPrinter.cpp so

it can be used by other classes. It has also been improved so it can
be used with the soon to be added ExprSMTLIBPrinter classes."

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166555 91177308-0d34-0410-b5e6-96231b3b80d8
parent fddd26a3
#ifndef PRINTCONTEXT_H_
#define PRINTCONTEXT_H_
#include <ostream>
#include <sstream>
#include <string>
#include <stack>
#include <iomanip>
/// PrintContext - Helper class for pretty printing.
/// It provides a basic wrapper around std::ostream that keeps track of
/// how many characters have been used on the current line.
///
/// It also provides an optional way keeping track of the various levels of indentation
/// by using a stack.
/// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
class PrintContext {
private:
std::ostream &os;
std::stringstream ss;
std::string newline;
///This is used to keep track of the stack of indentations used by
/// \sa breakLineI()
/// \sa pushIndent()
/// \sa popIndent()
std::stack<unsigned int> indentStack;
public:
/// Number of characters on the current line.
unsigned pos;
PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
{
indentStack.push(pos);
}
void setNewline(const std::string &_newline) {
newline = _newline;
}
void breakLine(unsigned indent=0) {
os << newline;
if (indent)
os << std::setw(indent) << ' ';
pos = indent;
}
///Break line using the indent on the top of the indent stack
/// \return The PrintContext object so the method is chainable
PrintContext& breakLineI()
{
breakLine(indentStack.top());
return *this;
}
///Add the current position on the line to the top of the indent stack
/// \return The PrintContext object so the method is chainable
PrintContext& pushIndent()
{
indentStack.push(pos);
return *this;
}
///Pop the top off the indent stack
/// \return The PrintContext object so the method is chainable
PrintContext& popIndent()
{
indentStack.pop();
return *this;
}
/// write - Output a string to the stream and update the
/// position. The stream should not have any newlines.
void write(const std::string &s) {
os << s;
pos += s.length();
}
template <typename T>
PrintContext &operator<<(T elt) {
ss.str("");
ss << elt;
write(ss.str());
return *this;
}
};
#endif /* PRINTCONTEXT_H_ */
......@@ -7,6 +7,7 @@
//
//===----------------------------------------------------------------------===//
#include "klee/util/PrintContext.h"
#include "klee/util/ExprPPrinter.h"
#include "klee/Constraints.h"
......@@ -38,48 +39,6 @@ namespace {
PCAllConstWidths("pc-all-const-widths", llvm::cl::init(false));
}
/// PrintContext - Helper class for storing extra information for
/// the pretty printer.
class PrintContext {
private:
std::ostream &os;
std::stringstream ss;
std::string newline;
public:
/// Number of characters on the current line.
unsigned pos;
public:
PrintContext(std::ostream &_os) : os(_os), newline("\n"), pos(0) {}
void setNewline(const std::string &_newline) {
newline = _newline;
}
void breakLine(unsigned indent=0) {
os << newline;
if (indent)
os << std::setw(indent) << ' ';
pos = indent;
}
/// write - Output a string to the stream and update the
/// position. The stream should not have any newlines.
void write(const std::string &s) {
os << s;
pos += s.length();
}
template <typename T>
PrintContext &operator<<(T elt) {
ss.str("");
ss << elt;
write(ss.str());
return *this;
}
};
class PPrinter : public ExprPPrinter {
public:
std::set<const Array*> usedArrays;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment