From d934d983692c8952cdb887cbcd59f2df0001b9c0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:15:59 +0200 Subject: Refactoring from std::ostream to llvm::raw_ostream According to LLVM: lightweight and simpler implementation of streams. --- lib/Expr/ExprSMTLIBPrinter.cpp | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) (limited to 'lib/Expr/ExprSMTLIBPrinter.cpp') 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 &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 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 &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 &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: -- cgit 1.4.1 From 3b35ffed89405e7ba3059664dfbdc165b5d8625d Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:21:33 +0200 Subject: Remove #include to avoid static constructors iostream injects static constructor function into every compilation unit. Remove this to avoid it. --- include/klee/Internal/ADT/TreeStream.h | 1 - lib/Core/ExecutorUtil.cpp | 1 - lib/Core/ExternalDispatcher.cpp | 1 - lib/Core/ImpliedValue.cpp | 1 - lib/Core/Memory.cpp | 1 - lib/Core/PTree.cpp | 1 - lib/Core/PTree.h | 4 ---- lib/Core/Searcher.h | 4 +--- lib/Core/SpecialFunctionHandler.cpp | 5 +++-- lib/Core/StatsTracker.cpp | 2 -- lib/Core/StatsTracker.h | 1 - lib/Expr/Constraints.cpp | 1 - lib/Expr/Expr.cpp | 1 - lib/Expr/ExprPPrinter.cpp | 3 --- lib/Expr/ExprSMTLIBLetPrinter.cpp | 2 +- lib/Expr/ExprSMTLIBPrinter.cpp | 2 -- lib/Expr/Lexer.cpp | 1 - lib/Expr/Parser.cpp | 1 - lib/Module/Checks.cpp | 1 - lib/Module/ModuleUtil.cpp | 2 -- lib/Module/Optimize.cpp | 1 - lib/SMT/SMTParser.cpp | 1 - lib/SMT/SMTParser.h | 2 -- lib/SMT/main.cpp | 1 - lib/Solver/FastCexSolver.cpp | 1 - lib/Solver/IndependentSolver.cpp | 1 - lib/Solver/STPBuilder.cpp | 1 - lib/Solver/Solver.cpp | 1 - lib/Support/TreeStream.cpp | 1 - tools/kleaver/main.cpp | 2 -- tools/klee/Debug.cpp | 1 - tools/klee/main.cpp | 1 - 32 files changed, 5 insertions(+), 45 deletions(-) (limited to 'lib/Expr/ExprSMTLIBPrinter.cpp') diff --git a/include/klee/Internal/ADT/TreeStream.h b/include/klee/Internal/ADT/TreeStream.h index 63e49dbb..1494aa76 100644 --- a/include/klee/Internal/ADT/TreeStream.h +++ b/include/klee/Internal/ADT/TreeStream.h @@ -11,7 +11,6 @@ #define __UTIL_TREESTREAM_H__ #include -#include #include namespace klee { diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 79d1707e..f6b3dd5e 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -41,7 +41,6 @@ #include "llvm/Support/CallSite.h" -#include #include using namespace klee; diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index bbe1c42e..4c1e2b86 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -42,7 +42,6 @@ #endif #include #include -#include using namespace llvm; using namespace klee; diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index f20259fb..c8342df1 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -18,7 +18,6 @@ #include "klee/util/ExprUtil.h" -#include #include #include diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 7f5d024e..b6f225d1 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -32,7 +32,6 @@ #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -#include #include #include diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index a435cd5e..f0e7ab51 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -13,7 +13,6 @@ #include #include -#include using namespace klee; diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index 2ac688bd..11d3f48c 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -12,10 +12,6 @@ #include -#include -#include -#include - namespace klee { class ExecutionState; diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 3c077636..d866f521 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -10,14 +10,12 @@ #ifndef KLEE_SEARCHER_H #define KLEE_SEARCHER_H +#include "llvm/Support/raw_ostream.h" #include #include #include #include -// FIXME: Move out of header, use llvm streams. -#include - namespace llvm { class BasicBlock; class Function; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index dcba5436..a7a1b32e 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -27,6 +27,7 @@ #include "llvm/Module.h" #endif #include "llvm/ADT/Twine.h" +#include "llvm/Support/Debug.h" #include @@ -279,8 +280,8 @@ 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]); - DEBUG_WITH_TYPE("alias_handling", errs() << "Replacing " << old_fn - << "() with " << new_fn << "()\n";); + DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn + << "() with " << new_fn << "()\n"); if (old_fn == new_fn) state.removeFnAlias(old_fn); else state.addFnAlias(old_fn, new_fn); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 4f4552e7..0946d2ba 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -46,12 +46,10 @@ #endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/CFG.h" -#include "llvm/Support/raw_os_ostream.h" #include "llvm/Support/Process.h" #include "llvm/Support/Path.h" #include "llvm/Support/FileSystem.h" -#include #include #include diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index f06decdc..629a723d 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -12,7 +12,6 @@ #include "CallPathManager.h" -#include #include namespace llvm { 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 #include using namespace klee; diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 14737e8c..d54b8f4d 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -21,7 +21,6 @@ #include "klee/util/ExprPPrinter.h" -#include #include using namespace klee; diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index a7ad5ddc..ddcc57a1 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -17,9 +17,6 @@ #include #include -#include -#include -#include using namespace klee; diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp index 2ea5c4e0..bcdaab32 100644 --- a/lib/Expr/ExprSMTLIBLetPrinter.cpp +++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp @@ -8,7 +8,7 @@ // //===----------------------------------------------------------------------===// -#include +#include "llvm/Support/raw_ostream.h" #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBLetPrinter.h" diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index 2dbf3634..1cdab762 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -7,8 +7,6 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include - #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBPrinter.h" 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 -#include #include using namespace llvm; diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 6b346648..aebce666 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -22,7 +22,6 @@ #include "llvm/Support/raw_ostream.h" #include -#include #include #include diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp index 80b6b245..e1076d43 100644 --- a/lib/Module/Checks.cpp +++ b/lib/Module/Checks.cpp @@ -46,7 +46,6 @@ #include "llvm/Transforms/Scalar.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" #include "llvm/Support/CallSite.h" -#include using namespace llvm; using namespace klee; diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 4f65d0e7..d00cf574 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -28,7 +28,6 @@ #include "llvm/Object/ObjectFile.h" #include "llvm/Object/Error.h" #include "llvm/Support/FileSystem.h" -#include "llvm/Support/raw_os_ostream.h" #include "llvm/IR/ValueSymbolTable.h" #include "llvm/Support/SourceMgr.h" #include "llvm/Support/DataStream.h" @@ -51,7 +50,6 @@ #include #include -#include #include #include #include diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 6f060edd..ed1e0e34 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -40,7 +40,6 @@ #include "llvm/Transforms/Scalar.h" #include "llvm/Support/PassNameParser.h" #include "llvm/Support/PluginLoader.h" -#include using namespace llvm; #if 0 diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index d16e1edb..5622f048 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -14,7 +14,6 @@ #include "klee/Constraints.h" #include "expr/Parser.h" -#include #include #include #include diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index fd1ec044..ac84e74c 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -13,8 +13,6 @@ #include "expr/Parser.h" -#include -#include #include #include #include diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp index 034c4ce4..6b66e279 100644 --- a/lib/SMT/main.cpp +++ b/lib/SMT/main.cpp @@ -2,7 +2,6 @@ #include "klee/ExprBuilder.h" -#include using namespace std; using namespace klee; diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index a488db2a..5c0cf8d0 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -19,7 +19,6 @@ #include "klee/Internal/Support/IntEvaluation.h" #include "llvm/Support/raw_ostream.h" -#include #include #include #include diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 3c0b9b26..2cb4b2c6 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -19,7 +19,6 @@ #include #include #include -#include using namespace klee; using namespace llvm; diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index e4a21f74..34ce0ede 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -34,7 +34,6 @@ #include // max, min #include -#include #include #include #include diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 025c70f2..229fa234 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -771,7 +771,6 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, } } } -#include bool STPSolverImpl::computeInitialValues(const Query &query, const std::vector diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp index e95fc582..0d5e4568 100644 --- a/lib/Support/TreeStream.cpp +++ b/lib/Support/TreeStream.cpp @@ -10,7 +10,6 @@ #include "klee/Internal/ADT/TreeStream.h" #include -#include #include #include #include diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index e31140e8..b19e2ea6 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -1,5 +1,3 @@ -#include - #include "expr/Lexer.h" #include "expr/Parser.h" diff --git a/tools/klee/Debug.cpp b/tools/klee/Debug.cpp index ad264045..fbabed9d 100644 --- a/tools/klee/Debug.cpp +++ b/tools/klee/Debug.cpp @@ -1,5 +1,4 @@ #include -#include void kdb_printExpr(klee::Expr *e) { llvm::errs() << "expr: " << e << " -- "; diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 6abb1569..0292376c 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -62,7 +62,6 @@ #include #include #include -#include #include #include -- cgit 1.4.1 From 4290d38b1a8dbc5576c206a7d4f2db14d16362ca Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:22:43 +0200 Subject: Avoid non-explicit use of functions from std namespace in KLEE --- lib/Expr/ExprSMTLIBLetPrinter.cpp | 11 +++++------ lib/Expr/ExprSMTLIBPrinter.cpp | 9 ++++----- lib/SMT/SMTParser.cpp | 1 - lib/SMT/main.cpp | 2 -- 4 files changed, 9 insertions(+), 14 deletions(-) (limited to 'lib/Expr/ExprSMTLIBPrinter.cpp') 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 useLetExpressions("smtlib-use-let-expressions", @@ -85,7 +83,7 @@ void ExprSMTLIBLetPrinter::scan(const ref &e) { void ExprSMTLIBLetPrinter::generateBindings() { // Assign a number to each binding that will be used unsigned int counter = 0; - for (set >::const_iterator i = twoOrMoreEO.begin(); + for (std::set >::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 &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) { - map, unsigned int>::const_iterator i = bindings.find(e); + std::map, 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, unsigned int>::const_iterator i = + for (std::map, 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 >::const_iterator constraint = query->constraints.begin(); + std::vector >::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 @@ -495,7 +493,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { /*loop over elements in the array and generate an assert statement for each one */ - for (vector >::const_iterator + for (std::vector >::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_iterator it = + for (std::vector::const_iterator it = arraysToCallGetValueOn->begin(); it != arraysToCallGetValueOn->end(); it++) { theArray = *it; @@ -882,7 +880,8 @@ ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector &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_iterator i = a.begin(); i != a.end(); ++i) { + for (std::vector::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) { -- cgit 1.4.1 From d124e44cf09da646f88b61b1937efb39b98efc6d Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 29 May 2014 23:22:59 +0200 Subject: Fix header --- lib/Expr/ExprSMTLIBPrinter.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'lib/Expr/ExprSMTLIBPrinter.cpp') diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index e1a49afb..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 // -- cgit 1.4.1