trying to catch signals

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/branches/peter-incremental-unwinding@3167 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: schram

src/cbmc/bmc.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/location.h>
 #include <util/time_stopping.h>
 #include <util/message_stream.h>
+#include <util/signal_exception.h>
 
 #include <langapi/mode.h>
 #include <langapi/languages.h>
@@ -448,45 +449,40 @@ bool bmct::run(const goto_functionst &goto_functions)
 	  error(error_str);
 	  return true;
 	}
-
       catch(const char *error_str)
 	{
 	  error(error_str);
 	  return true;
 	}
 
-      catch(std::bad_alloc)
-	{
-	  error() << "Out of memory" << eom;
-	  return true;
-	}
-
     } //while
 
     return verification_result;
   }
-
   catch(std::string &error_str)
   {
     message_streamt message_stream(get_message_handler());
     message_stream.err_location(symex.last_location);
     message_stream.error(error_str);
     return true;
   }
-
   catch(const char *error_str)
   {
     message_streamt message_stream(get_message_handler());
     message_stream.err_location(symex.last_location);
     message_stream.error(error_str);
     return true;
   }
-
   catch(std::bad_alloc)
   {
     error() << "Out of memory" << eom;
     return true;
   }
+  catch(signal_exceptiont& e)
+  {
+    error() << e.what() << eom;
+    return true;
+  }
 }
 
 /*******************************************************************\

src/cbmc/bmc.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <list>
 #include <map>
+#include <exception>
 
 #include <util/hash_cont.h>
 #include <util/options.h>

src/cbmc/cbmc_main.cpp

@@ -14,7 +14,12 @@ Author: Daniel Kroening, [email protected]
 
 */
 
+#include <cstdlib>
+#include <csignal>
+#include <iostream>
+
 #include <util/unicode.h>
+#include <util/signal_exception.h>
 
 #include "cbmc_parseoptions.h"
 
@@ -31,15 +36,50 @@ Function: main
 \*******************************************************************/
 
 #ifdef _MSC_VER
+/*
+//prospective Windows signal handling code
+#include <windows.h>
+BOOL WINAPI CCHandler(DWORD);
+BOOL WINAPI kill_handler(DWORD dwType) 
+{
+  switch(dwType) {
+    case CTRL_C_EVENT:
+    case CTRL_BREAK_EVENT:
+      std::cerr << "signal caught" << std::endl;
+      exit(1);
+      break;
+    default:
+      break;
+  }
+  return TRUE;
+}
+*/
 int wmain(int argc, const wchar_t **argv_wide)
 {
+  /*
+  if (!SetConsoleCtrlHandler((PHANDLER_ROUTINE)CCHandler,TRUE)) {
+    std::cerr << "Unable to install signal handler!" << std::endl;
+    return 243;
+  }
+  */
+
   const char **argv=narrow_argv(argc, argv_wide);
   cbmc_parseoptionst parseoptions(argc, argv);
   return parseoptions.main();
 }
 #else
+//signal_exceptiont signal_exception;
+
+void kill_handler(int s) 
+{
+  //std::cerr << "signal caught" << std::endl;
+  //exit(1);
+  throw signal_exceptiont(s);
+}
+
 int main(int argc, const char **argv)
 {
+  signal(SIGINT,kill_handler);
   cbmc_parseoptionst parseoptions(argc, argv);
   return parseoptions.main();
 }

src/util/signal_exception.h

@@ -0,0 +1,16 @@
+#include <util/i2string.h>
+
+class signal_exceptiont: public std::exception
+{
+ public:
+  signal_exceptiont(int _s) {
+    s = _s;
+  } 
+  
+  virtual const char* what() const throw() {
+    return (std::string("caught signal ")+i2string(s)).c_str();
+  }
+
+ protected:
+  int s;
+};