From 0cee95cfe268c31196ec74392c5654f42c34ae95 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 22 Jan 2013 19:39:34 +0000 Subject: Added a new option --ignore-solver-failures, disabled by default, to cause KLEE to terminate on fatal solver errors. Better documented the ulimit issue when STP seg faults. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173187 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Solver/Solver.cpp | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) (limited to 'lib/Solver') diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index abb70770..b3d1613d 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -35,6 +35,14 @@ #include #include +#include "llvm/Support/CommandLine.h" + +llvm::cl::opt +IgnoreSolverFailures("ignore-solver-failures", + llvm::cl::init(false), + llvm::cl::desc("Ignore any solver failures (default=off)")); + + using namespace klee; /***/ @@ -640,7 +648,9 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, fflush(stderr); int pid = fork(); if (pid==-1) { - fprintf(stderr, "error: fork failed (for STP)"); + fprintf(stderr, "ERROR: fork failed (for STP)"); + if (!IgnoreSolverFailures) + exit(1); return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED; } @@ -672,7 +682,9 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, } while (res < 0 && errno == EINTR); if (res < 0) { - fprintf(stderr, "error: waitpid() for STP failed"); + fprintf(stderr, "ERROR: waitpid() for STP failed"); + if (!IgnoreSolverFailures) + exit(1); return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED; } @@ -680,7 +692,10 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, // "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"); + fprintf(stderr, "ERROR: STP did not return successfully. Most likely you forgot to run 'ulimit -s unlimited'\n"); + if (!IgnoreSolverFailures) { + exit(1); + } return SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED; } @@ -695,6 +710,8 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } else { fprintf(stderr, "error: STP did not return a recognized code"); + if (!IgnoreSolverFailures) + exit(1); return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; } -- cgit 1.4.1