From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 12 Dec 2017 19:34:46 +0000 (-0800)
Subject: Add SIGTERM handler. (#1440)
X-Git-Tag: cvc5-1.0.0~5415
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=83d2279aaa79ce04aa35b394b5063c6d59ff3ac1;p=cvc5.git

Add SIGTERM handler. (#1440)

Print statistics if CVC4 gets a SIGTERM signal.
---

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 110fc2c67..43c880a7f 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -77,6 +77,14 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
   abort();
 }
 
+/** Handler for SIGTERM. */
+void sigterm_handler(int sig, siginfo_t* info, void*)
+{
+  safe_print(STDERR_FILENO, "CVC4 interrupted by SIGTERM.\n");
+  print_statistics();
+  abort();
+}
+
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   safe_print(STDERR_FILENO, "CVC4 interrupted by user.\n");
@@ -321,6 +329,15 @@ void cvc4_init() throw(Exception) {
   }
 #endif /* HAVE_SIGALTSTACK */
 
+  struct sigaction act5;
+  act5.sa_sigaction = sigterm_handler;
+  act5.sa_flags = SA_SIGINFO;
+  sigemptyset(&act5.sa_mask);
+  if (sigaction(SIGTERM, &act5, NULL))
+  {
+    throw Exception(string("sigaction(SIGTERM) failure: ") + strerror(errno));
+  }
+
 #endif /* __WIN32__ */
 
   set_unexpected(cvc4unexpected);