diff options
| -rw-r--r-- | lib/Basic/ConstructSolverChain.cpp | 17 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 12 | ||||
| -rw-r--r-- | lib/Core/Searcher.cpp | 6 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 6 | ||||
| -rw-r--r-- | lib/Solver/Z3Solver.cpp | 4 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 32 |
6 files changed, 37 insertions, 40 deletions
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 2df87d51..debb1e9e 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -12,6 +12,7 @@ */ #include "klee/Common.h" #include "klee/CommandLine.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" namespace klee { @@ -24,15 +25,15 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, if (optionIsSet(queryLoggingOptions, SOLVER_PC)) { solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath, MinQueryTimeToLog); - llvm::errs() << "Logging queries that reach solver in .pc format to " - << baseSolverQueryPCLogPath.c_str() << "\n"; + klee_message("Logging queries that reach solver in .pc format to %s\n", + baseSolverQueryPCLogPath.c_str()); } if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) { solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, MinQueryTimeToLog); - llvm::errs() << "Logging queries that reach solver in .smt2 format to " - << baseSolverQuerySMT2LogPath.c_str() << "\n"; + klee_message("Logging queries that reach solver in .smt2 format to %s\n", + baseSolverQuerySMT2LogPath.c_str()); } if (UseFastCexSolver) @@ -52,15 +53,15 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, if (optionIsSet(queryLoggingOptions, ALL_PC)) { solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog); - llvm::errs() << "Logging all queries in .pc format to " - << queryPCLogPath.c_str() << "\n"; + klee_message("Logging all queries in .pc format to %s\n", + queryPCLogPath.c_str()); } if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) { solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog); - llvm::errs() << "Logging all queries in .smt2 format to " - << querySMT2LogPath.c_str() << "\n"; + klee_message("Logging all queries in .smt2 format to %s\n", + querySMT2LogPath.c_str()); } if (DebugCrossCheckCoreSolverWith != NO_SOLVER) { Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8b885527..1df51b4d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -356,8 +356,7 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) if (coreSolverTimeout) UseForkedCoreSolver = true; Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); if (!coreSolver) { - llvm::errs() << "Failed to create core solver\n"; - exit(1); + klee_error("Failed to create core solver\n"); } Solver *solver = constructSolverChain( coreSolver, @@ -1481,9 +1480,8 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { GlobalValue *old_gv = gv; gv = currModule->getNamedValue(alias); if (!gv) { - llvm::errs() << "Function " << alias << "(), alias for " - << old_gv->getName() << " not found!\n"; - assert(0 && "function alias not found"); + klee_error("Function %s(), alias for %s not found!\n", alias.c_str(), + old_gv->getName().str().c_str()); } } @@ -3018,8 +3016,8 @@ void Executor::callExternalFunction(ExecutionState &state, return; if (NoExternals && !okExternals.count(function->getName())) { - llvm::errs() << "KLEE:ERROR: Calling not-OK external function : " - << function->getName().str() << "\n"; + klee_warning("Calling not-OK external function : %s\n", + function->getName().str().c_str()); terminateStateOnError(state, "externals disallowed", User); return; } diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 973057c3..3bfcd6b3 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -527,8 +527,8 @@ ExecutionState &BatchingSearcher::selectState() { if (lastState) { double delta = util::getWallTime()-lastStartTime; if (delta>timeBudget*1.1) { - llvm::errs() << "KLEE: increased time budget from " << timeBudget - << " to " << delta << "\n"; + klee_message("KLEE: increased time budget from %f to %f\n", timeBudget, + delta); timeBudget = delta; } } @@ -601,7 +601,7 @@ void IterativeDeepeningTimeSearcher::update( if (baseSearcher->empty()) { time *= 2; - llvm::errs() << "KLEE: increasing time budget to: " << time << "\n"; + klee_message("KLEE: increased time budget to %f\n", time); std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end()); baseSearcher->update(0, ps, std::vector<ExecutionState *>()); pausedStates.clear(); diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 411c07b1..6bfd79c1 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -397,9 +397,9 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( // "occasion" return a status when the process was terminated by a // signal, so test signal first. if (WIFSIGNALED(status) || !WIFEXITED(status)) { - fprintf(stderr, - "error: metaSMT did not return successfully (status = %d) \n", - WTERMSIG(status)); + klee_warning( + "error: metaSMT did not return successfully (status = %d) \n", + WTERMSIG(status)); return (SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED); } diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 96a7dafa..1cbca566 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// #include "klee/Config/config.h" +#include "klee/Internal/Support/ErrorHandling.h" #ifdef ENABLE_Z3 #include "Z3Builder.h" #include "klee/Constraints.h" @@ -285,8 +286,7 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( if (strcmp(reason, "unknown") == 0) { return SolverImpl::SOLVER_RUN_STATUS_FAILURE; } - llvm::errs() << "Unexpected solver failure. Reason is \"" << reason - << "\"\n"; + klee_warning("Unexpected solver failure. Reason is \"%s,\"\n", reason); abort(); } default: diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 1eab170f..e198697c 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -393,7 +393,7 @@ llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string &filename) { f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::raw_fd_ostream::F_Binary); #endif if (!Error.empty()) { - klee_error("error opening file \"%s\". KLEE may have run out of file " + klee_warning("error opening file \"%s\". KLEE may have run out of file " "descriptors: try to increase the maximum number of open file " "descriptors by using ulimit (%s).", filename.c_str(), Error.c_str()); @@ -1011,9 +1011,7 @@ static char *format_tdiff(char *buf, long seconds) #ifndef SUPPORT_KLEE_UCLIBC static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) { - fprintf(stderr, "error: invalid libc, no uclibc support!\n"); - exit(1); - return 0; + klee_error("invalid libc, no uclibc support!\n"); } #else static void replaceOrRenameFunction(llvm::Module *module, @@ -1176,7 +1174,7 @@ int main(int argc, char **argv, char **envp) { if (pid<0) { klee_error("unable to fork watchdog"); } else if (pid) { - fprintf(stderr, "KLEE: WATCHDOG: watching %d\n", pid); + klee_message("KLEE: WATCHDOG: watching %d\n", pid); fflush(stderr); sys::SetInterruptFunction(interrupt_handle_watchdog); @@ -1193,7 +1191,7 @@ int main(int argc, char **argv, char **envp) { if (errno==ECHILD) { // No child, no need to watch but // return error since we didn't catch // the exit. - fprintf(stderr, "KLEE: watchdog exiting (no child)\n"); + klee_warning("KLEE: watchdog exiting (no child)\n"); return 1; } else if (errno!=EINTR) { perror("watchdog waitpid"); @@ -1208,13 +1206,16 @@ int main(int argc, char **argv, char **envp) { ++level; if (level==1) { - fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via INT\n"); + klee_warning( + "KLEE: WATCHDOG: time expired, attempting halt via INT\n"); kill(pid, SIGINT); } else if (level==2) { - fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via gdb\n"); + klee_warning( + "KLEE: WATCHDOG: time expired, attempting halt via gdb\n"); halt_via_gdb(pid); } else { - fprintf(stderr, "KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)\n"); + klee_warning( + "KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)\n"); kill(pid, SIGKILL); return 1; // what more can we do } @@ -1425,7 +1426,7 @@ int main(int argc, char **argv, char **envp) { if (out) { kTests.push_back(out); } else { - llvm::errs() << "KLEE: unable to open: " << *it << "\n"; + klee_warning("unable to open: %s\n", (*it).c_str()); } } @@ -1462,8 +1463,7 @@ int main(int argc, char **argv, char **envp) { it != ie; ++it) { KTest *out = kTest_fromFile(it->c_str()); if (!out) { - llvm::errs() << "KLEE: unable to open: " << *it << "\n"; - exit(1); + klee_error("unable to open: %s\n", (*it).c_str()); } seeds.push_back(out); } @@ -1477,19 +1477,17 @@ int main(int argc, char **argv, char **envp) { it2 != ie; ++it2) { KTest *out = kTest_fromFile(it2->c_str()); if (!out) { - llvm::errs() << "KLEE: unable to open: " << *it2 << "\n"; - exit(1); + klee_error("unable to open: %s\n", (*it2).c_str()); } seeds.push_back(out); } if (kTestFiles.empty()) { - llvm::errs() << "KLEE: seeds directory is empty: " << *it << "\n"; - exit(1); + klee_error("seeds directory is empty: %s\n", (*it).c_str()); } } if (!seeds.empty()) { - llvm::errs() << "KLEE: using " << seeds.size() << " seeds\n"; + klee_message("KLEE: using %lu seeds\n", seeds.size()); interpreter->useSeeds(&seeds); } if (RunInDir != "") { |