about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h2
-rw-r--r--include/klee/util/Ref.h2
-rw-r--r--lib/Core/ExecutionState.cpp34
-rw-r--r--lib/Core/Executor.cpp13
-rw-r--r--lib/Core/ExecutorTimers.cpp2
-rw-r--r--lib/Core/ExecutorUtil.cpp5
-rw-r--r--lib/Core/ExternalDispatcher.cpp4
-rw-r--r--lib/Core/ImpliedValue.cpp6
-rw-r--r--lib/Core/Memory.cpp23
-rw-r--r--lib/Core/Searcher.cpp22
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp22
-rw-r--r--lib/Expr/Expr.cpp6
-rw-r--r--lib/Expr/Lexer.cpp8
-rw-r--r--lib/Expr/Parser.cpp18
-rw-r--r--lib/Module/InstructionInfoTable.cpp11
-rw-r--r--lib/Module/KModule.cpp26
-rw-r--r--lib/Module/ModuleUtil.cpp1
-rw-r--r--lib/Solver/FastCexSolver.cpp22
-rw-r--r--lib/Solver/IndependentSolver.cpp18
-rw-r--r--tools/kleaver/main.cpp44
-rw-r--r--tools/klee/Debug.cpp8
-rw-r--r--tools/klee/main.cpp38
-rw-r--r--unittests/Expr/ExprTest.cpp1
-rw-r--r--unittests/Solver/SolverTest.cpp1
24 files changed, 174 insertions, 163 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 9edcd8d0..b0f36e1c 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -15,10 +15,10 @@
 
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/SmallVector.h"
-#include "llvm/Support/Streams.h"
 
 #include <set>
 #include <vector>
+#include <iosfwd> // FIXME: Remove this!!!
 
 namespace llvm {
   class Type;
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index 61e91f3c..1b823f56 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -11,7 +11,6 @@
 #define KLEE_REF_H
 
 #include "llvm/Support/Casting.h"
-#include "llvm/Support/Streams.h"
 using llvm::isa;
 using llvm::cast;
 using llvm::cast_or_null;
@@ -19,6 +18,7 @@ using llvm::dyn_cast;
 using llvm::dyn_cast_or_null;
 
 #include <assert.h>
+#include <iosfwd> // FIXME: Remove this!!!
 
 namespace klee {
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 9eb560b8..694b21b1 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -147,7 +147,7 @@ std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) {
 
 bool ExecutionState::merge(const ExecutionState &b) {
   if (DebugLogStateMerge)
-    llvm::cerr << "-- attempting merge of A:" 
+    std::cerr << "-- attempting merge of A:" 
                << this << " with B:" << &b << "--\n";
   if (pc != b.pc)
     return false;
@@ -185,21 +185,21 @@ bool ExecutionState::merge(const ExecutionState &b) {
                       commonConstraints.begin(), commonConstraints.end(),
                       std::inserter(bSuffix, bSuffix.end()));
   if (DebugLogStateMerge) {
-    llvm::cerr << "\tconstraint prefix: [";
+    std::cerr << "\tconstraint prefix: [";
     for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(), 
            ie = commonConstraints.end(); it != ie; ++it)
-      llvm::cerr << *it << ", ";
-    llvm::cerr << "]\n";
-    llvm::cerr << "\tA suffix: [";
+      std::cerr << *it << ", ";
+    std::cerr << "]\n";
+    std::cerr << "\tA suffix: [";
     for (std::set< ref<Expr> >::iterator it = aSuffix.begin(), 
            ie = aSuffix.end(); it != ie; ++it)
-      llvm::cerr << *it << ", ";
-    llvm::cerr << "]\n";
-    llvm::cerr << "\tB suffix: [";
+      std::cerr << *it << ", ";
+    std::cerr << "]\n";
+    std::cerr << "\tB suffix: [";
     for (std::set< ref<Expr> >::iterator it = bSuffix.begin(), 
            ie = bSuffix.end(); it != ie; ++it)
-      llvm::cerr << *it << ", ";
-    llvm::cerr << "]\n";
+      std::cerr << *it << ", ";
+    std::cerr << "]\n";
   }
 
   // We cannot merge if addresses would resolve differently in the
@@ -212,9 +212,9 @@ bool ExecutionState::merge(const ExecutionState &b) {
   // and not the other
 
   if (DebugLogStateMerge) {
-    llvm::cerr << "\tchecking object states\n";
-    llvm::cerr << "A: " << addressSpace.objects << "\n";
-    llvm::cerr << "B: " << b.addressSpace.objects << "\n";
+    std::cerr << "\tchecking object states\n";
+    std::cerr << "A: " << addressSpace.objects << "\n";
+    std::cerr << "B: " << b.addressSpace.objects << "\n";
   }
     
   std::set<const MemoryObject*> mutated;
@@ -226,22 +226,22 @@ bool ExecutionState::merge(const ExecutionState &b) {
     if (ai->first != bi->first) {
       if (DebugLogStateMerge) {
         if (ai->first < bi->first) {
-          llvm::cerr << "\t\tB misses binding for: " << ai->first->id << "\n";
+          std::cerr << "\t\tB misses binding for: " << ai->first->id << "\n";
         } else {
-          llvm::cerr << "\t\tA misses binding for: " << bi->first->id << "\n";
+          std::cerr << "\t\tA misses binding for: " << bi->first->id << "\n";
         }
       }
       return false;
     }
     if (ai->second != bi->second) {
       if (DebugLogStateMerge)
-        llvm::cerr << "\t\tmutated: " << ai->first->id << "\n";
+        std::cerr << "\t\tmutated: " << ai->first->id << "\n";
       mutated.insert(ai->first);
     }
   }
   if (ai!=ae || bi!=be) {
     if (DebugLogStateMerge)
-      llvm::cerr << "\t\tmappings differ\n";
+      std::cerr << "\t\tmappings differ\n";
     return false;
   }
   
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 35238793..d865bcb5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1074,7 +1074,8 @@ void Executor::executeGetValue(ExecutionState &state,
 void Executor::stepInstruction(ExecutionState &state) {
   if (DebugPrintInstructions) {
     printFileLine(state, state.pc);
-    llvm::cerr << std::setw(10) << stats::instructions << " " << *state.pc->inst;
+    std::cerr << std::setw(10) << stats::instructions << " ";
+    llvm::errs() << *(state.pc->inst);
   }
 
   if (statsTracker)
@@ -1273,9 +1274,9 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
 void Executor::printFileLine(ExecutionState &state, KInstruction *ki) {
   const InstructionInfo &ii = *ki->info;
   if (ii.file != "") 
-    llvm::cerr << "     " << ii.file << ":" << ii.line << ":";
+    std::cerr << "     " << ii.file << ":" << ii.line << ":";
   else
-    llvm::cerr << "     [no debug info]:";
+    std::cerr << "     [no debug info]:";
 }
 
 
@@ -2374,7 +2375,7 @@ void Executor::run(ExecutionState &initialState) {
   
  dump:
   if (DumpStatesOnHalt && !states.empty()) {
-    llvm::cerr << "KLEE: halting execution, dumping remaining states\n";
+    std::cerr << "KLEE: halting execution, dumping remaining states\n";
     for (std::set<ExecutionState*>::iterator
            it = states.begin(), ie = states.end();
          it != ie; ++it) {
@@ -2558,7 +2559,7 @@ void Executor::callExternalFunction(ExecutionState &state,
     return;
   
   if (NoExternals && !okExternals.count(function->getName())) {
-    llvm::cerr << "KLEE:ERROR: Calling not-OK external function : " 
+    std::cerr << "KLEE:ERROR: Calling not-OK external function : " 
                << function->getNameStr() << "\n";
     terminateStateOnError(state, "externals disallowed", "user.err");
     return;
@@ -2653,7 +2654,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
                                  Expr::getMinBytesForWidth(e->getWidth()));
   ref<Expr> res = Expr::createTempRead(array, e->getWidth());
   ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
-  llvm::cerr << "Making symbolic: " << eq << "\n";
+  std::cerr << "Making symbolic: " << eq << "\n";
   state.addConstraint(eq);
   return res;
 }
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 0c274d5c..8934a6cd 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -47,7 +47,7 @@ public:
   ~HaltTimer() {}
 
   void run() {
-    llvm::cerr << "KLEE: HaltTimer invoked\n";
+    std::cerr << "KLEE: HaltTimer invoked\n";
     executor->setHaltExecution(true);
   }
 };
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 69bb2017..32fee991 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -24,7 +24,6 @@
 #include "llvm/ModuleProvider.h"
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/GetElementPtrTypeIterator.h"
-#include "llvm/Support/Streams.h"
 #include "llvm/Target/TargetData.h"
 #include <iostream>
 #include <cassert>
@@ -47,8 +46,8 @@ namespace klee {
     switch (ce->getOpcode()) {
     default :
       ce->dump();
-      llvm::cerr << "error: unknown ConstantExpr type\n"
-                 << "opcode: " << ce->getOpcode() << "\n";
+      std::cerr << "error: unknown ConstantExpr type\n"
+                << "opcode: " << ce->getOpcode() << "\n";
       abort();
 
     case Instruction::Trunc: 
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index e5b00b7f..94dad33c 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -18,11 +18,11 @@
 #include "llvm/ExecutionEngine/GenericValue.h"
 #include "llvm/Support/CallSite.h"
 #include "llvm/System/DynamicLibrary.h"
-#include "llvm/Support/Streams.h"
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Target/TargetSelect.h"
 #include <setjmp.h>
 #include <signal.h>
+#include <iostream>
 
 using namespace llvm;
 using namespace klee;
@@ -73,7 +73,7 @@ ExternalDispatcher::ExternalDispatcher() {
   std::string error;
   executionEngine = ExecutionEngine::createJIT(MP, &error);
   if (!executionEngine) {
-    llvm::cerr << "unable to make jit: " << error << "\n";
+    std::cerr << "unable to make jit: " << error << "\n";
     abort();
   }
 
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index a3d30f76..56c1d1a9 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -246,9 +246,9 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
     } else {
       if (it!=found.end()) {
         ref<Expr> binding = it->second;
-        llvm::cerr << "checkForImpliedValues: " << e  << " = " << value << "\n"
-                   << "\t\t implies " << var << " == " << binding
-                   << " (error)\n";
+        std::cerr << "checkForImpliedValues: " << e  << " = " << value << "\n"
+                  << "\t\t implies " << var << " == " << binding
+                  << " (error)\n";
         assert(0);
       }
     }
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index aa170ceb..08c0696c 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -22,6 +22,7 @@
 #include <llvm/Instruction.h>
 #include <llvm/Value.h>
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include <iostream>
 #include <cassert>
@@ -65,7 +66,7 @@ MemoryObject::~MemoryObject() {
 }
 
 void MemoryObject::getAllocInfo(std::string &result) const {
-  std::ostringstream info;
+  llvm::raw_string_ostream info(result);
 
   info << "MO" << id << "[" << size << "]";
 
@@ -83,7 +84,7 @@ void MemoryObject::getAllocInfo(std::string &result) const {
     info << " (no allocation info)";
   }
   
-  result = info.str();
+  info.flush();
 }
 
 /***/
@@ -558,23 +559,23 @@ void ObjectState::write64(unsigned offset, uint64_t value) {
 }
 
 void ObjectState::print() {
-  llvm::cerr << "-- ObjectState --\n";
-  llvm::cerr << "\tMemoryObject ID: " << object->id << "\n";
-  llvm::cerr << "\tRoot Object: " << updates.root << "\n";
-  llvm::cerr << "\tSize: " << size << "\n";
+  std::cerr << "-- ObjectState --\n";
+  std::cerr << "\tMemoryObject ID: " << object->id << "\n";
+  std::cerr << "\tRoot Object: " << updates.root << "\n";
+  std::cerr << "\tSize: " << size << "\n";
 
-  llvm::cerr << "\tBytes:\n";
+  std::cerr << "\tBytes:\n";
   for (unsigned i=0; i<size; i++) {
-    llvm::cerr << "\t\t["<<i<<"]"
+    std::cerr << "\t\t["<<i<<"]"
                << " concrete? " << isByteConcrete(i)
                << " known-sym? " << isByteKnownSymbolic(i)
                << " flushed? " << isByteFlushed(i) << " = ";
     ref<Expr> e = read8(i);
-    llvm::cerr << e << "\n";
+    std::cerr << e << "\n";
   }
 
-  llvm::cerr << "\tUpdates:\n";
+  std::cerr << "\tUpdates:\n";
   for (const UpdateNode *un=updates.head; un; un=un->next) {
-    llvm::cerr << "\t\t[" << un->index << "] = " << un->value << "\n";
+    std::cerr << "\t\t[" << un->index << "] = " << un->value << "\n";
   }
 }
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 4c94c59b..6fa75a26 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -374,17 +374,17 @@ ExecutionState &MergingSearcher::selectState() {
   }
   
   if (DebugLogMerge)
-    llvm::cerr << "-- all at merge --\n";
+    std::cerr << "-- all at merge --\n";
   for (std::map<Instruction*, std::vector<ExecutionState*> >::iterator
          it = merges.begin(), ie = merges.end(); it != ie; ++it) {
     if (DebugLogMerge) {
-      llvm::cerr << "\tmerge: " << it->first << " [";
+      std::cerr << "\tmerge: " << it->first << " [";
       for (std::vector<ExecutionState*>::iterator it2 = it->second.begin(),
              ie2 = it->second.end(); it2 != ie2; ++it2) {
         ExecutionState *state = *it2;
-        llvm::cerr << state << ", ";
+        std::cerr << state << ", ";
       }
-      llvm::cerr << "]\n";
+      std::cerr << "]\n";
     }
 
     // merge states
@@ -403,13 +403,13 @@ ExecutionState &MergingSearcher::selectState() {
         }
       }
       if (DebugLogMerge && !toErase.empty()) {
-        llvm::cerr << "\t\tmerged: " << base << " with [";
+        std::cerr << "\t\tmerged: " << base << " with [";
         for (std::set<ExecutionState*>::iterator it = toErase.begin(),
                ie = toErase.end(); it != ie; ++it) {
-          if (it!=toErase.begin()) llvm::cerr << ", ";
-          llvm::cerr << *it;
+          if (it!=toErase.begin()) std::cerr << ", ";
+          std::cerr << *it;
         }
-        llvm::cerr << "]\n";
+        std::cerr << "]\n";
       }
       for (std::set<ExecutionState*>::iterator it = toErase.begin(),
              ie = toErase.end(); it != ie; ++it) {
@@ -427,7 +427,7 @@ ExecutionState &MergingSearcher::selectState() {
   }
   
   if (DebugLogMerge)
-    llvm::cerr << "-- merge complete, continuing --\n";
+    std::cerr << "-- merge complete, continuing --\n";
   
   return selectState();
 }
@@ -475,7 +475,7 @@ ExecutionState &BatchingSearcher::selectState() {
     if (lastState) {
       double delta = util::getWallTime()-lastStartTime;
       if (delta>timeBudget*1.1) {
-        llvm::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n";
+        std::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n";
         timeBudget = delta;
       }
     }
@@ -541,7 +541,7 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current,
 
   if (baseSearcher->empty()) {
     time *= 2;
-    llvm::cerr << "KLEE: increasing time budget to: " << time << "\n";
+    std::cerr << "KLEE: increasing time budget to: " << time << "\n";
     baseSearcher->update(0, pausedStates, std::set<ExecutionState*>());
     pausedStates.clear();
   }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 45202c19..ba86428d 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -216,7 +216,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state,
 
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    llvm::cerr << "TAINT: skipping abort fail\n";
+    std::cerr << "TAINT: skipping abort fail\n";
     executor.terminateState(state);
   } else {
     executor.terminateStateOnError(state, "abort failure", "abort.err");
@@ -244,7 +244,7 @@ void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state,
          "invalid number of arguments to klee_alias_function");
   std::string old_fn = readStringAtAddress(state, arguments[0]);
   std::string new_fn = readStringAtAddress(state, arguments[1]);
-  //llvm::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n";
+  //std::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n";
   if (old_fn == new_fn)
     state.removeFnAlias(old_fn);
   else state.addFnAlias(old_fn, new_fn);
@@ -257,7 +257,7 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state,
   
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    llvm::cerr << "TAINT: skipping assertion:" 
+    std::cerr << "TAINT: skipping assertion:" 
                << readStringAtAddress(state, arguments[0]) << "\n";
     executor.terminateState(state);
   } else
@@ -273,7 +273,7 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
   
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    llvm::cerr << "TAINT: skipping assertion:" 
+    std::cerr << "TAINT: skipping assertion:" 
                << readStringAtAddress(state, arguments[0]) << "\n";
     executor.terminateState(state);
   } else
@@ -291,7 +291,7 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state,
   
   //XXX:DRE:TAINT
   if(state.underConstrained) {
-    llvm::cerr << "TAINT: skipping klee_report_error:"
+    std::cerr << "TAINT: skipping klee_report_error:"
                << readStringAtAddress(state, arguments[2]) << ":"
                << readStringAtAddress(state, arguments[3]) << "\n";
     executor.terminateState(state);
@@ -409,7 +409,7 @@ void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
          "invalid number of arguments to klee_print_expr");
 
   std::string msg_str = readStringAtAddress(state, arguments[0]);
-  llvm::cerr << msg_str << ":" << arguments[1] << "\n";
+  std::cerr << msg_str << ":" << arguments[1] << "\n";
 }
 
 void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
@@ -456,7 +456,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
          "invalid number of arguments to klee_print_range");
 
   std::string msg_str = readStringAtAddress(state, arguments[0]);
-  llvm::cerr << msg_str << ":" << arguments[1];
+  std::cerr << msg_str << ":" << arguments[1];
   if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
     ref<ConstantExpr> value;
@@ -468,15 +468,15 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
                                           res);
     assert(success && "FIXME: Unhandled solver failure");
     if (res) {
-      llvm::cerr << " == " << value;
+      std::cerr << " == " << value;
     } else { 
-      llvm::cerr << " ~= " << value;
+      std::cerr << " ~= " << value;
       std::pair< ref<Expr>, ref<Expr> > res =
         executor.solver->getRange(state, arguments[1]);
-      llvm::cerr << " (in [" << res.first << ", " << res.second <<"])";
+      std::cerr << " (in [" << res.first << ", " << res.second <<"])";
     }
   }
-  llvm::cerr << "\n";
+  std::cerr << "\n";
 }
 
 void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state,
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index b1bf9824..386d29de 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -10,13 +10,13 @@
 #include "klee/Expr.h"
 
 #include "llvm/Support/CommandLine.h"
-#include "llvm/Support/Streams.h"
 // FIXME: We shouldn't need this once fast constant support moves into
 // Core. If we need to do arithmetic, we probably want to use APInt.
 #include "klee/Internal/Support/IntEvaluation.h"
 
 #include "klee/util/ExprPPrinter.h"
 
+#include <iostream>
 #include <sstream>
 
 using namespace klee;
@@ -291,8 +291,8 @@ void Expr::print(std::ostream &os) const {
 }
 
 void Expr::dump() const {
-  this->print(*llvm::cerr.stream());
-  llvm::cerr << std::endl;
+  this->print(std::cerr);
+  std::cerr << std::endl;
 }
 
 /***/
diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp
index d8809a53..84e2c185 100644
--- a/lib/Expr/Lexer.cpp
+++ b/lib/Expr/Lexer.cpp
@@ -10,7 +10,7 @@
 #include "expr/Lexer.h"
 
 #include "llvm/Support/MemoryBuffer.h"
-#include "llvm/Support/Streams.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include <iomanip>
 #include <iostream>
@@ -53,9 +53,9 @@ const char *Token::getKindName() const {
 }
 
 void Token::dump() {
-  llvm::cerr << "(Token \"" << getKindName() << "\" "
-             << (void*) start << " " << length << " "
-             << line << " " << column << ")";
+  llvm::errs() << "(Token \"" << getKindName() << "\" "
+               << (void*) start << " " << length << " "
+               << line << " " << column << ")";
 }
 
 ///
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 11fb8546..88729c09 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -18,7 +18,7 @@
 
 #include "llvm/ADT/APInt.h"
 #include "llvm/Support/MemoryBuffer.h"
-#include "llvm/Support/Streams.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include <cassert>
 #include <iostream>
@@ -1523,9 +1523,9 @@ void ParserImpl::Error(const char *Message, const Token &At) {
   if (MaxErrors && NumErrors >= MaxErrors)
     return;
 
-  llvm::cerr << Filename 
-             << ":" << At.line << ":" << At.column 
-             << ": error: " << Message << "\n";
+  std::cerr << Filename
+            << ":" << At.line << ":" << At.column 
+            << ": error: " << Message << "\n";
 
   // Skip carat diagnostics on EOF token.
   if (At.kind == Token::EndOfFile)
@@ -1545,18 +1545,18 @@ void ParserImpl::Error(const char *Message, const Token &At) {
     ++LineEnd;
 
   // Show the line.
-  llvm::cerr << std::string(LineBegin, LineEnd) << "\n";
+  std::cerr << std::string(LineBegin, LineEnd) << "\n";
 
   // Show the caret or squiggly, making sure to print back spaces the
   // same.
   for (const char *S=LineBegin; S != At.start; ++S)
-    llvm::cerr << (isspace(*S) ? *S : ' ');
+    std::cerr << (isspace(*S) ? *S : ' ');
   if (At.length > 1) {
     for (unsigned i=0; i<At.length; ++i)
-      llvm::cerr << '~';
+      std::cerr << '~';
   } else
-    llvm::cerr << '^';
-  llvm::cerr << '\n';
+    std::cerr << '^';
+  std::cerr << '\n';
 }
 
 // AST API
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index 82874406..7573f51c 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -18,12 +18,10 @@
 #include "llvm/Support/CFG.h"
 #include "llvm/Support/InstIterator.h"
 #include "llvm/Support/raw_ostream.h"
+#include "llvm/Support/raw_os_ostream.h"
 #include "llvm/Analysis/ValueTracking.h"
 
 #include <map>
-#include <iostream>
-#include <fstream>
-#include <sstream>
 #include <string>
 
 using namespace llvm;
@@ -39,9 +37,10 @@ public:
 static void buildInstructionToLineMap(Module *m,
                                       std::map<const Instruction*, unsigned> &out) {  
   InstructionToLineAnnotator a;
-  std::ostringstream buffer;
-  m->print(buffer, &a);
-  std::string str = buffer.str();
+  std::string str;
+  llvm::raw_string_ostream os(str);
+  m->print(os, &a);
+  os.flush();
   const char *s;
 
   unsigned line = 1;
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 37e869c8..55eb4b8a 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -27,6 +27,7 @@
 #include "llvm/ValueSymbolTable.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
+#include "llvm/Support/raw_os_ostream.h"
 #include "llvm/System/Path.h"
 #include "llvm/Target/TargetData.h"
 #include "llvm/Transforms/Scalar.h"
@@ -326,42 +327,47 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
     std::ostream *os = ih->openOutputFile("assembly.ll");
     assert(os && os->good() && "unable to open source output");
 
+    llvm::raw_os_ostream *ros = new llvm::raw_os_ostream(*os);
+
     // We have an option for this in case the user wants a .ll they
     // can compile.
     if (NoTruncateSourceLines) {
-      *os << *module;
+      *ros << *module;
     } else {
       bool truncated = false;
-      std::stringstream buffer;
-      buffer << *module;
-      std::string string = buffer.str();
+      std::string string;
+      llvm::raw_string_ostream rss(string);
+      rss << *module;
+      rss.flush();
       const char *position = string.c_str();
 
       for (;;) {
         const char *end = index(position, '\n');
         if (!end) {
-          *os << position;
+          *ros << position;
           break;
         } else {
           unsigned count = (end - position) + 1;
           if (count<255) {
-            os->write(position, count);
+            ros->write(position, count);
           } else {
-            os->write(position, 254);
-            *os << "\n";
+            ros->write(position, 254);
+            *ros << "\n";
             truncated = true;
           }
           position = end+1;
         }
       }
     }
-
+    delete ros;
     delete os;
   }
 
   if (OutputModule) {
     std::ostream *f = ih->openOutputFile("final.bc");
-    WriteBitcodeToFile(module, *f);
+    llvm::raw_os_ostream* rfs = new llvm::raw_os_ostream(*f);
+    WriteBitcodeToFile(module, *rfs);
+    delete rfs;
     delete f;
   }
 
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index dae6ffc5..adfc5cfd 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -19,6 +19,7 @@
 #include "llvm/Support/InstIterator.h"
 #include "llvm/Support/raw_ostream.h"
 #include "llvm/Analysis/ValueTracking.h"
+#include "llvm/System/Path.h"
 
 #include <map>
 #include <iostream>
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index b7a7f4fc..08a9ef7c 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -443,7 +443,7 @@ public:
 
   void propogatePossibleValues(ref<Expr> e, CexValueData range) {
     #ifdef DEBUG
-    llvm::cerr << "propogate: " << range << " for\n" << e << "\n";
+    std::cerr << "propogate: " << range << " for\n" << e << "\n";
     #endif
 
     switch (e->getKind()) {
@@ -938,27 +938,27 @@ public:
   }
 
   void dump() {
-    llvm::cerr << "-- propogated values --\n";
+    std::cerr << "-- 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;
     
-      llvm::cerr << A->name << "\n";
-      llvm::cerr << "possible: [";
+      std::cerr << A->name << "\n";
+      std::cerr << "possible: [";
       for (unsigned i = 0; i < A->size; ++i) {
         if (i)
-          llvm::cerr << ", ";
-        llvm::cerr << COD->getPossibleValues(i);
+          std::cerr << ", ";
+        std::cerr << COD->getPossibleValues(i);
       }
-      llvm::cerr << "]\n";
-      llvm::cerr << "exact   : [";
+      std::cerr << "]\n";
+      std::cerr << "exact   : [";
       for (unsigned i = 0; i < A->size; ++i) {
         if (i)
-          llvm::cerr << ", ";
-        llvm::cerr << COD->getExactValues(i);
+          std::cerr << ", ";
+        std::cerr << COD->getExactValues(i);
       }
-      llvm::cerr << "]\n";
+      std::cerr << "]\n";
     }
   }
 };
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 3e19dbc6..090d027a 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -15,10 +15,10 @@
 
 #include "klee/util/ExprUtil.h"
 
-#include "llvm/Support/Streams.h"
-
 #include <map>
 #include <vector>
+#include <ostream>
+#include <iostream>
 
 using namespace klee;
 using namespace llvm;
@@ -249,17 +249,17 @@ IndependentElementSet getIndependentConstraints(const Query& query,
 
   if (0) {
     std::set< ref<Expr> > reqset(result.begin(), result.end());
-    llvm::cerr << "--\n";
-    llvm::cerr << "Q: " << query.expr << "\n";
-    llvm::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n";
+    std::cerr << "--\n";
+    std::cerr << "Q: " << query.expr << "\n";
+    std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n";
     int i = 0;
   for (ConstraintManager::const_iterator it = query.constraints.begin(), 
          ie = query.constraints.end(); it != ie; ++it) {
-      llvm::cerr << "C" << i++ << ": " << *it;
-      llvm::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
-      llvm::cerr << "\telts: " << IndependentElementSet(*it) << "\n";
+      std::cerr << "C" << i++ << ": " << *it;
+      std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
+      std::cerr << "\telts: " << IndependentElementSet(*it) << "\n";
     }
-    llvm::cerr << "elts closure: " << eltsClosure << "\n";
+    std::cerr << "elts closure: " << eltsClosure << "\n";
   }
 
   return eltsClosure;
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 07de2784..c489612f 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -1,3 +1,5 @@
+#include <iostream>
+
 #include "expr/Lexer.h"
 #include "expr/Parser.h"
 
@@ -99,7 +101,7 @@ static void PrintInputTokens(const MemoryBuffer *MB) {
   Token T;
   do {
     L.Lex(T);
-    llvm::cout << "(Token \"" << T.getKindName() << "\" "
+    std::cout << "(Token \"" << T.getKindName() << "\" "
                << "\"" << escapedString(T.start, T.length) << "\" "
                << T.length << " "
                << T.line << " " << T.column << ")\n";
@@ -117,7 +119,7 @@ static bool PrintInputAST(const char *Filename,
   while (Decl *D = P->ParseTopLevelDecl()) {
     if (!P->GetNumErrors()) {
       if (isa<QueryCommand>(D))
-        llvm::cout << "# Query " << ++NumQueries << "\n";
+        std::cout << "# Query " << ++NumQueries << "\n";
 
       D->dump();
     }
@@ -126,7 +128,7 @@ static bool PrintInputAST(const char *Filename,
 
   bool success = true;
   if (unsigned N = P->GetNumErrors()) {
-    llvm::cerr << Filename << ": parse failure: "
+    std::cerr << Filename << ": parse failure: "
                << N << " errors.\n";
     success = false;
   }
@@ -152,7 +154,7 @@ static bool EvaluateInputAST(const char *Filename,
 
   bool success = true;
   if (unsigned N = P->GetNumErrors()) {
-    llvm::cerr << Filename << ": parse failure: "
+    std::cerr << Filename << ": parse failure: "
                << N << " errors.\n";
     success = false;
   }  
@@ -178,16 +180,16 @@ static bool EvaluateInputAST(const char *Filename,
          ie = Decls.end(); it != ie; ++it) {
     Decl *D = *it;
     if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
-      llvm::cout << "Query " << Index << ":\t";
+      std::cout << "Query " << Index << ":\t";
 
       assert("FIXME: Support counterexample query commands!");
       if (QC->Values.empty() && QC->Objects.empty()) {
         bool result;
         if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
                           result)) {
-          llvm::cout << (result ? "VALID" : "INVALID");
+          std::cout << (result ? "VALID" : "INVALID");
         } else {
-          llvm::cout << "FAIL";
+          std::cout << "FAIL";
         }
       } else if (!QC->Values.empty()) {
         assert(QC->Objects.empty() && 
@@ -200,10 +202,10 @@ static bool EvaluateInputAST(const char *Filename,
         if (S->getValue(Query(ConstraintManager(QC->Constraints), 
                               QC->Values[0]),
                         result)) {
-          llvm::cout << "INVALID\n";
-          llvm::cout << "\tExpr 0:\t" << result;
+          std::cout << "INVALID\n";
+          std::cout << "\tExpr 0:\t" << result;
         } else {
-          llvm::cout << "FAIL";
+          std::cout << "FAIL";
         }
       } else {
         std::vector< std::vector<unsigned char> > result;
@@ -211,27 +213,27 @@ static bool EvaluateInputAST(const char *Filename,
         if (S->getInitialValues(Query(ConstraintManager(QC->Constraints), 
                                       QC->Query),
                                 QC->Objects, result)) {
-          llvm::cout << "INVALID\n";
+          std::cout << "INVALID\n";
 
           for (unsigned i = 0, e = result.size(); i != e; ++i) {
-            llvm::cout << "\tArray " << i << ":\t"
+            std::cout << "\tArray " << i << ":\t"
                        << QC->Objects[i]->name
                        << "[";
             for (unsigned j = 0; j != QC->Objects[i]->size; ++j) {
-              llvm::cout << (unsigned) result[i][j];
+              std::cout << (unsigned) result[i][j];
               if (j + 1 != QC->Objects[i]->size)
-                llvm::cout << ", ";
+                std::cout << ", ";
             }
-            llvm::cout << "]";
+            std::cout << "]";
             if (i + 1 != e)
-              llvm::cout << "\n";
+              std::cout << "\n";
           }
         } else {
-          llvm::cout << "FAIL";
+          std::cout << "FAIL";
         }
       }
 
-      llvm::cout << "\n";
+      std::cout << "\n";
       ++Index;
     }
   }
@@ -244,7 +246,7 @@ static bool EvaluateInputAST(const char *Filename,
   delete S;
 
   if (uint64_t queries = *theStatisticManager->getStatisticByName("Queries")) {
-    llvm::cout 
+    std::cout 
       << "--\n"
       << "total queries = " << queries << "\n"
       << "total queries constructs = " 
@@ -269,7 +271,7 @@ int main(int argc, char **argv) {
   std::string ErrorStr;
   MemoryBuffer *MB = MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), &ErrorStr);
   if (!MB) {
-    llvm::cerr << argv[0] << ": error: " << ErrorStr << "\n";
+    std::cerr << argv[0] << ": error: " << ErrorStr << "\n";
     return 1;
   }
 
@@ -302,7 +304,7 @@ int main(int argc, char **argv) {
                                MB, Builder);
     break;
   default:
-    llvm::cerr << argv[0] << ": error: Unknown program action!\n";
+    std::cerr << argv[0] << ": error: Unknown program action!\n";
   }
 
   delete Builder;
diff --git a/tools/klee/Debug.cpp b/tools/klee/Debug.cpp
index d11a79a7..3d46de03 100644
--- a/tools/klee/Debug.cpp
+++ b/tools/klee/Debug.cpp
@@ -2,11 +2,11 @@
 #include <iostream>
 
 void kdb_printExpr(klee::Expr *e) {
-  llvm::cerr << "expr: " << e << " -- ";
+  std::cerr << "expr: " << e << " -- ";
   if (e) {
-    llvm::cerr << *e;
+    std::cerr << *e;
   } else {
-    llvm::cerr << "(null)";
+    std::cerr << "(null)";
   }
-  llvm::cerr << "\n";
+  std::cerr << "\n";
 }
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index f7a8f0bf..2c418fc8 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -269,7 +269,7 @@ KleeHandler::KleeHandler(int argc, char **argv)
       }
     }    
 
-    llvm::cerr << "KLEE: output directory = \"" << dirname << "\"\n";
+    std::cerr << "KLEE: output directory = \"" << dirname << "\"\n";
 
     llvm::sys::Path klee_last(directory);
     klee_last.appendComponent("klee-last");
@@ -296,7 +296,7 @@ KleeHandler::KleeHandler(int argc, char **argv)
   strcpy(m_outputDirectory, p.c_str());
 
   if (mkdir(m_outputDirectory, 0775) < 0) {
-    llvm::cerr << "KLEE: ERROR: Unable to make output directory: \"" 
+    std::cerr << "KLEE: ERROR: Unable to make output directory: \"" 
                << m_outputDirectory 
                << "\", refusing to overwrite.\n";
     exit(1);
@@ -377,7 +377,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
                                   const char *errorMessage, 
                                   const char *errorSuffix) {
   if (errorMessage && ExitOnError) {
-    llvm::cerr << "EXITING ON ERROR:\n" << errorMessage << "\n";
+    std::cerr << "EXITING ON ERROR:\n" << errorMessage << "\n";
     exit(1);
   }
 
@@ -517,13 +517,13 @@ void KleeHandler::getOutFiles(std::string path,
   std::set<llvm::sys::Path> contents;
   std::string error;
   if (p.getDirectoryContents(contents, &error)) {
-    llvm::cerr << "ERROR: unable to read output directory: " << path 
+    std::cerr << "ERROR: unable to read output directory: " << path 
                << ": " << error << "\n";
     exit(1);
   }
   for (std::set<llvm::sys::Path>::iterator it = contents.begin(),
          ie = contents.end(); it != ie; ++it) {
-    std::string f = it->toString();
+    std::string f = it->str();
     if (f.substr(f.size()-6,f.size()) == ".ktest") {
       results.push_back(f);
     }
@@ -602,7 +602,7 @@ static int initEnv(Module *mainModule) {
   Function *mainFn = mainModule->getFunction("main");
     
   if (mainFn->arg_size() < 2) {
-    llvm::cerr << "Cannot handle ""-init-env"" when main() has less than two arguments.\n";
+    std::cerr << "Cannot handle ""-init-env"" when main() has less than two arguments.\n";
     return -1;
   }
 
@@ -876,11 +876,11 @@ void stop_forking() {
 
 static void interrupt_handle() {
   if (!interrupted && theInterpreter) {
-    llvm::cerr << "KLEE: ctrl-c detected, requesting interpreter to halt.\n";
+    std::cerr << "KLEE: ctrl-c detected, requesting interpreter to halt.\n";
     halt_execution();
     sys::SetInterruptFunction(interrupt_handle);
   } else {
-    llvm::cerr << "KLEE: ctrl-c detected, exiting.\n";
+    std::cerr << "KLEE: ctrl-c detected, exiting.\n";
     exit(1);
   }
   interrupted = true;
@@ -1200,7 +1200,7 @@ int main(int argc, char **argv, char **envp) {
   // locale and other data and then calls main.
   Function *mainFn = mainModule->getFunction("main");
   if (!mainFn) {
-    llvm::cerr << "'main' function not found in module.\n";
+    std::cerr << "'main' function not found in module.\n";
     return -1;
   }
 
@@ -1294,7 +1294,7 @@ int main(int argc, char **argv, char **envp) {
       if (out) {
         kTests.push_back(out);
       } else {
-        llvm::cerr << "KLEE: unable to open: " << *it << "\n";
+        std::cerr << "KLEE: unable to open: " << *it << "\n";
       }
     }
 
@@ -1311,7 +1311,7 @@ int main(int argc, char **argv, char **envp) {
          it != ie; ++it) {
       KTest *out = *it;
       interpreter->setReplayOut(out);
-      llvm::cerr << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) << " bytes)"
+      std::cerr << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) << " bytes)"
                  << " (" << ++i << "/" << outFiles.size() << ")\n";
       // XXX should put envp in .ktest ?
       interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
@@ -1329,7 +1329,7 @@ int main(int argc, char **argv, char **envp) {
          it != ie; ++it) {
       KTest *out = kTest_fromFile(it->c_str());
       if (!out) {
-        llvm::cerr << "KLEE: unable to open: " << *it << "\n";
+        std::cerr << "KLEE: unable to open: " << *it << "\n";
         exit(1);
       }
       seeds.push_back(out);
@@ -1344,19 +1344,19 @@ int main(int argc, char **argv, char **envp) {
            it2 != ie; ++it2) {
         KTest *out = kTest_fromFile(it2->c_str());
         if (!out) {
-          llvm::cerr << "KLEE: unable to open: " << *it2 << "\n";
+          std::cerr << "KLEE: unable to open: " << *it2 << "\n";
           exit(1);
         }
         seeds.push_back(out);
       }
       if (outFiles.empty()) {
-        llvm::cerr << "KLEE: seeds directory is empty: " << *it << "\n";
+        std::cerr << "KLEE: seeds directory is empty: " << *it << "\n";
         exit(1);
       }
     }
        
     if (!seeds.empty()) {
-      llvm::cerr << "KLEE: using " << seeds.size() << " seeds\n";
+      std::cerr << "KLEE: using " << seeds.size() << " seeds\n";
       interpreter->useSeeds(&seeds);
     }
     if (RunInDir != "") {
@@ -1421,12 +1421,12 @@ int main(int argc, char **argv, char **envp) {
   std::stringstream stats;
   stats << "\n";
   stats << "KLEE: done: total instructions = " 
-             << instructions << "\n";
+        << instructions << "\n";
   stats << "KLEE: done: completed paths = " 
-             << handler->getNumPathsExplored() << "\n";
+        << handler->getNumPathsExplored() << "\n";
   stats << "KLEE: done: generated tests = " 
-             << handler->getNumTestCases() << "\n";
-  llvm::cerr << stats.str();
+        << handler->getNumTestCases() << "\n";
+  std::cerr << stats.str();
   handler->getInfoStream() << stats.str();
 
   delete handler;
diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp
index 4b56f472..18284f03 100644
--- a/unittests/Expr/ExprTest.cpp
+++ b/unittests/Expr/ExprTest.cpp
@@ -7,6 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include <iostream>
 #include "gtest/gtest.h"
 
 #include "klee/Expr.h"
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index cda0cf96..3c9bf89a 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -7,6 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include <iostream>
 #include "gtest/gtest.h"
 
 #include "klee/Constraints.h"
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 08:48:17 +0000