aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Basic/ConstructSolverChain.cpp17
-rw-r--r--lib/Core/Executor.cpp12
-rw-r--r--lib/Core/Searcher.cpp6
-rw-r--r--lib/Solver/MetaSMTSolver.cpp6
-rw-r--r--lib/Solver/Z3Solver.cpp4
5 files changed, 22 insertions, 23 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:
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-15 21:31:53 +0000