diff --git a/src/cbmc/cbmc_main.cpp b/src/cbmc/cbmc_main.cpp index 2a379433c29..cf93b4b9d79 100644 --- a/src/cbmc/cbmc_main.cpp +++ b/src/cbmc/cbmc_main.cpp @@ -21,6 +21,12 @@ Author: Daniel Kroening, kroening@kroening.com #endif #include "cbmc_parse_options.h" +#include +#include +#include + +#include +#include /*******************************************************************\ @@ -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 } diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 0e03a5c97ba..48780ddc6b6 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #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(); } diff --git a/src/util/signal_catcher.cpp b/src/util/signal_catcher.cpp index 7c68f6c5247..bb8a02da048 100644 --- a/src/util/signal_catcher.cpp +++ b/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 diff --git a/src/util/signal_catcher.h b/src/util/signal_catcher.h index 9057730ed76..49e803c35d1 100644 --- a/src/util/signal_catcher.h +++ b/src/util/signal_catcher.h @@ -1,2 +1,3 @@ void install_signal_catcher(); void signal_catcher(int sig); +extern pid_t child_pgid;