From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 19 Jun 2014 07:31:00 +0000 (-0400)
Subject: Better --segv-spin messages.
X-Git-Tag: cvc5-1.0.0~6758^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=917842682328cdf232487ef761593049118cf485;p=cvc5.git

Better --segv-spin messages.
---

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 14ee82613..bcb3d448f 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -106,7 +106,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
     abort();
   } else {
     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
-    cerr << "Try:  gdb " << progName << " " << getpid() << endl;
+    cerr << "Try:  gdb " << progName << " " << getpid() << endl
+         << " or:  gdb --pid=" << getpid() << " " << progName << endl;
     for(;;) {
       sleep(60);
     }
@@ -141,6 +142,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   } else {
     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
     fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
+    fprintf(stderr, " or:  gdb --pid=%u %s\n", getpid(), progName);
     for(;;) {
       sleep(60);
     }
@@ -181,6 +183,7 @@ void cvc4unexpected() {
   } else {
     fprintf(stderr, "Spinning so that a debugger can be connected.\n");
     fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
+    fprintf(stderr, " or:  gdb --pid=%u %s\n", getpid(), progName);
     for(;;) {
       sleep(60);
     }