diff options
| -rw-r--r-- | lib/Expr/ExprSMTLIBLetPrinter.cpp | 11 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 9 | ||||
| -rw-r--r-- | lib/SMT/SMTParser.cpp | 1 | ||||
| -rw-r--r-- | lib/SMT/main.cpp | 2 |
4 files changed, 9 insertions, 14 deletions
diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp index bcdaab32..d4243452 100644 --- a/lib/Expr/ExprSMTLIBLetPrinter.cpp +++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp @@ -12,8 +12,6 @@ #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBLetPrinter.h" -using namespace std; - namespace ExprSMTLIBOptions { llvm::cl::opt<bool> useLetExpressions("smtlib-use-let-expressions", @@ -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 1cdab762..e1a49afb 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -11,8 +11,6 @@ #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBPrinter.h" -using namespace std; - namespace ExprSMTLIBOptions { // Command line options llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode> @@ -495,7 +493,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 ("; @@ -556,7 +554,7 @@ 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; @@ -882,7 +880,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/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index 5622f048..03042fdd 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -22,7 +22,6 @@ //#define DEBUG -using namespace std; using namespace klee; using namespace klee::expr; diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp index 6b66e279..31fa311d 100644 --- a/lib/SMT/main.cpp +++ b/lib/SMT/main.cpp @@ -2,8 +2,6 @@ #include "klee/ExprBuilder.h" - -using namespace std; using namespace klee; int main(int argc, char** argv) { |