Merge pull request #4050 from tautschnig/messaget-languaget

languaget is not a messaget [blocks: #3800]
diffblue · Dec 12, 2023 · 3bf78f7 · 3bf78f7
2 parents 64fe4d0 + 82948a4
commit 3bf78f7
Show file tree

Hide file tree

Showing 36 changed files with 489 additions and 352 deletions.
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -376,18 +376,18 @@ int janalyzer_parse_optionst::doit()
   {
     std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
     CHECK_RETURN(language != nullptr);
-    language->set_language_options(options);
-    language->set_message_handler(ui_message_handler);
+    language->set_language_options(options, ui_message_handler);
 
     log.status() << "Parsing ..." << messaget::eom;
 
-    if(static_cast<java_bytecode_languaget *>(language.get())->parse())
+    if(static_cast<java_bytecode_languaget *>(language.get())
+         ->parse(ui_message_handler))
     {
       log.error() << "PARSING ERROR" << messaget::eom;
       return CPROVER_EXIT_PARSE_ERROR;
     }
 
-    language->show_parse(std::cout);
+    language->show_parse(std::cout, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 

diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md
@@ -674,10 +674,10 @@ determine which loading strategy to use.
 If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is
 \ref LAZY_METHODS_MODE_EAGER then eager loading is
 used. Under eager loading
-\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &)
+\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &)
 is called once for each method listed in method_bytecode (described above). This
 then calls
-\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &);
+\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &, message_handlert &);
 
 without a ci_lazy_methods_neededt object, which calls
 \ref java_bytecode_convert_method, passing in the method parse tree. This in

diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp
@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
 #include "ci_lazy_methods.h"
 
 #include <util/expr_iterator.h>
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/suffix.h>
 #include <util/symbol_table.h>