Remove the patchy exception handling in Java tools and use default

This is a copy of an earlier patch to the CBMC tools which replaced
patchy and inconsistent exception handling in each tool with the
comprehensive set of catch handlers in parse_options_baset.

Author: martin

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -355,29 +355,8 @@ int janalyzer_parse_optionst::doit()
 
   register_languages();
 
-  try
-  {
-    goto_model =
-      initialize_goto_model(cmdline.args, get_message_handler(), options);
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception: " << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
+  goto_model =
+    initialize_goto_model(cmdline.args, get_message_handler(), options);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
@@ -402,34 +381,7 @@ int janalyzer_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  try
-  {
-    return perform_analysis(options);
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception: " << e << eom;
-    return CPROVER_EXIT_EXCEPTION;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
-  }
+  return perform_analysis(options);
 }
 
 /// Depending on the command line mode, run one of the analysis tasks
@@ -554,8 +506,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
     return CPROVER_EXIT_SUCCESS;
   }
 
-  if(set_properties())
-    return CPROVER_EXIT_SET_PROPERTIES_FAILED;
+  if(cmdline.isset("property"))
+    ::set_properties(goto_model, cmdline.get_values("property"));
 
   if(options.get_bool_option("general-analysis"))
   {
@@ -637,34 +589,6 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
   return CPROVER_EXIT_USAGE_ERROR;
 }
 
-bool janalyzer_parse_optionst::set_properties()
-{
-  try
-  {
-    if(cmdline.isset("property"))
-      ::set_properties(goto_model, cmdline.get_values("property"));
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int)
-  {
-    return true;
-  }
-
-  return false;
-}
-
 bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 {
   try

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -167,7 +167,6 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget
   virtual void get_command_line_options(optionst &options);
 
   virtual bool process_goto_program(const optionst &options);
-  bool set_properties();
 
   virtual int perform_analysis(const optionst &options);
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -429,22 +429,7 @@ int jbmc_parse_optionst::doit()
   //
 
   optionst options;
-  try
-  {
-    get_command_line_options(options);
-  }
-
-  catch(const char *error_msg)
-  {
-    error() << error_msg << eom;
-    return 6; // should contemplate EX_SOFTWARE from sysexits.h
-  }
-
-  catch(const std::string &error_msg)
-  {
-    error() << error_msg << eom;
-    return 6; // should contemplate EX_SOFTWARE from sysexits.h
-  }
+  get_command_line_options(options);
 
   //
   // Print a banner
@@ -640,28 +625,8 @@ int jbmc_parse_optionst::doit()
 
 bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model)
 {
-  try
-  {
-    if(cmdline.isset("property"))
-      ::set_properties(goto_model, cmdline.get_values("property"));
-  }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int)
-  {
-    return true;
-  }
+  if(cmdline.isset("property"))
+    ::set_properties(goto_model, cmdline.get_values("property"));
 
   return false;
 }
@@ -676,7 +641,6 @@ int jbmc_parse_optionst::get_goto_program(
     return 6;
   }
 
-  try
   {
     lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
       *this, options, get_message_handler());
@@ -742,29 +706,6 @@ int jbmc_parse_optionst::get_goto_program(
     status() << config.object_bits_info() << eom;
   }
 
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return 6;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return 6;
-  }
-
-  catch(int)
-  {
-    return 6;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return 6;
-  }
-
   return -1; // no error, continue
 }
 
@@ -780,7 +721,6 @@ void jbmc_parse_optionst::process_goto_function(
   bool using_symex_driven_loading =
     options.get_bool_option("symex-driven-lazy-loading");
 
-  try
   {
     // Removal of RTTI inspection:
     remove_instanceof(
@@ -865,24 +805,6 @@ void jbmc_parse_optionst::process_goto_function(
     // update the function member in each instruction
     function.update_instructions_function();
   }
-
-  catch(const char *e)
-  {
-    error() << e << eom;
-    throw;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    throw;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    throw;
-  }
 }
 
 bool jbmc_parse_optionst::show_loaded_functions(
@@ -937,7 +859,6 @@ bool jbmc_parse_optionst::process_goto_functions(
   goto_modelt &goto_model,
   const optionst &options)
 {
-  try
   {
     status() << "Running GOTO functions transformation passes" << eom;
 
@@ -1025,29 +946,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     remove_skip(goto_model);
   }
 
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int)
-  {
-    return true;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    return true;
-  }
-
   return false;
 }
 

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -346,7 +346,6 @@ bool jdiff_parse_optionst::process_goto_program(
   const optionst &options,
   goto_modelt &goto_model)
 {
-  try
   {
     // remove function pointers
     status() << "Removing function pointers and virtual functions" << eom;
@@ -411,31 +410,6 @@ bool jdiff_parse_optionst::process_goto_program(
     goto_model.goto_functions.update();
   }
 
-  catch(const char *e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(const std::string &e)
-  {
-    error() << e << eom;
-    return true;
-  }
-
-  catch(int e)
-  {
-    error() << "Numeric exception: " << e << eom;
-    return true;
-  }
-
-  catch(const std::bad_alloc &)
-  {
-    error() << "Out of memory" << eom;
-    exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
-    return true;
-  }
-
   return false;
 }