diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-09-13 22:13:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-09-13 22:13:36 +0000 |
commit | 5e619ab6d4622403cc427c17f4282900deb940d5 (patch) | |
tree | 3903755af0f3bbf1f10af34d0511fa5807646574 /src/main/util.cpp | |
parent | 67f05d7dd6881c689c6e5385feff32d81ae05fb8 (diff) |
statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given
Diffstat (limited to 'src/main/util.cpp')
-rw-r--r-- | src/main/util.cpp | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/src/main/util.cpp b/src/main/util.cpp index c685766fa..968563b97 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -24,7 +24,9 @@ #include <signal.h> #include "util/exception.h" +#include "util/options.h" #include "util/Assert.h" +#include "util/stats.h" #include "cvc4autoconfig.h" #include "main.h" @@ -42,9 +44,21 @@ namespace main { */ bool segvNoSpin = false; +/** Handler for SIGXCPU, i.e., timeout. */ +void timeout_handler(int sig, siginfo_t* info, void*) { + fprintf(stderr, "CVC4 interrupted by timeout.\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } + abort(); +} + /** Handler for SIGINT, i.e., when the user hits control C. */ void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); + if(options.statistics) { + StatisticsRegistry::flushStatistics(cerr); + } abort(); } @@ -123,10 +137,17 @@ void cvc4_init() throw() { throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno)); struct sigaction act2; - act2.sa_sigaction = segv_handler; + act2.sa_sigaction = timeout_handler; act2.sa_flags = SA_SIGINFO; sigemptyset(&act2.sa_mask); - if(sigaction(SIGSEGV, &act2, NULL)) + if(sigaction(SIGXCPU, &act2, NULL)) + throw Exception(string("sigaction(SIGXCPU) failure: ") + strerror(errno)); + + struct sigaction act3; + act3.sa_sigaction = segv_handler; + act3.sa_flags = SA_SIGINFO; + sigemptyset(&act3.sa_mask); + if(sigaction(SIGSEGV, &act3, NULL)) throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); set_unexpected(cvc4unexpected); |