Do not kill parent processes when CBMC is killed

src/cbmc/cbmc_main.cpp

@@ -21,6 +21,12 @@ Author: Daniel Kroening, [email protected]
 #endif
 
 #include "cbmc_parse_options.h"
+#include <util/signal_catcher.h>
+#include <stdio.h>
+#include <unistd.h>
+
+#include <cstring>
+#include <sys/wait.h>
 
 /*******************************************************************\
 
@@ -48,6 +54,7 @@ int wmain(int argc, const wchar_t **argv_wide)
 int main(int argc, const char **argv)
 {
 #endif
+#if defined(_WIN32)
   cbmc_parse_optionst parse_options(argc, argv);
 
   int res=parse_options.main();
@@ -59,4 +66,45 @@ int main(int argc, const char **argv)
   #endif
 
   return res;
+#else
+  if((argc>1 && 0==strcmp(argv[1],"+nofork"))
+      /* consider: || getpid() == getpgrp()
+       * - no signal catcher in this case */)
+  {
+    argv[1]=argv[0];
+    cbmc_parse_optionst parse_options(argc-1, argv+1);
+
+    int res=parse_options.main();
+
+    #ifdef IREP_HASH_STATS
+    std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << std::endl;
+    std::cout << "IREP_CMP_CNT=" << irep_cmp_cnt << std::endl;
+    std::cout << "IREP_CMP_NE_CNT=" << irep_cmp_ne_cnt << std::endl;
+    #endif
+
+    return res;
+  }
+
+  pid_t child=fork();
+  assert(0<=child);
+  child_pgid=child;
+  if(0==child)
+  {
+    setpgid(0, getpid());
+    char ** args=new char*[argc+2];
+    args[0]=strdup(argv[0]);
+    args[1]=strdup("+nofork");
+    args[argc+1]=0;
+    while(--argc>0)
+      args[argc+1]=strdup(argv[argc]);
+    execvp(argv[0], args);
+    perror("Failed to run child");
+    assert(0);
+  }
+
+  install_signal_catcher();
+  int exitcode=-1;
+  waitpid(child, &exitcode, 0);
+  return WEXITSTATUS(exitcode);
+#endif
 }

src/util/parse_options.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "cmdline.h"
 #include "parse_options.h"
-#include "signal_catcher.h"
 
 /*******************************************************************\
 
@@ -97,9 +96,6 @@ int parse_options_baset::main()
     help();
     return EX_OK;
   }
-
-  // install signal catcher
-  install_signal_catcher();
 
   return doit();
 }

src/util/signal_catcher.cpp

@@ -19,6 +19,8 @@
 
 #include "signal_catcher.h"
 
+pid_t child_pgid;
+
 /*******************************************************************\
 
 Function: install_signal_catcher
@@ -40,10 +42,15 @@ void install_signal_catcher()
 
   act.sa_handler=signal_catcher;
   act.sa_flags=0;
-  sigfillset(&(act.sa_mask));
+  sigemptyset(&(act.sa_mask));
 
   // install signal handler
+  sigaction(SIGHUP, &act, NULL);
+  sigaction(SIGINT, &act, NULL);
   sigaction(SIGTERM, &act, NULL);
+  sigaction(SIGALRM, &act, NULL);
+  sigaction(SIGUSR1, &act, NULL);
+  sigaction(SIGUSR2, &act, NULL);
   #endif
 }
 
@@ -64,7 +71,7 @@ void signal_catcher(int sig)
   #if defined(_WIN32)
   #else
   // kill any children by killing group
-  killpg(0, sig);
+  killpg(child_pgid, sig);
 
   exit(sig);
   #endif

src/util/signal_catcher.h

@@ -1,2 +1,3 @@
 void install_signal_catcher();
 void signal_catcher(int sig);
+extern pid_t child_pgid;