about summary refs log tree commit diff homepage
path: root/lib/Expr/ExprSMTLIBPrinter.cpp
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2014-05-29 23:15:59 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2014-05-29 23:57:45 +0200
commitd934d983692c8952cdb887cbcd59f2df0001b9c0 (patch)
tree9179a257bb053ba0a0da0e9dc4d2c030202c0f28 /lib/Expr/ExprSMTLIBPrinter.cpp
parentc2dec441f3f89916962175f0307b5c33473fa616 (diff)
downloadklee-d934d983692c8952cdb887cbcd59f2df0001b9c0.tar.gz
Refactoring from std::ostream to llvm::raw_ostream
According to LLVM: lightweight and simpler implementation of streams.
Diffstat (limited to 'lib/Expr/ExprSMTLIBPrinter.cpp')
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp39
1 files changed, 20 insertions, 19 deletions
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index cff5abfe..2dbf3634 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -53,7 +53,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 +146,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 +425,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 +451,7 @@ void ExprSMTLIBPrinter::printSetLogic() {
     *o << "QF_AUFBV";
     break;
   }
-  *o << " )" << std::endl;
+  *o << " )\n";
 }
 
 namespace {
@@ -467,7 +467,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 +478,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;
 
@@ -527,7 +527,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 +548,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
@@ -565,7 +565,7 @@ void ExprSMTLIBPrinter::printAction() {
       // 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 +573,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 +609,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 +627,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 +638,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 +742,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: