From 400aea6b9d4d0a33f4c6cae4cada7e54029fccc4 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Tue, 1 Sep 2009 06:53:41 +0000 Subject: Update for LLVM ostream changes. - Includes patch by Michael Stone! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Core/ExecutionState.cpp | 34 +++++++++++++++++----------------- lib/Core/Executor.cpp | 13 +++++++------ lib/Core/ExecutorTimers.cpp | 2 +- lib/Core/ExecutorUtil.cpp | 5 ++--- lib/Core/ExternalDispatcher.cpp | 4 ++-- lib/Core/ImpliedValue.cpp | 6 +++--- lib/Core/Memory.cpp | 23 ++++++++++++----------- lib/Core/Searcher.cpp | 22 +++++++++++----------- lib/Core/SpecialFunctionHandler.cpp | 22 +++++++++++----------- lib/Expr/Expr.cpp | 6 +++--- lib/Expr/Lexer.cpp | 8 ++++---- lib/Expr/Parser.cpp | 18 +++++++++--------- lib/Module/InstructionInfoTable.cpp | 11 +++++------ lib/Module/KModule.cpp | 26 ++++++++++++++++---------- lib/Module/ModuleUtil.cpp | 1 + lib/Solver/FastCexSolver.cpp | 22 +++++++++++----------- lib/Solver/IndependentSolver.cpp | 18 +++++++++--------- 17 files changed, 124 insertions(+), 117 deletions(-) (limited to 'lib') diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 9eb560b8..694b21b1 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -147,7 +147,7 @@ std::ostream &klee::operator<<(std::ostream &os, const MemoryMap &mm) { bool ExecutionState::merge(const ExecutionState &b) { if (DebugLogStateMerge) - llvm::cerr << "-- attempting merge of A:" + std::cerr << "-- attempting merge of A:" << this << " with B:" << &b << "--\n"; if (pc != b.pc) return false; @@ -185,21 +185,21 @@ bool ExecutionState::merge(const ExecutionState &b) { commonConstraints.begin(), commonConstraints.end(), std::inserter(bSuffix, bSuffix.end())); if (DebugLogStateMerge) { - llvm::cerr << "\tconstraint prefix: ["; + std::cerr << "\tconstraint prefix: ["; for (std::set< ref >::iterator it = commonConstraints.begin(), ie = commonConstraints.end(); it != ie; ++it) - llvm::cerr << *it << ", "; - llvm::cerr << "]\n"; - llvm::cerr << "\tA suffix: ["; + std::cerr << *it << ", "; + std::cerr << "]\n"; + std::cerr << "\tA suffix: ["; for (std::set< ref >::iterator it = aSuffix.begin(), ie = aSuffix.end(); it != ie; ++it) - llvm::cerr << *it << ", "; - llvm::cerr << "]\n"; - llvm::cerr << "\tB suffix: ["; + std::cerr << *it << ", "; + std::cerr << "]\n"; + std::cerr << "\tB suffix: ["; for (std::set< ref >::iterator it = bSuffix.begin(), ie = bSuffix.end(); it != ie; ++it) - llvm::cerr << *it << ", "; - llvm::cerr << "]\n"; + std::cerr << *it << ", "; + std::cerr << "]\n"; } // We cannot merge if addresses would resolve differently in the @@ -212,9 +212,9 @@ bool ExecutionState::merge(const ExecutionState &b) { // and not the other if (DebugLogStateMerge) { - llvm::cerr << "\tchecking object states\n"; - llvm::cerr << "A: " << addressSpace.objects << "\n"; - llvm::cerr << "B: " << b.addressSpace.objects << "\n"; + std::cerr << "\tchecking object states\n"; + std::cerr << "A: " << addressSpace.objects << "\n"; + std::cerr << "B: " << b.addressSpace.objects << "\n"; } std::set mutated; @@ -226,22 +226,22 @@ bool ExecutionState::merge(const ExecutionState &b) { if (ai->first != bi->first) { if (DebugLogStateMerge) { if (ai->first < bi->first) { - llvm::cerr << "\t\tB misses binding for: " << ai->first->id << "\n"; + std::cerr << "\t\tB misses binding for: " << ai->first->id << "\n"; } else { - llvm::cerr << "\t\tA misses binding for: " << bi->first->id << "\n"; + std::cerr << "\t\tA misses binding for: " << bi->first->id << "\n"; } } return false; } if (ai->second != bi->second) { if (DebugLogStateMerge) - llvm::cerr << "\t\tmutated: " << ai->first->id << "\n"; + std::cerr << "\t\tmutated: " << ai->first->id << "\n"; mutated.insert(ai->first); } } if (ai!=ae || bi!=be) { if (DebugLogStateMerge) - llvm::cerr << "\t\tmappings differ\n"; + std::cerr << "\t\tmappings differ\n"; return false; } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 35238793..d865bcb5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1074,7 +1074,8 @@ void Executor::executeGetValue(ExecutionState &state, void Executor::stepInstruction(ExecutionState &state) { if (DebugPrintInstructions) { printFileLine(state, state.pc); - llvm::cerr << std::setw(10) << stats::instructions << " " << *state.pc->inst; + std::cerr << std::setw(10) << stats::instructions << " "; + llvm::errs() << *(state.pc->inst); } if (statsTracker) @@ -1273,9 +1274,9 @@ void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src, void Executor::printFileLine(ExecutionState &state, KInstruction *ki) { const InstructionInfo &ii = *ki->info; if (ii.file != "") - llvm::cerr << " " << ii.file << ":" << ii.line << ":"; + std::cerr << " " << ii.file << ":" << ii.line << ":"; else - llvm::cerr << " [no debug info]:"; + std::cerr << " [no debug info]:"; } @@ -2374,7 +2375,7 @@ void Executor::run(ExecutionState &initialState) { dump: if (DumpStatesOnHalt && !states.empty()) { - llvm::cerr << "KLEE: halting execution, dumping remaining states\n"; + std::cerr << "KLEE: halting execution, dumping remaining states\n"; for (std::set::iterator it = states.begin(), ie = states.end(); it != ie; ++it) { @@ -2558,7 +2559,7 @@ void Executor::callExternalFunction(ExecutionState &state, return; if (NoExternals && !okExternals.count(function->getName())) { - llvm::cerr << "KLEE:ERROR: Calling not-OK external function : " + std::cerr << "KLEE:ERROR: Calling not-OK external function : " << function->getNameStr() << "\n"; terminateStateOnError(state, "externals disallowed", "user.err"); return; @@ -2653,7 +2654,7 @@ ref Executor::replaceReadWithSymbolic(ExecutionState &state, Expr::getMinBytesForWidth(e->getWidth())); ref res = Expr::createTempRead(array, e->getWidth()); ref eq = NotOptimizedExpr::create(EqExpr::create(e, res)); - llvm::cerr << "Making symbolic: " << eq << "\n"; + std::cerr << "Making symbolic: " << eq << "\n"; state.addConstraint(eq); return res; } diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 0c274d5c..8934a6cd 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -47,7 +47,7 @@ public: ~HaltTimer() {} void run() { - llvm::cerr << "KLEE: HaltTimer invoked\n"; + std::cerr << "KLEE: HaltTimer invoked\n"; executor->setHaltExecution(true); } }; diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 69bb2017..32fee991 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -24,7 +24,6 @@ #include "llvm/ModuleProvider.h" #include "llvm/Support/CallSite.h" #include "llvm/Support/GetElementPtrTypeIterator.h" -#include "llvm/Support/Streams.h" #include "llvm/Target/TargetData.h" #include #include @@ -47,8 +46,8 @@ namespace klee { switch (ce->getOpcode()) { default : ce->dump(); - llvm::cerr << "error: unknown ConstantExpr type\n" - << "opcode: " << ce->getOpcode() << "\n"; + std::cerr << "error: unknown ConstantExpr type\n" + << "opcode: " << ce->getOpcode() << "\n"; abort(); case Instruction::Trunc: diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index e5b00b7f..94dad33c 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -18,11 +18,11 @@ #include "llvm/ExecutionEngine/GenericValue.h" #include "llvm/Support/CallSite.h" #include "llvm/System/DynamicLibrary.h" -#include "llvm/Support/Streams.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Target/TargetSelect.h" #include #include +#include using namespace llvm; using namespace klee; @@ -73,7 +73,7 @@ ExternalDispatcher::ExternalDispatcher() { std::string error; executionEngine = ExecutionEngine::createJIT(MP, &error); if (!executionEngine) { - llvm::cerr << "unable to make jit: " << error << "\n"; + std::cerr << "unable to make jit: " << error << "\n"; abort(); } diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index a3d30f76..56c1d1a9 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -246,9 +246,9 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref e, } else { if (it!=found.end()) { ref binding = it->second; - llvm::cerr << "checkForImpliedValues: " << e << " = " << value << "\n" - << "\t\t implies " << var << " == " << binding - << " (error)\n"; + std::cerr << "checkForImpliedValues: " << e << " = " << value << "\n" + << "\t\t implies " << var << " == " << binding + << " (error)\n"; assert(0); } } diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index aa170ceb..08c0696c 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -22,6 +22,7 @@ #include #include #include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" #include #include @@ -65,7 +66,7 @@ MemoryObject::~MemoryObject() { } void MemoryObject::getAllocInfo(std::string &result) const { - std::ostringstream info; + llvm::raw_string_ostream info(result); info << "MO" << id << "[" << size << "]"; @@ -83,7 +84,7 @@ void MemoryObject::getAllocInfo(std::string &result) const { info << " (no allocation info)"; } - result = info.str(); + info.flush(); } /***/ @@ -558,23 +559,23 @@ void ObjectState::write64(unsigned offset, uint64_t value) { } void ObjectState::print() { - llvm::cerr << "-- ObjectState --\n"; - llvm::cerr << "\tMemoryObject ID: " << object->id << "\n"; - llvm::cerr << "\tRoot Object: " << updates.root << "\n"; - llvm::cerr << "\tSize: " << size << "\n"; + std::cerr << "-- ObjectState --\n"; + std::cerr << "\tMemoryObject ID: " << object->id << "\n"; + std::cerr << "\tRoot Object: " << updates.root << "\n"; + std::cerr << "\tSize: " << size << "\n"; - llvm::cerr << "\tBytes:\n"; + std::cerr << "\tBytes:\n"; for (unsigned i=0; inext) { - llvm::cerr << "\t\t[" << un->index << "] = " << un->value << "\n"; + std::cerr << "\t\t[" << un->index << "] = " << un->value << "\n"; } } diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 4c94c59b..6fa75a26 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -374,17 +374,17 @@ ExecutionState &MergingSearcher::selectState() { } if (DebugLogMerge) - llvm::cerr << "-- all at merge --\n"; + std::cerr << "-- all at merge --\n"; for (std::map >::iterator it = merges.begin(), ie = merges.end(); it != ie; ++it) { if (DebugLogMerge) { - llvm::cerr << "\tmerge: " << it->first << " ["; + std::cerr << "\tmerge: " << it->first << " ["; for (std::vector::iterator it2 = it->second.begin(), ie2 = it->second.end(); it2 != ie2; ++it2) { ExecutionState *state = *it2; - llvm::cerr << state << ", "; + std::cerr << state << ", "; } - llvm::cerr << "]\n"; + std::cerr << "]\n"; } // merge states @@ -403,13 +403,13 @@ ExecutionState &MergingSearcher::selectState() { } } if (DebugLogMerge && !toErase.empty()) { - llvm::cerr << "\t\tmerged: " << base << " with ["; + std::cerr << "\t\tmerged: " << base << " with ["; for (std::set::iterator it = toErase.begin(), ie = toErase.end(); it != ie; ++it) { - if (it!=toErase.begin()) llvm::cerr << ", "; - llvm::cerr << *it; + if (it!=toErase.begin()) std::cerr << ", "; + std::cerr << *it; } - llvm::cerr << "]\n"; + std::cerr << "]\n"; } for (std::set::iterator it = toErase.begin(), ie = toErase.end(); it != ie; ++it) { @@ -427,7 +427,7 @@ ExecutionState &MergingSearcher::selectState() { } if (DebugLogMerge) - llvm::cerr << "-- merge complete, continuing --\n"; + std::cerr << "-- merge complete, continuing --\n"; return selectState(); } @@ -475,7 +475,7 @@ ExecutionState &BatchingSearcher::selectState() { if (lastState) { double delta = util::getWallTime()-lastStartTime; if (delta>timeBudget*1.1) { - llvm::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n"; + std::cerr << "KLEE: increased time budget from " << timeBudget << " to " << delta << "\n"; timeBudget = delta; } } @@ -541,7 +541,7 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, if (baseSearcher->empty()) { time *= 2; - llvm::cerr << "KLEE: increasing time budget to: " << time << "\n"; + std::cerr << "KLEE: increasing time budget to: " << time << "\n"; baseSearcher->update(0, pausedStates, std::set()); pausedStates.clear(); } diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 45202c19..ba86428d 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -216,7 +216,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - llvm::cerr << "TAINT: skipping abort fail\n"; + std::cerr << "TAINT: skipping abort fail\n"; executor.terminateState(state); } else { executor.terminateStateOnError(state, "abort failure", "abort.err"); @@ -244,7 +244,7 @@ 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]); - //llvm::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n"; + //std::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n"; if (old_fn == new_fn) state.removeFnAlias(old_fn); else state.addFnAlias(old_fn, new_fn); @@ -257,7 +257,7 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - llvm::cerr << "TAINT: skipping assertion:" + std::cerr << "TAINT: skipping assertion:" << readStringAtAddress(state, arguments[0]) << "\n"; executor.terminateState(state); } else @@ -273,7 +273,7 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - llvm::cerr << "TAINT: skipping assertion:" + std::cerr << "TAINT: skipping assertion:" << readStringAtAddress(state, arguments[0]) << "\n"; executor.terminateState(state); } else @@ -291,7 +291,7 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state, //XXX:DRE:TAINT if(state.underConstrained) { - llvm::cerr << "TAINT: skipping klee_report_error:" + std::cerr << "TAINT: skipping klee_report_error:" << readStringAtAddress(state, arguments[2]) << ":" << readStringAtAddress(state, arguments[3]) << "\n"; executor.terminateState(state); @@ -409,7 +409,7 @@ void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state, "invalid number of arguments to klee_print_expr"); std::string msg_str = readStringAtAddress(state, arguments[0]); - llvm::cerr << msg_str << ":" << arguments[1] << "\n"; + std::cerr << msg_str << ":" << arguments[1] << "\n"; } void SpecialFunctionHandler::handleSetForking(ExecutionState &state, @@ -456,7 +456,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, "invalid number of arguments to klee_print_range"); std::string msg_str = readStringAtAddress(state, arguments[0]); - llvm::cerr << msg_str << ":" << arguments[1]; + std::cerr << msg_str << ":" << arguments[1]; if (!isa(arguments[1])) { // FIXME: Pull into a unique value method? ref value; @@ -468,15 +468,15 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, res); assert(success && "FIXME: Unhandled solver failure"); if (res) { - llvm::cerr << " == " << value; + std::cerr << " == " << value; } else { - llvm::cerr << " ~= " << value; + std::cerr << " ~= " << value; std::pair< ref, ref > res = executor.solver->getRange(state, arguments[1]); - llvm::cerr << " (in [" << res.first << ", " << res.second <<"])"; + std::cerr << " (in [" << res.first << ", " << res.second <<"])"; } } - llvm::cerr << "\n"; + std::cerr << "\n"; } void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state, diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index b1bf9824..386d29de 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -10,13 +10,13 @@ #include "klee/Expr.h" #include "llvm/Support/CommandLine.h" -#include "llvm/Support/Streams.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 #include using namespace klee; @@ -291,8 +291,8 @@ void Expr::print(std::ostream &os) const { } void Expr::dump() const { - this->print(*llvm::cerr.stream()); - llvm::cerr << std::endl; + this->print(std::cerr); + std::cerr << std::endl; } /***/ diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp index d8809a53..84e2c185 100644 --- a/lib/Expr/Lexer.cpp +++ b/lib/Expr/Lexer.cpp @@ -10,7 +10,7 @@ #include "expr/Lexer.h" #include "llvm/Support/MemoryBuffer.h" -#include "llvm/Support/Streams.h" +#include "llvm/Support/raw_ostream.h" #include #include @@ -53,9 +53,9 @@ const char *Token::getKindName() const { } void Token::dump() { - llvm::cerr << "(Token \"" << getKindName() << "\" " - << (void*) start << " " << length << " " - << line << " " << column << ")"; + llvm::errs() << "(Token \"" << getKindName() << "\" " + << (void*) start << " " << length << " " + << line << " " << column << ")"; } /// diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 11fb8546..88729c09 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -18,7 +18,7 @@ #include "llvm/ADT/APInt.h" #include "llvm/Support/MemoryBuffer.h" -#include "llvm/Support/Streams.h" +#include "llvm/Support/raw_ostream.h" #include #include @@ -1523,9 +1523,9 @@ void ParserImpl::Error(const char *Message, const Token &At) { if (MaxErrors && NumErrors >= MaxErrors) return; - llvm::cerr << Filename - << ":" << At.line << ":" << At.column - << ": error: " << Message << "\n"; + std::cerr << Filename + << ":" << At.line << ":" << At.column + << ": error: " << Message << "\n"; // Skip carat diagnostics on EOF token. if (At.kind == Token::EndOfFile) @@ -1545,18 +1545,18 @@ void ParserImpl::Error(const char *Message, const Token &At) { ++LineEnd; // Show the line. - llvm::cerr << std::string(LineBegin, LineEnd) << "\n"; + std::cerr << 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) - llvm::cerr << (isspace(*S) ? *S : ' '); + std::cerr << (isspace(*S) ? *S : ' '); if (At.length > 1) { for (unsigned i=0; i -#include -#include -#include #include using namespace llvm; @@ -39,9 +37,10 @@ public: static void buildInstructionToLineMap(Module *m, std::map &out) { InstructionToLineAnnotator a; - std::ostringstream buffer; - m->print(buffer, &a); - std::string str = buffer.str(); + std::string str; + llvm::raw_string_ostream os(str); + m->print(os, &a); + os.flush(); const char *s; unsigned line = 1; diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 37e869c8..55eb4b8a 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -27,6 +27,7 @@ #include "llvm/ValueSymbolTable.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" +#include "llvm/Support/raw_os_ostream.h" #include "llvm/System/Path.h" #include "llvm/Target/TargetData.h" #include "llvm/Transforms/Scalar.h" @@ -326,42 +327,47 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, std::ostream *os = ih->openOutputFile("assembly.ll"); assert(os && os->good() && "unable to open source output"); + llvm::raw_os_ostream *ros = new llvm::raw_os_ostream(*os); + // We have an option for this in case the user wants a .ll they // can compile. if (NoTruncateSourceLines) { - *os << *module; + *ros << *module; } else { bool truncated = false; - std::stringstream buffer; - buffer << *module; - std::string string = buffer.str(); + std::string string; + llvm::raw_string_ostream rss(string); + rss << *module; + rss.flush(); const char *position = string.c_str(); for (;;) { const char *end = index(position, '\n'); if (!end) { - *os << position; + *ros << position; break; } else { unsigned count = (end - position) + 1; if (count<255) { - os->write(position, count); + ros->write(position, count); } else { - os->write(position, 254); - *os << "\n"; + ros->write(position, 254); + *ros << "\n"; truncated = true; } position = end+1; } } } - + delete ros; delete os; } if (OutputModule) { std::ostream *f = ih->openOutputFile("final.bc"); - WriteBitcodeToFile(module, *f); + llvm::raw_os_ostream* rfs = new llvm::raw_os_ostream(*f); + WriteBitcodeToFile(module, *rfs); + delete rfs; delete f; } diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index dae6ffc5..adfc5cfd 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -19,6 +19,7 @@ #include "llvm/Support/InstIterator.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Analysis/ValueTracking.h" +#include "llvm/System/Path.h" #include #include diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index b7a7f4fc..08a9ef7c 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -443,7 +443,7 @@ public: void propogatePossibleValues(ref e, CexValueData range) { #ifdef DEBUG - llvm::cerr << "propogate: " << range << " for\n" << e << "\n"; + std::cerr << "propogate: " << range << " for\n" << e << "\n"; #endif switch (e->getKind()) { @@ -938,27 +938,27 @@ public: } void dump() { - llvm::cerr << "-- propogated values --\n"; + std::cerr << "-- propogated values --\n"; for (std::map::iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { const Array *A = it->first; CexObjectData *COD = it->second; - llvm::cerr << A->name << "\n"; - llvm::cerr << "possible: ["; + std::cerr << A->name << "\n"; + std::cerr << "possible: ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - llvm::cerr << ", "; - llvm::cerr << COD->getPossibleValues(i); + std::cerr << ", "; + std::cerr << COD->getPossibleValues(i); } - llvm::cerr << "]\n"; - llvm::cerr << "exact : ["; + std::cerr << "]\n"; + std::cerr << "exact : ["; for (unsigned i = 0; i < A->size; ++i) { if (i) - llvm::cerr << ", "; - llvm::cerr << COD->getExactValues(i); + std::cerr << ", "; + std::cerr << COD->getExactValues(i); } - llvm::cerr << "]\n"; + std::cerr << "]\n"; } } }; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 3e19dbc6..090d027a 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -15,10 +15,10 @@ #include "klee/util/ExprUtil.h" -#include "llvm/Support/Streams.h" - #include #include +#include +#include using namespace klee; using namespace llvm; @@ -249,17 +249,17 @@ IndependentElementSet getIndependentConstraints(const Query& query, if (0) { std::set< ref > reqset(result.begin(), result.end()); - llvm::cerr << "--\n"; - llvm::cerr << "Q: " << query.expr << "\n"; - llvm::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n"; + std::cerr << "--\n"; + std::cerr << "Q: " << query.expr << "\n"; + std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n"; int i = 0; for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { - llvm::cerr << "C" << i++ << ": " << *it; - llvm::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; - llvm::cerr << "\telts: " << IndependentElementSet(*it) << "\n"; + std::cerr << "C" << i++ << ": " << *it; + std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n"; + std::cerr << "\telts: " << IndependentElementSet(*it) << "\n"; } - llvm::cerr << "elts closure: " << eltsClosure << "\n"; + std::cerr << "elts closure: " << eltsClosure << "\n"; } return eltsClosure; -- cgit 1.4.1