To revert: language-is-a-messaget

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -72,8 +72,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

@@ -1683,9 +1683,9 @@ void java_bytecode_languaget::show_parse(std::ostream &out, message_handlert &)
   }
 }
 
-std::unique_ptr<languaget> new_java_bytecode_language()
+std::unique_ptr<languaget> new_java_bytecode_language(message_handlert &message_handler)
 {
-  return util_make_unique<java_bytecode_languaget>();
+  return util_make_unique<java_bytecode_languaget>(message_handler);
 }
 
 bool java_bytecode_languaget::from_expr(

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -310,15 +310,34 @@ class java_bytecode_languaget:public languaget
 
   virtual ~java_bytecode_languaget();
   java_bytecode_languaget(
+<<<<<<< HEAD
     std::unique_ptr<select_pointer_typet> pointer_type_selector)
     : object_factory_parameters(),
+=======
+    std::unique_ptr<select_pointer_typet> pointer_type_selector,
+    message_handlert &message_handler):
+      languaget(message_handler),
+      java_class_loader(message_handler),
+      language_options_initialized(false),
+      threading_support(false),
+      assume_inputs_non_null(false),
+      object_factory_parameters(),
+      max_user_array_length(0),
+      lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER),
+      string_refinement_enabled(false),
+      throw_runtime_exceptions(false),
+      assert_uncaught_exceptions(false),
+      throw_assertion_error(false),
+      nondet_static(false),
+>>>>>>> To revert: language-is-a-messaget
       pointer_type_selector(std::move(pointer_type_selector))
   {
   }
 
-  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)
   {
   }
 
@@ -340,7 +359,7 @@ class java_bytecode_languaget:public languaget
     message_handlert &message_handler) override;
 
   std::unique_ptr<languaget> new_language() override
-  { return util_make_unique<java_bytecode_languaget>(); }
+  { return util_make_unique<java_bytecode_languaget>(get_message_handler()); }
 
   std::string id() const override { return "java"; }
   std::string description() const override { return "Java Bytecode"; }
@@ -422,7 +441,7 @@ class java_bytecode_languaget:public languaget
   void initialize_class_loader();
 };
 
-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

@@ -37,7 +37,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

@@ -18,6 +18,11 @@ Author: Daniel Kroening, [email protected]
 class java_class_loader_baset : public messaget
 {
 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

@@ -35,8 +35,9 @@ Date:   March 2017
 class java_string_library_preprocesst:public messaget
 {
 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

@@ -507,8 +507,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

@@ -37,7 +37,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));
 }
@@ -188,7 +188,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);