Revert "Revert "To revert: language-is-a-messaget""

This reverts commit 09287a846d12865379c57b744c753ed711bf0f2c.

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -60,8 +60,8 @@ janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
 void janalyzer_parse_optionst::register_languages()
 {
   // Need ansi C language for __CPROVER_rounding_mode
-  register_language(new_ansi_c_language);
-  register_language(new_java_bytecode_language);
+  register_language(new_ansi_c_language, get_message_handler());
+  register_language(new_java_bytecode_language, get_message_handler());
 }
 
 void janalyzer_parse_optionst::get_command_line_options(optionst &options)

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1542,13 +1542,9 @@ void java_bytecode_languaget::show_parse(
   }
 }
 
-std::unique_ptr<languaget> new_java_bytecode_language()
+std::unique_ptr<languaget> new_java_bytecode_language(message_handlert &message_handler)
 {
-<<<<<<< HEAD
   return std::make_unique<java_bytecode_languaget>(message_handler);
-=======
-  return util_make_unique<java_bytecode_languaget>();
->>>>>>> 510638cb9d... Revert "To revert: language-is-a-messaget"
 }
 
 bool java_bytecode_languaget::from_expr(

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -293,7 +293,6 @@ class java_bytecode_languaget:public languaget
 
   virtual ~java_bytecode_languaget();
   java_bytecode_languaget(
-<<<<<<< HEAD
 <<<<<<< HEAD
     std::unique_ptr<select_pointer_typet> pointer_type_selector)
     : object_factory_parameters(),
@@ -303,10 +302,6 @@ class java_bytecode_languaget:public languaget
       languaget(message_handler),
       java_class_loader(message_handler),
       language_options_initialized(false),
-=======
-    std::unique_ptr<select_pointer_typet> pointer_type_selector):
-      : language_options_initialized(false),
->>>>>>> Revert "To revert: language-is-a-messaget"
       threading_support(false),
       assume_inputs_non_null(false),
       object_factory_parameters(),
@@ -322,9 +317,10 @@ class java_bytecode_languaget:public languaget
   {
   }
 
-  java_bytecode_languaget():
+  explicit java_bytecode_languaget(message_handlert &message_handler):
     java_bytecode_languaget(
-      std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
+      std::unique_ptr<select_pointer_typet>(new select_pointer_typet()),
+      message_handler)
   {
   }
 
@@ -346,17 +342,13 @@ class java_bytecode_languaget:public languaget
     message_handlert &message_handler) override;
 
   std::unique_ptr<languaget> new_language() override
-<<<<<<< HEAD
 <<<<<<< HEAD
   {
     return std::make_unique<java_bytecode_languaget>();
   }
 =======
   { return util_make_unique<java_bytecode_languaget>(get_message_handler()); }
 >>>>>>> 7dd2c65f34... To revert: language-is-a-messaget
-=======
-  { return util_make_unique<java_bytecode_languaget>(); }
->>>>>>> 510638cb9d... Revert "To revert: language-is-a-messaget"
 
   std::string id() const override { return "java"; }
   std::string description() const override { return "Java Bytecode"; }
@@ -430,7 +422,7 @@ class java_bytecode_languaget:public languaget
   void initialize_class_loader(message_handlert &);
 };
 
-std::unique_ptr<languaget> new_java_bytecode_language();
+std::unique_ptr<languaget> new_java_bytecode_language(message_handlert &message_handler);
 
 void parse_java_language_options(const cmdlinet &cmd, optionst &options);
 

jbmc/src/java_bytecode/java_class_loader.h

@@ -36,7 +36,8 @@ class java_class_loadert : public java_class_loader_baset
   typedef std::function<std::vector<irep_idt>(const irep_idt &)>
     get_extra_class_refs_functiont;
 
-  java_class_loadert()
+  explicit java_class_loadert(message_handlert &message_handler)
+    : java_class_loader_baset(message_handler)
   {
   }
 

jbmc/src/java_bytecode/java_class_loader_base.h

@@ -22,6 +22,11 @@ struct java_bytecode_parse_treet;
 class java_class_loader_baset
 {
 public:
+  explicit java_class_loader_baset(message_handlert &message_handler)
+    : messaget(message_handler)
+  {
+  }
+
   /// Clear all classpath entries
   void clear_classpath()
   {

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -37,8 +37,9 @@ class symbolt;
 class java_string_library_preprocesst
 {
 public:
-  java_string_library_preprocesst()
-    : char_type(java_char_type()),
+  explicit java_string_library_preprocesst(message_handlert &message_handler)
+    : messaget(message_handler),
+      char_type(java_char_type()),
       index_type(java_int_type()),
       refined_string_type(index_type, pointer_type(char_type))
   {

jbmc/src/java_bytecode/lazy_goto_model.cpp

@@ -49,6 +49,7 @@ lazy_goto_modelt::lazy_goto_modelt(
       driver_program_can_generate_function_body,
       driver_program_generate_function_body,
       message_handler),
+    language_files(message_handler),
     post_process_function(post_process_function),
     post_process_functions(post_process_functions),
     driver_program_can_generate_function_body(

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -414,8 +414,8 @@ int jbmc_parse_optionst::doit()
       break;
   }
 
-  register_language(new_ansi_c_language);
-  register_language(new_java_bytecode_language);
+  register_language(new_ansi_c_language, get_message_handler());
+  register_language(new_java_bytecode_language, get_message_handler());
 
   if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
        (cmdline.isset("gb") && cmdline.args.empty()) ||

jbmc/src/jdiff/jdiff_languages.cpp

@@ -17,5 +17,5 @@ Author: Peter Schrammel
 
 void jdiff_parse_optionst::register_languages()
 {
-  register_language(new_java_bytecode_language);
+  register_language(new_java_bytecode_language, get_message_handler());
 }

jbmc/unit/java-testing-utils/load_java_class.cpp

@@ -36,7 +36,7 @@ symbol_tablet load_java_class_lazy(
   const std::string &class_path,
   const std::string &main)
 {
-  std::unique_ptr<languaget> lang = new_java_bytecode_language();
+  std::unique_ptr<languaget> lang = new_java_bytecode_language(null_message_handler);
 
   return load_java_class(java_class_name, class_path, main, std::move(lang));
 }
@@ -187,7 +187,7 @@ goto_modelt load_goto_model_from_java_class(
   for(const auto &option : command_line_options)
     command_line.add_option(option.first, option.second);
 
-  std::unique_ptr<languaget> lang = new_java_bytecode_language();
+  std::unique_ptr<languaget> lang = new_java_bytecode_language(null_message_handler);
 
   return load_goto_model_from_java_class(
     java_class_name, class_path, main, std::move(lang), command_line);