From: Morgan Deters Date: Sat, 2 Oct 2010 22:14:44 +0000 (+0000) Subject: dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout... X-Git-Tag: cvc5-1.0.0~8835 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=999b496fbf50525b7245ee28e972d7f0f04a1025;p=cvc5.git dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout... --- diff --git a/src/main/util.cpp b/src/main/util.cpp index e91e80c3f..65f6ed329 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -78,6 +78,9 @@ void segv_handler(int sig, siginfo_t* info, void*) { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 suffered a segfault.\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } abort(); #endif /* CVC4_DEBUG */ } @@ -88,6 +91,9 @@ void ill_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n"); if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } abort(); } else { fprintf(stderr, "Spinning so that a debugger can be connected.\n"); @@ -98,6 +104,9 @@ void ill_handler(int sig, siginfo_t* info, void*) { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 executed an illegal instruction.\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } abort(); #endif /* CVC4_DEBUG */ } @@ -119,6 +128,9 @@ void cvc4unexpected() { } if(segvNoSpin) { fprintf(stderr, "No-spin requested.\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } set_terminate(default_terminator); } else { fprintf(stderr, "Spinning so that a debugger can be connected.\n"); @@ -129,6 +141,9 @@ void cvc4unexpected() { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } set_terminate(default_terminator); #endif /* CVC4_DEBUG */ } @@ -139,11 +154,17 @@ void cvc4terminate() { "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding. " "(Don't do that.)\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } default_terminator(); #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } default_terminator(); #endif /* CVC4_DEBUG */ }