diff options
author | Daniel Dunbar <daniel@zuster.org> | 2014-09-13 18:22:45 -0700 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2014-09-13 18:22:45 -0700 |
commit | 35723ae8eec286d357e6def1c2adec3638b4af2d (patch) | |
tree | f3adca8ee335176c8dd86ff03cd2a934d4f0e2d2 /lib/Solver | |
parent | f11c0b1039bcadf5420e1d9139200ef1ea93e37a (diff) | |
download | klee-35723ae8eec286d357e6def1c2adec3638b4af2d.tar.gz |
[Solver] Ensure shared memory allocation failures are reported as errors, not asserts.
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/Solver.cpp | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 229fa234..d4e572cf 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -38,6 +38,7 @@ #include <sys/shm.h> #include "llvm/Support/CommandLine.h" +#include "llvm/Support/ErrorHandling.h" llvm::cl::opt<bool> IgnoreSolverFailures("ignore-solver-failures", @@ -518,7 +519,7 @@ public: static unsigned char *shared_memory_ptr; static const unsigned shared_memory_size = 1<<20; -static int shared_memory_id; +static int shared_memory_id = 0; static void stp_error_handler(const char* err_msg) { fprintf(stderr, "error: STP Error: %s\n", err_msg); @@ -546,15 +547,23 @@ STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides) vc_registerErrorHandler(::stp_error_handler); if (useForkedSTP) { + assert(shared_memory_id == 0 && "shared memory id already allocated"); shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700); - assert(shared_memory_id>=0 && "shmget failed"); + if (shared_memory_id < 0) + llvm::report_fatal_error("unable to allocate shared memory region"); shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0); - assert(shared_memory_ptr!=(void*)-1 && "shmat failed"); + if (shared_memory_ptr == (void*)-1) + llvm::report_fatal_error("unable to attach shared memory region"); shmctl(shared_memory_id, IPC_RMID, NULL); } } STPSolverImpl::~STPSolverImpl() { + // Detach the memory region. + shmdt(shared_memory_ptr); + shared_memory_ptr = 0; + shared_memory_id = 0; + delete builder; vc_Destroy(vc); @@ -678,7 +687,8 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) sum += (*it)->size; - assert(sum<shared_memory_size && "not enough shared memory for counterexample"); + if (sum >= shared_memory_size) + llvm::report_fatal_error("not enough shared memory for counterexample"); fflush(stdout); fflush(stderr); |