4 files changed, 34 insertions, 18 deletions
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
index cf4ebb18..622b0e80 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/util/ExprPPrinter.h
@@ -12,6 +12,9 @@
 
 #include "klee/Expr.h"
 
+namespace llvm {
+  class raw_ostream;
+}
 namespace klee {
   class ConstraintManager;
 
@@ -20,7 +23,7 @@ namespace klee {
     ExprPPrinter() {}
     
   public:
-    static ExprPPrinter *create(std::ostream &os);
+    static ExprPPrinter *create(llvm::raw_ostream &os);
 
     virtual ~ExprPPrinter() {}
 
@@ -45,7 +48,7 @@ namespace klee {
 
     /// printOne - Pretty print a single expression prefixed by a
     /// message and followed by a line break.
-    static void printOne(std::ostream &os, const char *message, 
+    static void printOne(llvm::raw_ostream &os, const char *message,
                          const ref<Expr> &e);
 
     /// printSingleExpr - Pretty print a single expression.
@@ -55,12 +58,12 @@ namespace klee {
     /// 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.
-    static void printSingleExpr(std::ostream &os, const ref<Expr> &e);
+    static void printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e);
 
-    static void printConstraints(std::ostream &os,
+    static void printConstraints(llvm::raw_ostream &os,
                                  const ConstraintManager &constraints);
 
-    static void printQuery(std::ostream &os,
+    static void printQuery(llvm::raw_ostream &os,
                            const ConstraintManager &constraints,
                            const ref<Expr> &q,
                            const ref<Expr> *evalExprsBegin = 0,
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
index 42f38007..8b072242 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -11,7 +11,6 @@
 #ifndef KLEE_EXPRSMTLIBPRINTER_H
 #define KLEE_EXPRSMTLIBPRINTER_H
 
-#include <ostream>
 #include <string>
 #include <set>
 #include <map>
@@ -20,6 +19,10 @@
 #include <klee/util/PrintContext.h>
 #include <klee/Solver.h>
 
+namespace llvm {
+class raw_ostream;
+}
+
 namespace klee {
 
 /// Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic.
@@ -121,7 +124,7 @@ public:
 
   /// Set the output stream that will be printed to.
   /// This call is persistent across queries.
-  void setOutput(std::ostream &output);
+  void setOutput(llvm::raw_ostream &output);
 
   /// Set the query to print. This will setArrayValuesToGet()
   /// to none (i.e. no array values will be requested using
@@ -130,7 +133,7 @@ public:
 
   virtual ~ExprSMTLIBPrinter();
 
-  /// Print the query to the std::ostream
+  /// Print the query to the llvm::raw_ostream
   /// setOutput() and setQuery() must be called before calling this.
   ///
   /// All options should be set before calling this.
@@ -202,7 +205,7 @@ protected:
   std::set<const Array *> usedArrays;
 
   /// Output stream to write to
-  std::ostream *o;
+  llvm::raw_ostream *o;
 
   /// The query to print
   const Query *query;
diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h
index a9e91925..6b1ef77a 100644
--- a/include/klee/util/PrintContext.h
+++ b/include/klee/util/PrintContext.h
@@ -1,14 +1,14 @@
 #ifndef PRINTCONTEXT_H_
 #define PRINTCONTEXT_H_
 
-#include <ostream>
+#include "klee/Expr.h"
+#include "llvm/Support/raw_ostream.h"
 #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
+/// It provides a basic wrapper around llvm::raw_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
@@ -16,8 +16,7 @@
 /// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
 class PrintContext {
 private:
-  std::ostream &os;
-  std::stringstream ss;
+  llvm::raw_ostream &os;
   std::string newline;
 
   ///This is used to keep track of the stack of indentations used by
@@ -30,7 +29,7 @@ public:
   /// Number of characters on the current line.
   unsigned pos;
 
-  PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
   {
 	  indentStack.push(pos);
   }
@@ -42,7 +41,7 @@ public:
   void breakLine(unsigned indent=0) {
     os << newline;
     if (indent)
-      os << std::setw(indent) << ' ';
+      os.indent(indent) << ' ';
     pos = indent;
   }
 
@@ -79,7 +78,8 @@ public:
 
   template <typename T>
   PrintContext &operator<<(T elt) {
-    ss.str("");
+    std::string str;
+    llvm::raw_string_ostream ss(str);
     ss << elt;
     write(ss.str());
     return *this;
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index d14de471..c77149aa 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -20,6 +20,10 @@ using llvm::dyn_cast_or_null;
 #include <assert.h>
 #include <iosfwd> // FIXME: Remove this!!!
 
+namespace llvm {
+  class raw_ostream;
+}
+
 namespace klee {
 
 template<class T>
@@ -107,7 +111,13 @@ public:
 };
 
 template<class T>
-inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref<T> &e) {
+  os << *e;
+  return os;
+}
+
+template<class T>
+inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) {
   os << *e;
   return os;
 }