5 files changed, 54 insertions, 41 deletions

diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 6e52dc32..a488db2a 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -18,6 +18,7 @@
 // FIXME: Use APInt.
 #include "klee/Internal/Support/IntEvaluation.h"
 
+#include "llvm/Support/raw_ostream.h"
 #include <iostream>
 #include <sstream>
 #include <cassert>
@@ -109,7 +110,7 @@ public:
   ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {}
   ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {}
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     if (isFixed()) {
       os << m_min;
     } else {
@@ -283,7 +284,8 @@ public:
   }
 };
 
-inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const ValueRange &vr) {
   vr.print(os);
   return os;
 }
@@ -443,7 +445,7 @@ public:
 
   void propogatePossibleValues(ref<Expr> e, CexValueData range) {
     #ifdef DEBUG
-    std::cerr << "propogate: " << range << " for\n" << e << "\n";
+        llvm::errs() << "propogate: " << range << " for\n" << e << "\n";
     #endif
 
     switch (e->getKind()) {
@@ -938,27 +940,29 @@ public:
   }
 
   void dump() {
-    std::cerr << "-- propogated values --\n";
-    for (std::map<const Array*, CexObjectData*>::iterator 
-           it = objects.begin(), ie = objects.end(); it != ie; ++it) {
+    llvm::errs() << "-- propogated values --\n";
+    for (std::map<const Array *, CexObjectData *>::iterator
+             it = objects.begin(),
+             ie = objects.end();
+         it != ie; ++it) {
       const Array *A = it->first;
       CexObjectData *COD = it->second;
-    
-      std::cerr << A->name << "\n";
-      std::cerr << "possible: [";
+
+      llvm::errs() << A->name << "\n";
+      llvm::errs() << "possible: [";
       for (unsigned i = 0; i < A->size; ++i) {
         if (i)
-          std::cerr << ", ";
-        std::cerr << COD->getPossibleValues(i);
+          llvm::errs() << ", ";
+        llvm::errs() << COD->getPossibleValues(i);
       }
-      std::cerr << "]\n";
-      std::cerr << "exact   : [";
+      llvm::errs() << "]\n";
+      llvm::errs() << "exact   : [";
       for (unsigned i = 0; i < A->size; ++i) {
         if (i)
-          std::cerr << ", ";
-        std::cerr << COD->getExactValues(i);
+          llvm::errs() << ", ";
+        llvm::errs() << COD->getExactValues(i);
       }
-      std::cerr << "]\n";
+      llvm::errs() << "]\n";
     }
   }
 };
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index d9fc77dc..3c0b9b26 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -15,6 +15,7 @@
 
 #include "klee/util/ExprUtil.h"
 
+#include "llvm/Support/raw_ostream.h"
 #include <map>
 #include <vector>
 #include <ostream>
@@ -60,7 +61,7 @@ public:
     return false;
   }
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     bool first = true;
     os << "{";
     for (typename set_ty::iterator it = s.begin(), ie = s.end(); 
@@ -76,8 +77,9 @@ public:
   }
 };
 
-template<class T>
-inline std::ostream &operator<<(std::ostream &os, const ::DenseSet<T> &dis) {
+template <class T>
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const ::DenseSet<T> &dis) {
   dis.print(os);
   return os;
 }
@@ -124,7 +126,7 @@ public:
     return *this;
   }
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     os << "{";
     bool first = true;
     for (std::set<const Array*>::iterator it = wholeObjects.begin(), 
@@ -214,7 +216,8 @@ public:
   }
 };
 
-inline std::ostream &operator<<(std::ostream &os, const IndependentElementSet &ies) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const IndependentElementSet &ies) {
   ies.print(os);
   return os;
 }
@@ -247,20 +250,22 @@ IndependentElementSet getIndependentConstraints(const Query& query,
     worklist.swap(newWorklist);
   } while (!done);
 
+#if 0
   if (0) {
     std::set< ref<Expr> > reqset(result.begin(), result.end());
-    std::cerr << "--\n";
-    std::cerr << "Q: " << query.expr << "\n";
-    std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n";
+    errs() << "--\n";
+    errs() << "Q: " << query.expr << "\n";
+    errs() << "\telts: " << IndependentElementSet(query.expr) << "\n";
     int i = 0;
-  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
-         ie = query.constraints.end(); it != ie; ++it) {
-      std::cerr << "C" << i++ << ": " << *it;
-      std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
-      std::cerr << "\telts: " << IndependentElementSet(*it) << "\n";
+    for (ConstraintManager::const_iterator it = query.constraints.begin(),
+        ie = query.constraints.end(); it != ie; ++it) {
+      errs() << "C" << i++ << ": " << *it;
+      errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
+      errs() << "\telts: " << IndependentElementSet(*it) << "\n";
     }
-    std::cerr << "elts closure: " << eltsClosure << "\n";
+    errs() << "elts closure: " << eltsClosure << "\n";
   }
+#endif
 
   return eltsClosure;
 }
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index f1e55614..b5c99907 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -599,9 +599,9 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu
     
     ++stats::queryConstructs;
     
-//     std::cerr << "Constructing expression ";
-//     ExprPPrinter::printSingleExpr(std::cerr, e);
-//     std::cerr << "\n";
+//     llvm::errs() << "Constructing expression ";
+//     ExprPPrinter::printSingleExpr(llvm::errs(), e);
+//     llvm::errs() << "\n";
 
     switch (e->getKind()) {
 
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index f2e38182..d5598d1d 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -18,9 +18,10 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver,
                                        std::string path,
                                        const std::string& commentSign,
                                        int queryTimeToLog)                                  
-    : solver(_solver), 
-      os(path.c_str(), std::ios::trunc),
-      logBuffer(""),
+    : solver(_solver),
+      os(path.c_str(), ErrorInfo),
+      BufferString(""),
+      logBuffer(BufferString),
       queryCount(0),    
       minQueryTimeToLog(queryTimeToLog),
       startTime(0.0f),
@@ -79,8 +80,7 @@ void QueryLoggingSolver::flushBuffer() {
       }
       
       // prepare the buffer for reuse
-      logBuffer.clear();
-      logBuffer.str("");
+      BufferString = "";
 }
 
 bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) {
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 2c7d80e8..ad1722ca 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -12,6 +12,7 @@
 
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
+#include "llvm/Support/raw_ostream.h"
 #include <fstream>
 #include <sstream>
 
@@ -25,9 +26,12 @@ class QueryLoggingSolver : public SolverImpl {
 
 protected:
     Solver *solver;
-    std::ofstream os;
-    std::ostringstream logBuffer; // buffer to store logs before flushing to 
-                                  // file
+    std::string ErrorInfo;
+    llvm::raw_fd_ostream os;
+    // @brief Buffer used by logBuffer
+    std::string BufferString;
+    // @brief buffer to store logs before flushing to file
+    llvm::raw_string_ostream logBuffer;
     unsigned queryCount;
     int minQueryTimeToLog; // we log to file only those queries
                            // which take longer than the specified time (ms);