WIP: message_handlert

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -67,8 +67,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/character_refine_preprocess.h

@@ -29,6 +29,11 @@ Date:   March 2017
 class character_refine_preprocesst:public messaget
 {
 public:
+  explicit character_refine_preprocesst(message_handlert &message_handler)
+    : messaget(message_handler)
+  {
+  }
+
   void initialize_conversion_table();
   codet replace_character_call(const code_function_callt &call) const;
 

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1173,9 +1173,9 @@ void java_bytecode_languaget::show_parse(std::ostream &out)
   }
 }
 
-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

@@ -112,19 +112,29 @@ class java_bytecode_languaget:public languaget
 
   virtual ~java_bytecode_languaget();
   java_bytecode_languaget(
-    std::unique_ptr<select_pointer_typet> pointer_type_selector):
+    std::unique_ptr<select_pointer_typet> pointer_type_selector,
+    message_handlert &message_handler):
+      languaget(message_handler),
+      java_class_loader(message_handler),
+      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),
+      string_preprocess(message_handler),
+      nondet_static(false),
       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)
   {
   }
 
@@ -145,7 +155,7 @@ class java_bytecode_languaget:public languaget
     const namespacet &ns) 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"; }
@@ -211,7 +221,7 @@ class java_bytecode_languaget:public languaget
   std::vector<load_extra_methodst> extra_methods;
 };
 
-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_bytecode_parser.cpp

@@ -32,8 +32,8 @@ Author: Daniel Kroening, [email protected]
 class java_bytecode_parsert:public parsert
 {
 public:
-  explicit java_bytecode_parsert(bool skip_instructions)
-    : skip_instructions(skip_instructions)
+  java_bytecode_parsert(bool skip_instructions, message_handlert &message_handler)
+    : parsert(message_handler), skip_instructions(skip_instructions)
   {
     populate_bytecode_mnemonics_table();
   }
@@ -1875,9 +1875,8 @@ java_bytecode_parse(
   message_handlert &message_handler,
   bool skip_instructions)
 {
-  java_bytecode_parsert java_bytecode_parser(skip_instructions);
+  java_bytecode_parsert java_bytecode_parser(skip_instructions, message_handler);
   java_bytecode_parser.in=&istream;
-  java_bytecode_parser.set_message_handler(message_handler);
 
   bool parser_result=java_bytecode_parser.parse();
 

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,10 @@ 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),
+    character_preprocess(message_handler),
+      char_type(java_char_type()),
       index_type(java_int_type()),
       refined_string_type(index_type, pointer_type(char_type))
   {

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -470,8 +470,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("show-parse-tree"))
   {

jbmc/src/jdiff/jdiff_languages.cpp

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