about summary refs log tree commit diff homepage
path: root/lib/Expr
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr')
-rw-r--r--lib/Expr/Constraints.cpp1
-rw-r--r--lib/Expr/Expr.cpp12
-rw-r--r--lib/Expr/ExprPPrinter.cpp18
-rw-r--r--lib/Expr/ExprSMTLIBLetPrinter.cpp15
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp53
-rw-r--r--lib/Expr/Lexer.cpp1
-rw-r--r--lib/Expr/Parser.cpp27
7 files changed, 59 insertions, 68 deletions
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 90d9bcd4..ae4563f4 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -19,7 +19,6 @@
 #include "llvm/Support/CommandLine.h"
 #include "klee/Internal/Module/KModule.h"
 
-#include <iostream>
 #include <map>
 
 using namespace klee;
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 82c60205..d54b8f4d 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -14,13 +14,13 @@
 #include "llvm/ADT/Hashing.h"
 #endif
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.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;
@@ -116,7 +116,7 @@ int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
   return 0;
 }
 
-void Expr::printKind(std::ostream &os, Kind k) {
+void Expr::printKind(llvm::raw_ostream &os, Kind k) {
   switch(k) {
 #define X(C) case C: os << #C; break
     X(Constant);
@@ -286,7 +286,7 @@ ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
 }
 
 
-void Expr::printWidth(std::ostream &os, Width width) {
+void Expr::printWidth(llvm::raw_ostream &os, Width width) {
   switch(width) {
   case Expr::Bool: os << "Expr::Bool"; break;
   case Expr::Int8: os << "Expr::Int8"; break;
@@ -306,13 +306,13 @@ ref<Expr> Expr::createIsZero(ref<Expr> e) {
   return EqExpr::create(e, ConstantExpr::create(0, e->getWidth()));
 }
 
-void Expr::print(std::ostream &os) const {
+void Expr::print(llvm::raw_ostream &os) const {
   ExprPPrinter::printSingleExpr(os, const_cast<Expr*>(this));
 }
 
 void Expr::dump() const {
-  this->print(std::cerr);
-  std::cerr << std::endl;
+  this->print(errs());
+  errs() << "\n";
 }
 
 /***/
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index d58358b5..ddcc57a1 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -13,12 +13,10 @@
 #include "klee/Constraints.h"
 
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/raw_ostream.h"
 
 #include <map>
 #include <vector>
-#include <iostream>
-#include <sstream>
-#include <iomanip>
 
 using namespace klee;
 
@@ -47,7 +45,7 @@ private:
   std::map<const UpdateNode*, unsigned> updateBindings;
   std::set< ref<Expr> > couldPrint, shouldPrint;
   std::set<const UpdateNode*> couldPrintUpdates, shouldPrintUpdates;
-  std::ostream &os;
+  llvm::raw_ostream &os;
   unsigned counter;
   unsigned updateCounter;
   bool hasScan;
@@ -300,7 +298,7 @@ private:
   }
 
 public:
-  PPrinter(std::ostream &_os) : os(_os), newline("\n") {
+  PPrinter(llvm::raw_ostream &_os) : os(_os), newline("\n") {
     reset();
   }
 
@@ -426,11 +424,11 @@ public:
   }
 };
 
-ExprPPrinter *klee::ExprPPrinter::create(std::ostream &os) {
+ExprPPrinter *klee::ExprPPrinter::create(llvm::raw_ostream &os) {
   return new PPrinter(os);
 }
 
-void ExprPPrinter::printOne(std::ostream &os,
+void ExprPPrinter::printOne(llvm::raw_ostream &os,
                             const char *message, 
                             const ref<Expr> &e) {
   PPrinter p(os);
@@ -444,7 +442,7 @@ void ExprPPrinter::printOne(std::ostream &os,
   PC.breakLine();
 }
 
-void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) {
+void ExprPPrinter::printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e) {
   PPrinter p(os);
   p.scan(e);
 
@@ -454,13 +452,13 @@ void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) {
   p.print(e, PC);
 }
 
-void ExprPPrinter::printConstraints(std::ostream &os,
+void ExprPPrinter::printConstraints(llvm::raw_ostream &os,
                                     const ConstraintManager &constraints) {
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
 
-void ExprPPrinter::printQuery(std::ostream &os,
+void ExprPPrinter::printQuery(llvm::raw_ostream &os,
                               const ConstraintManager &constraints,
                               const ref<Expr> &q,
                               const ref<Expr> *evalExprsBegin,
diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp
index 6a88ab5d..d4243452 100644
--- a/lib/Expr/ExprSMTLIBLetPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp
@@ -8,12 +8,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include <iostream>
+#include "llvm/Support/raw_ostream.h"
 #include "llvm/Support/CommandLine.h"
 #include "klee/util/ExprSMTLIBLetPrinter.h"
 
-using namespace std;
-
 namespace ExprSMTLIBOptions {
 llvm::cl::opt<bool>
 useLetExpressions("smtlib-use-let-expressions",
@@ -31,7 +29,7 @@ ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter()
 
 void ExprSMTLIBLetPrinter::generateOutput() {
   if (p == NULL || query == NULL || o == NULL) {
-    std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl;
+    llvm::errs() << "Can't print SMTLIBv2. Output or query bad!\n";
     return;
   }
 
@@ -85,7 +83,7 @@ void ExprSMTLIBLetPrinter::scan(const ref<Expr> &e) {
 void ExprSMTLIBLetPrinter::generateBindings() {
   // Assign a number to each binding that will be used
   unsigned int counter = 0;
-  for (set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
+  for (std::set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
        i != twoOrMoreEO.end(); ++i) {
     bindings.insert(std::make_pair(*i, counter));
     ++counter;
@@ -94,7 +92,7 @@ void ExprSMTLIBLetPrinter::generateBindings() {
 
 void ExprSMTLIBLetPrinter::printExpression(
     const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
-  map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e);
+  std::map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e);
 
   if (disablePrintedAbbreviations || i == bindings.end()) {
     /*There is no abbreviation for this expression so print it normally.
@@ -143,7 +141,7 @@ void ExprSMTLIBLetPrinter::printLetExpression() {
     p->pushIndent();
 
     // Print each binding
-    for (map<const ref<Expr>, unsigned int>::const_iterator i =
+    for (std::map<const ref<Expr>, unsigned int>::const_iterator i =
              bindings.begin();
          i != bindings.end(); ++i) {
       printSeperator();
@@ -173,7 +171,8 @@ void ExprSMTLIBLetPrinter::printLetExpression() {
   // print out Expressions with abbreviations.
   unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query
   unsigned int itemsLeft = numberOfItems;
-  vector<ref<Expr> >::const_iterator constraint = query->constraints.begin();
+  std::vector<ref<Expr> >::const_iterator constraint =
+      query->constraints.begin();
 
   /* Produce nested (and () () statements. If the constraint set
    * is empty then we will only print the "queryAssert".
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index cff5abfe..bbb82d0d 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -1,5 +1,4 @@
-//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++
-//-*-===//
+//===-- ExprSMTLIBPrinter.cpp -----------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,14 +6,10 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
-#include <iostream>
-
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/CommandLine.h"
 #include "klee/util/ExprSMTLIBPrinter.h"
 
-using namespace std;
-
 namespace ExprSMTLIBOptions {
 // Command line options
 llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode>
@@ -53,7 +48,7 @@ ExprSMTLIBPrinter::~ExprSMTLIBPrinter() {
     delete p;
 }
 
-void ExprSMTLIBPrinter::setOutput(std::ostream &output) {
+void ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output) {
   o = &output;
   if (p != NULL)
     delete p;
@@ -146,8 +141,8 @@ void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr> &e) {
     break;
 
   default:
-    std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant "
-                 "display mode" << std::endl;
+    llvm::errs() << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant "
+                    "display mode\n";
   }
 }
 
@@ -425,8 +420,8 @@ void ExprSMTLIBPrinter::scanAll() {
 
 void ExprSMTLIBPrinter::generateOutput() {
   if (p == NULL || query == NULL || o == NULL) {
-    std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. "
-                 "Output or query bad!" << std::endl;
+    llvm::errs() << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. "
+                    "Output or query bad!\n";
     return;
   }
 
@@ -451,7 +446,7 @@ void ExprSMTLIBPrinter::printSetLogic() {
     *o << "QF_AUFBV";
     break;
   }
-  *o << " )" << std::endl;
+  *o << " )\n";
 }
 
 namespace {
@@ -467,7 +462,7 @@ struct ArrayPtrsByName {
 void ExprSMTLIBPrinter::printArrayDeclarations() {
   // Assume scan() has been called
   if (humanReadable)
-    *o << "; Array declarations" << endl;
+    *o << "; Array declarations\n";
 
   // Declare arrays in a deterministic order.
   std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end());
@@ -478,13 +473,13 @@ void ExprSMTLIBPrinter::printArrayDeclarations() {
                                             "(Array (_ BitVec "
        << (*it)->getDomain() << ") "
                                 "(_ BitVec " << (*it)->getRange() << ") ) )"
-       << endl;
+       << "\n";
   }
 
   // Set array values for constant values
   if (haveConstantArray) {
     if (humanReadable)
-      *o << "; Constant Array Definitions" << endl;
+      *o << "; Constant Array Definitions\n";
 
     const Array *array;
 
@@ -497,7 +492,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() {
         /*loop over elements in the array and generate an assert statement
           for each one
          */
-        for (vector<ref<ConstantExpr> >::const_iterator
+        for (std::vector<ref<ConstantExpr> >::const_iterator
                  ce = array->constantValues.begin();
              ce != array->constantValues.end(); ce++, byteIndex++) {
           *p << "(assert (";
@@ -527,7 +522,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() {
 
 void ExprSMTLIBPrinter::printConstraints() {
   if (humanReadable)
-    *o << "; Constraints" << endl;
+    *o << "; Constraints\n";
 
   // Generate assert statements for each constraint
   for (ConstraintManager::const_iterator i = query->constraints.begin();
@@ -548,7 +543,7 @@ void ExprSMTLIBPrinter::printConstraints() {
 
 void ExprSMTLIBPrinter::printAction() {
   // Ask solver to check for satisfiability
-  *o << "(check-sat)" << endl;
+  *o << "(check-sat)\n";
 
   /* If we has arrays to find the values of then we'll
    * ask the solver for the value of each bitvector in each array
@@ -558,14 +553,14 @@ void ExprSMTLIBPrinter::printAction() {
     const Array *theArray = 0;
 
     // loop over the array names
-    for (vector<const Array *>::const_iterator it =
+    for (std::vector<const Array *>::const_iterator it =
              arraysToCallGetValueOn->begin();
          it != arraysToCallGetValueOn->end(); it++) {
       theArray = *it;
       // Loop over the array indices
       for (unsigned int index = 0; index < theArray->size; ++index) {
         *o << "(get-value ( (select " << (**it).name << " (_ bv" << index << " "
-           << theArray->getDomain() << ") ) ) )" << endl;
+           << theArray->getDomain() << ") ) ) )\n";
       }
     }
   }
@@ -573,8 +568,8 @@ void ExprSMTLIBPrinter::printAction() {
 
 void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
   if (e.isNull()) {
-    std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!"
-              << std::endl;
+    llvm::errs() << "ExprSMTLIBPrinter::scan() : Found NULL expression!"
+                 << "\n";
     return;
   }
 
@@ -609,7 +604,7 @@ void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) {
   }
 }
 
-void ExprSMTLIBPrinter::printExit() { *o << "(exit)" << endl; }
+void ExprSMTLIBPrinter::printExit() { *o << "(exit)\n"; }
 
 bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l) {
   if (l > QF_AUFBV)
@@ -627,7 +622,7 @@ void ExprSMTLIBPrinter::printSeperator() {
 }
 
 void ExprSMTLIBPrinter::printNotice() {
-  *o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl;
+  *o << "; This file conforms to SMTLIBv2 and was generated by KLEE\n";
 }
 
 void ExprSMTLIBPrinter::setHumanReadable(bool hr) { humanReadable = hr; }
@@ -638,7 +633,7 @@ void ExprSMTLIBPrinter::printOptions() {
            smtlibBoolOptions.begin();
        i != smtlibBoolOptions.end(); i++) {
     *o << "(set-option :" << getSMTLIBOptionString(i->first) << " "
-       << ((i->second) ? "true" : "false") << ")" << endl;
+       << ((i->second) ? "true" : "false") << ")\n";
   }
 }
 
@@ -742,8 +737,9 @@ void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e,
     *p << ")";
 
     if (bitWidth != Expr::Bool)
-      std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length "
-                << bitWidth << ") to bool!" << std::endl;
+      llvm::errs()
+          << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length "
+          << bitWidth << ") to bool!\n";
 
   } break;
   default:
@@ -883,7 +879,8 @@ ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array *> &a) {
    * that the solver knows what to do when we ask for the values of arrays
    * that don't feature in our query!
    */
-  for (vector<const Array *>::const_iterator i = a.begin(); i != a.end(); ++i) {
+  for (std::vector<const Array *>::const_iterator i = a.begin(); i != a.end();
+       ++i) {
     usedArrays.insert(*i);
   }
 }
diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp
index 9859ff36..e250a968 100644
--- a/lib/Expr/Lexer.cpp
+++ b/lib/Expr/Lexer.cpp
@@ -13,7 +13,6 @@
 #include "llvm/Support/raw_ostream.h"
 
 #include <iomanip>
-#include <iostream>
 #include <string.h>
 
 using namespace llvm;
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 5b3e96b7..aebce666 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -22,7 +22,6 @@
 #include "llvm/Support/raw_ostream.h"
 
 #include <cassert>
-#include <iostream>
 #include <map>
 #include <cstring>
 
@@ -1522,7 +1521,7 @@ void ParserImpl::Error(const char *Message, const Token &At) {
   if (MaxErrors && NumErrors >= MaxErrors)
     return;
 
-  std::cerr << Filename
+  llvm::errs() << Filename
             << ":" << At.line << ":" << At.column 
             << ": error: " << Message << "\n";
 
@@ -1544,18 +1543,18 @@ void ParserImpl::Error(const char *Message, const Token &At) {
     ++LineEnd;
 
   // Show the line.
-  std::cerr << std::string(LineBegin, LineEnd) << "\n";
+  llvm::errs() << 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)
-    std::cerr << (isspace(*S) ? *S : ' ');
+    llvm::errs() << (isspace(*S) ? *S : ' ');
   if (At.length > 1) {
     for (unsigned i=0; i<At.length; ++i)
-      std::cerr << '~';
+      llvm::errs() << '~';
   } else
-    std::cerr << '^';
-  std::cerr << '\n';
+    llvm::errs() << '^';
+  llvm::errs() << '\n';
 }
 
 // AST API
@@ -1564,20 +1563,20 @@ void ParserImpl::Error(const char *Message, const Token &At) {
 Decl::Decl(DeclKind _Kind) : Kind(_Kind) {}
 
 void ArrayDecl::dump() {
-  std::cout << "array " << Root->name
+  llvm::outs() << "array " << Root->name
             << "[" << Root->size << "]"
             << " : " << 'w' << Domain << " -> " << 'w' << Range << " = ";
 
   if (Root->isSymbolicArray()) {
-    std::cout << "symbolic\n";
+    llvm::outs() << "symbolic\n";
   } else {
-    std::cout << '[';
+    llvm::outs() << '[';
     for (unsigned i = 0, e = Root->size; i != e; ++i) {
       if (i)
-        std::cout << " ";
-      std::cout << Root->constantValues[i];
+        llvm::outs() << " ";
+      llvm::outs() << Root->constantValues[i];
     }
-    std::cout << "]\n";
+    llvm::outs() << "]\n";
   }
 }
 
@@ -1592,7 +1591,7 @@ void QueryCommand::dump() {
     ObjectsBegin = &Objects[0];
     ObjectsEnd = ObjectsBegin + Objects.size();
   }
-  ExprPPrinter::printQuery(std::cout, ConstraintManager(Constraints), 
+  ExprPPrinter::printQuery(llvm::outs(), ConstraintManager(Constraints),
                            Query, ValuesBegin, ValuesEnd,
                            ObjectsBegin, ObjectsEnd,
                            false);