Use signal(sig, SIG_DFL); raise(sig); instead of abort() (#6518)

As discussed in #6484 (and https://www.gnu.org/software/libc/manual/html_node/Termination-in-Handler.html), simply calling std::abort at the end of a custom signal handler seems to be bad practice. As suggested, this PR changes these calls to instead first reset to the default signal handler for the given signal, and then calling it.
Fixes #6484.

1 files changed, 12 insertions, 6 deletions

diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index 503bbc198..d0628e2a7 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -85,7 +85,8 @@ void sigterm_handler(int sig, siginfo_t* info, void*)
 {
   safe_print(STDERR_FILENO, "cvc5 interrupted by SIGTERM.\n");
   print_statistics();
-  abort();
+  signal(sig, SIG_DFL);
+  raise(sig);
 }
 
 /** Handler for SIGINT, i.e., when the user hits control C. */
@@ -93,7 +94,8 @@ void sigint_handler(int sig, siginfo_t* info, void*)
 {
   safe_print(STDERR_FILENO, "cvc5 interrupted by user.\n");
   print_statistics();
-  abort();
+  signal(sig, SIG_DFL);
+  raise(sig);
 }
 
 #ifdef HAVE_SIGALTSTACK
@@ -126,7 +128,8 @@ void segv_handler(int sig, siginfo_t* info, void* c)
   if (!segvSpin)
   {
     print_statistics();
-    abort();
+    signal(sig, SIG_DFL);
+    raise(sig);
   }
   else
   {
@@ -165,7 +168,8 @@ void segv_handler(int sig, siginfo_t* info, void* c)
     safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
   }
   print_statistics();
-  abort();
+  signal(sig, SIG_DFL);
+  raise(sig);
 #endif /* CVC5_DEBUG */
 }
 #endif /* HAVE_SIGALTSTACK */
@@ -179,7 +183,8 @@ void ill_handler(int sig, siginfo_t* info, void*)
   if (!segvSpin)
   {
     print_statistics();
-    abort();
+    signal(sig, SIG_DFL);
+    raise(sig);
   }
   else
   {
@@ -203,7 +208,8 @@ void ill_handler(int sig, siginfo_t* info, void*)
 #else  /* CVC5_DEBUG */
   safe_print(STDERR_FILENO, "cvc5 executed an illegal instruction.\n");
   print_statistics();
-  abort();
+  signal(sig, SIG_DFL);
+  raise(sig);
 #endif /* CVC5_DEBUG */
 }