Merge pull request diffblue#392 from diffblue/owen-jones-diffblue/use-macros-for-exit-codes

Use existing macros for exit codes

Author: owen-jones-diffblue

src/driver/sec_driver_parse_options.cpp

@@ -46,6 +46,7 @@
 #include <util/msgstream.h>
 #include <util/prefix.h>
 #include <util/json_map_serializer.h>
+#include <util/exit_codes.h>
 
 #include <cbmc/version.h>
 
@@ -135,7 +136,7 @@ int sec_driver_parse_optionst::doit()
   if(cmdline.isset("version"))
   {
     std::cout << CBMC_VERSION << std::endl;
-    return 0;
+    return CPROVER_EXIT_SUCCESS;
   }
 
   //
@@ -176,7 +177,7 @@ int sec_driver_parse_optionst::doit()
     {
       error() << "lazy-methods-context-sensitive requires --function to be set"
               << messaget::eom;
-      return 6;
+      return CPROVER_EXIT_USAGE_ERROR;
     }
     csvsa_analysis=
       csvsa_load_and_analyze_functions(lazy_goto_model, get_message_handler());
@@ -189,14 +190,14 @@ int sec_driver_parse_optionst::doit()
   if(cmdline.isset("show-symbol-table"))
   {
     ::show_symbol_table(lazy_goto_model.symbol_table, get_ui());
-    return 6;
+    return CPROVER_EXIT_SUCCESS;
   }
 
   std::unique_ptr<goto_modelt> maybe_goto_model =
     lazy_goto_modelt::process_whole_model_and_freeze(
       std::move(lazy_goto_model));
   if(maybe_goto_model == nullptr)
-    return 6;
+    return CPROVER_EXIT_INTERNAL_ERROR;
   goto_modelt &goto_model = *maybe_goto_model;
 
   // show it?
@@ -205,7 +206,7 @@ int sec_driver_parse_optionst::doit()
     namespacet ns(goto_model.symbol_table);
 
     goto_model.goto_functions.output(ns, std::cout);
-    return 6;
+    return CPROVER_EXIT_SUCCESS;
   }
 
   if (cmdline.isset("do-not-use-precise-access-paths"))
@@ -215,11 +216,20 @@ int sec_driver_parse_optionst::doit()
 
   if (cmdline.isset("security-scanner"))
   {
-    return taint_do_security_scan(
-      cmdline.get_value("security-scanner"),
-      goto_model,
-      cmdline.isset("rebuild-taint-cache"),
-      *this) ? 0 : 127;
+    try
+    {
+      return taint_do_security_scan(
+        cmdline.get_value("security-scanner"),
+        goto_model,
+        cmdline.isset("rebuild-taint-cache"),
+        *this) ? CPROVER_EXIT_SUCCESS : CPROVER_EXIT_INCORRECT_TASK;
+    }
+    catch(const std::exception &e)
+    {
+      error()
+        << "ERROR: This exception was raised: " << e.what() << messaget::eom;
+      return CPROVER_EXIT_EXCEPTION;
+    }
   }
 
   if(cmdline.isset("local-value-set-analysis"))
@@ -228,7 +238,7 @@ int sec_driver_parse_optionst::doit()
     if(dbpath=="")
     {
       error() << "Must specify lvsa-summary-directory" << eom;
-      abort();
+      return CPROVER_EXIT_USAGE_ERROR;
     }
 
     json_map_serializert<irep_idt, lvsaa_single_external_set_summaryt>
@@ -252,7 +262,7 @@ int sec_driver_parse_optionst::doit()
           debug() << " " << f.first.c_str() << "\n";
         }
         debug() << eom;
-        abort();
+        return CPROVER_EXIT_INCORRECT_TASK;
       }
       const auto& gf=goto_model.goto_functions.function_map.at(fname);
       class_hierarchyt class_hierarchy;
@@ -330,7 +340,7 @@ int sec_driver_parse_optionst::doit()
         status() << dump_message << eom;
       }
     }
-    return 0;
+    return CPROVER_EXIT_SUCCESS;
   }
 
   if(cmdline.isset("dump-html-program"))
@@ -347,7 +357,7 @@ int sec_driver_parse_optionst::doit()
         << cmdline.get_value("dump-html-program")
         << "' for the HTML dump exists."
         << eom;
-      return -1;
+      return CPROVER_EXIT_INCORRECT_TASK;
     }
     class_hierarchyt class_hierarchy;
     class_hierarchy(goto_model.symbol_table);
@@ -361,12 +371,12 @@ int sec_driver_parse_optionst::doit()
       goto_model.symbol_table,
       inverted_topological_order,
       cmdline.get_value("dump-html-program"));
-    return 0;
+    return CPROVER_EXIT_SUCCESS;
   }
 
   error() << "no analysis option given -- consider reading --help"
           << eom;
-  return 6;
+  return CPROVER_EXIT_INCORRECT_TASK;
 }
 
 void sec_driver_parse_optionst::process_goto_function(