diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 9 | ||||
| -rw-r--r-- | lib/Solver/STPSolver.cpp | 12 |
2 files changed, 11 insertions, 10 deletions
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 56964b5d..411c07b1 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -11,6 +11,7 @@ #include "MetaSMTBuilder.h" #include "klee/Constraints.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "klee/util/Assignment.h" @@ -281,7 +282,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( fflush(stderr); int pid = fork(); if (pid == -1) { - fprintf(stderr, "error: fork failed (for metaSMT)"); + klee_warning("fork failed (for metaSMT)"); return (SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED); } @@ -388,7 +389,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( } while (res < 0 && errno == EINTR); if (res < 0) { - fprintf(stderr, "error: waitpid() for metaSMT failed"); + klee_warning("waitpid() for metaSMT failed"); return (SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED); } @@ -408,10 +409,10 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( } else if (exitcode == 1) { hasSolution = false; } else if (exitcode == 52) { - fprintf(stderr, "error: metaSMT timed out"); + klee_warning("metaSMT timed out"); return (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT); } else { - fprintf(stderr, "error: metaSMT did not return a recognized code"); + klee_warning("metaSMT did not return a recognized code"); return (SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE); } diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index f2500572..e1d41eba 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -231,7 +231,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, fflush(stderr); int pid = fork(); if (pid == -1) { - fprintf(stderr, "ERROR: fork failed (for STP)"); + klee_warning("fork failed (for STP)"); if (!IgnoreSolverFailures) exit(1); return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED; @@ -266,7 +266,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, } while (res < 0 && errno == EINTR); if (res < 0) { - fprintf(stderr, "ERROR: waitpid() for STP failed"); + klee_warning("waitpid() for STP failed"); if (!IgnoreSolverFailures) exit(1); return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED; @@ -276,8 +276,8 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, // "occasion" return a status when the process was terminated by a // signal, so test signal first. if (WIFSIGNALED(status) || !WIFEXITED(status)) { - fprintf(stderr, "ERROR: STP did not return successfully. Most likely " - "you forgot to run 'ulimit -s unlimited'\n"); + klee_warning("STP did not return successfully. Most likely you forgot " + "to run 'ulimit -s unlimited'"); if (!IgnoreSolverFailures) { exit(1); } @@ -290,11 +290,11 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, } else if (exitcode == 1) { hasSolution = false; } else if (exitcode == 52) { - fprintf(stderr, "error: STP timed out"); + klee_warning("STP timed out"); // mark that a timeout occurred return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } else { - fprintf(stderr, "error: STP did not return a recognized code"); + klee_warning("STP did not return a recognized code"); if (!IgnoreSolverFailures) exit(1); return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; |