From fc14c009e8e9d2274368b54c12f3580a9ec8f718 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 4 Feb 2010 03:31:38 +0000
Subject: src/expr/kind.h is now automatically generated.

Build src/expr before src/util.

Moved CVC4::Command to the expr package.

Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).

Added file-level documentation to Antlr sources

When built for debug, spin on SEGV instead of aborting.  Really useful
for debugging problems that crop up only on long runs.  Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.

Updated src/main/about.h for 2010.
---
 src/main/util.cpp | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

(limited to 'src/main/util.cpp')

diff --git a/src/main/util.cpp b/src/main/util.cpp
index df4ab803d..03ae26092 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Utilities for the main driver.
  **/
 
 #include <cstdio>
@@ -22,24 +22,48 @@
 #include "util/exception.h"
 #include "config.h"
 
+#include "main.h"
+
 using CVC4::Exception;
 using namespace std;
 
 namespace CVC4 {
 namespace main {
 
-// FIXME add comments to functions
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc.
+ */
+bool segvNoSpin = false;
 
+/** 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");
   abort();
 }
 
+/** Handler for SIGSEGV (segfault). */
 void segv_handler(int sig, siginfo_t* info, void*) {
+#ifdef CVC4_DEBUG
+  fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n");
+  if(segvNoSpin) {
+    fprintf(stderr, "No-spin requested, aborting...\n");
+    abort();
+  } else {
+    fprintf(stderr, "Spinning so that a debugger can be connected.\n");
+    fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
+    for(;;) {
+      sleep(60);
+    }
+  }
+#else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 suffered a segfault.\n");
   abort();
+#endif /* CVC4_DEBUG */
 }
 
+/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw() {
   struct sigaction act1;
   act1.sa_sigaction = sigint_handler;
-- 
cgit v1.2.3