diff options
Diffstat (limited to 'lib/Expr')
-rw-r--r-- | lib/Expr/Constraints.cpp | 1 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 12 | ||||
-rw-r--r-- | lib/Expr/ExprPPrinter.cpp | 18 | ||||
-rw-r--r-- | lib/Expr/ExprSMTLIBLetPrinter.cpp | 15 | ||||
-rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 53 | ||||
-rw-r--r-- | lib/Expr/Lexer.cpp | 1 | ||||
-rw-r--r-- | lib/Expr/Parser.cpp | 27 |
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); |