languaget is not a messaget

Pass a message handler as an argument to several of its functions, but do not
construct a messaget object without a configured message handler as that is
deprecated.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -274,14 +274,15 @@ struct java_bytecode_language_optionst
 class java_bytecode_languaget:public languaget
 {
 public:
-  void set_language_options(const optionst &) override;
+  void set_language_options(const optionst &, message_handlert &) override;
 
   void set_message_handler(message_handlert &message_handler) override;
 
   virtual bool preprocess(
     std::istream &instream,
     const std::string &path,
-    std::ostream &outstream) override;
+    std::ostream &outstream,
+    message_handlert &message_handler) override;
 
   // This is an extension to languaget
   // required because parsing of Java programs can be initiated without
@@ -291,18 +292,21 @@ class java_bytecode_languaget:public languaget
 
   bool parse(
     std::istream &instream,
-    const std::string &path) override;
+    const std::string &path,
+    message_handlert &message_handler) override;
 
   bool generate_support_functions(
-    symbol_tablet &symbol_table) override;
+    symbol_tablet &symbol_table,
+    message_handlert &message_handler) override;
 
   bool typecheck(
     symbol_tablet &context,
-    const std::string &module) override;
+    const std::string &module,
+    message_handlert &message_handler) override;
 
   virtual bool final(symbol_table_baset &context) override;
 
-  void show_parse(std::ostream &out) override;
+  void show_parse(std::ostream &out, message_handlert &) override;
 
   virtual ~java_bytecode_languaget();
   java_bytecode_languaget(
@@ -332,7 +336,8 @@ class java_bytecode_languaget:public languaget
     const std::string &code,
     const std::string &module,
     exprt &expr,
-    const namespacet &ns) override;
+    const namespacet &ns,
+    message_handlert &message_handler) override;
 
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<java_bytecode_languaget>(); }
@@ -346,32 +351,45 @@ class java_bytecode_languaget:public languaget
   methods_provided(std::unordered_set<irep_idt> &methods) const override;
   virtual void convert_lazy_method(
     const irep_idt &function_id,
-    symbol_table_baset &symbol_table) override;
+    symbol_table_baset &symbol_table,
+    message_handlert &message_handler) override;
 
 protected:
   void convert_single_method(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table,
+<<<<<<< HEAD
     lazy_class_to_declared_symbols_mapt &class_to_declared_symbols)
+=======
+    message_handlert &message_handler)
+>>>>>>> languaget is not a messaget
   {
     convert_single_method(
       function_id,
       symbol_table,
       optionalt<ci_lazy_methods_neededt>(),
+<<<<<<< HEAD
       class_to_declared_symbols);
+=======
+      message_handler);
+>>>>>>> languaget is not a messaget
   }
   bool convert_single_method(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+<<<<<<< HEAD
     lazy_class_to_declared_symbols_mapt &class_to_declared_symbols);
   bool convert_single_method_code(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     lazy_class_to_declared_symbols_mapt &class_to_declared_symbols);
+=======
+    message_handlert &message_handler);
+>>>>>>> languaget is not a messaget
 
-  bool do_ci_lazy_method_conversion(symbol_tablet &);
+  bool do_ci_lazy_method_conversion(symbol_tablet &, message_handlert &);
   const select_pointer_typet &get_pointer_type_selector() const;
 
   optionalt<java_bytecode_language_optionst> language_options;

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -186,13 +186,18 @@ void lazy_goto_modelt::initialize(
           "failed to figure out type of file '" + filename + '\'');
       }
 
+<<<<<<< HEAD:jbmc/src/java_bytecode/lazy_goto_model.cpp
       languaget &language = *lf.language;
       language.set_message_handler(message_handler);
       language.set_language_options(options);
+=======
+      languaget &language=*lf.language;
+      language.set_language_options(options, message_handler);
+>>>>>>> languaget is not a messaget:src/goto-programs/lazy_goto_model.cpp
 
       msg.status() << "Parsing " << filename << messaget::eom;
 
-      if(language.parse(infile, filename))
+      if(language.parse(infile, filename, message_handler))
       {
         throw invalid_source_file_exceptiont("PARSING ERROR");
       }

jbmc/src/java_bytecode/lazy_goto_model.cpp

@@ -540,24 +540,53 @@ int jbmc_parse_optionst::doit()
     cmdline.args.push_back(cmdline.get_value("gb"));
   }
 
+<<<<<<< HEAD
   // Shows the parse tree of the main class
   if(cmdline.isset("show-parse-tree"))
   {
     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, get_message_handler());
+>>>>>>> languaget is not a messaget
 
     log.status() << "Parsing ..." << messaget::eom;
 
+<<<<<<< HEAD
     if(static_cast<java_bytecode_languaget *>(language.get())->parse())
+=======
+    if(language->parse(infile, filename, get_message_handler()))
+>>>>>>> languaget is not a messaget
     {
       log.error() << "PARSING ERROR" << messaget::eom;
       return CPROVER_EXIT_PARSE_ERROR;
     }
 
+<<<<<<< HEAD
     language->show_parse(std::cout);
     return CPROVER_EXIT_SUCCESS;
+=======
+    language->show_parse(std::cout, get_message_handler());
+    return 0;
+  }
+
+  std::function<void(bmct &, const symbol_tablet &)> configure_bmc = nullptr;
+  if(options.get_bool_option("java-unwind-enum-static"))
+  {
+    configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
+      bmc.add_loop_unwind_handler(
+        [&symbol_table](
+          const goto_symex_statet::call_stackt &context,
+          unsigned loop_number,
+          unsigned unwind,
+          unsigned &max_unwind) {
+          return java_enum_static_init_unwind_handler(
+            context, loop_number, unwind, max_unwind, symbol_table);
+        });
+    };
+>>>>>>> languaget is not a messaget
   }
 
   object_factory_params.set(options);

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -123,11 +123,11 @@ goto_modelt load_goto_model_from_java_class(
   parse_java_language_options(command_line, options);
 
   // Configure the language, load the class files
-  language.set_message_handler(null_message_handler);
-  language.set_language_options(options);
-  language.parse(java_code_stream, filename);
-  language.typecheck(lazy_goto_model.symbol_table, "");
-  language.generate_support_functions(lazy_goto_model.symbol_table);
+  language.set_language_options(options, null_message_handler);
+  language.parse(java_code_stream, filename, null_message_handler);
+  language.typecheck(lazy_goto_model.symbol_table, "", null_message_handler);
+  language.generate_support_functions(
+    lazy_goto_model.symbol_table, null_message_handler);
   language.final(lazy_goto_model.symbol_table);
 
   lazy_goto_model.load_all_functions();

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

@@ -174,14 +174,18 @@ SCENARIO(
       command_line.add_flag("no-lazy-methods");
       command_line.add_flag("no-refine-strings");
       test_java_bytecode_languaget language;
-      language.set_message_handler(null_message_handler);
       optionst options;
       parse_java_language_options(command_line, options);
+<<<<<<< HEAD
       language.set_language_options(options);
       config.java.main_class = "AnnotationsEverywhere";
+=======
+      language.set_language_options(options, null_message_handler);
+>>>>>>> languaget is not a messaget
 
       std::istringstream java_code_stream("ignored");
-      language.parse(java_code_stream, "AnnotationsEverywhere.class");
+      language.parse(
+        java_code_stream, "AnnotationsEverywhere.class", null_message_handler);
       const java_class_loadert::parse_tree_with_overlayst &parse_trees =
         language.get_parse_trees_for_class("AnnotationsEverywhere");
       REQUIRE(parse_trees.size() == 1);

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp

@@ -40,26 +40,33 @@ void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
 bool ansi_c_languaget::preprocess(
   std::istream &instream,
   const std::string &path,
-  std::ostream &outstream)
+  std::ostream &outstream,
+  message_handlert &message_handler)
 {
   // stdin?
+<<<<<<< HEAD
   if(path.empty())
     return c_preprocess(instream, outstream, get_message_handler());
+=======
+  if(path=="")
+    return c_preprocess(instream, outstream, message_handler);
+>>>>>>> languaget is not a messaget
 
-  return c_preprocess(path, outstream, get_message_handler());
+  return c_preprocess(path, outstream, message_handler);
 }
 
 bool ansi_c_languaget::parse(
   std::istream &instream,
-  const std::string &path)
+  const std::string &path,
+  message_handlert &message_handler)
 {
   // store the path
   parse_path=path;
 
   // preprocessing
   std::ostringstream o_preprocessed;
 
-  if(preprocess(instream, path, o_preprocessed))
+  if(preprocess(instream, path, o_preprocessed, message_handler))
     return true;
 
   std::istringstream i_preprocessed(o_preprocessed.str());
@@ -73,7 +80,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.clear();
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&codestr;
-  ansi_c_parser.set_message_handler(get_message_handler());
+  ansi_c_parser.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.cpp98=false; // it's not C++
@@ -105,37 +112,38 @@ bool ansi_c_languaget::parse(
 bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module,
+<<<<<<< HEAD
   const bool keep_file_local)
+=======
+  message_handlert &message_handler)
+>>>>>>> languaget is not a messaget
 {
   symbol_tablet new_symbol_table;
 
-  if(ansi_c_typecheck(
-    parse_tree,
-    new_symbol_table,
-    module,
-    get_message_handler()))
+  if(ansi_c_typecheck(parse_tree, new_symbol_table, module, message_handler))
   {
     return true;
   }
 
   remove_internal_symbols(
     new_symbol_table, this->get_message_handler(), keep_file_local);
 
-  if(linking(symbol_table, new_symbol_table, get_message_handler()))
+  if(linking(symbol_table, new_symbol_table, message_handler))
     return true;
 
   return false;
 }
 
 bool ansi_c_languaget::generate_support_functions(
-  symbol_tablet &symbol_table)
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
 {
   // This creates __CPROVER_start and __CPROVER_initialize:
   return ansi_c_entry_point(
-    symbol_table, get_message_handler(), object_factory_params);
+    symbol_table, message_handler, object_factory_params);
 }
 
-void ansi_c_languaget::show_parse(std::ostream &out)
+void ansi_c_languaget::show_parse(std::ostream &out, message_handlert &)
 {
   parse_tree.output(out);
 }
@@ -176,7 +184,8 @@ bool ansi_c_languaget::to_expr(
   const std::string &code,
   const std::string &,
   exprt &expr,
-  const namespacet &ns)
+  const namespacet &ns,
+  message_handlert &message_handler)
 {
   expr.make_nil();
 
@@ -190,7 +199,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.clear();
   ansi_c_parser.set_file(irep_idt());
   ansi_c_parser.in=&i_preprocessed;
-  ansi_c_parser.set_message_handler(get_message_handler());
+  ansi_c_parser.set_message_handler(message_handler);
   ansi_c_parser.mode=config.ansi_c.mode;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_scanner_init();
@@ -204,7 +213,7 @@ bool ansi_c_languaget::to_expr(
     expr=ansi_c_parser.parse_tree.items.front().declarator().value();
 
     // typecheck it
-    result=ansi_c_typecheck(expr, get_message_handler(), ns);
+    result = ansi_c_typecheck(expr, message_handler, ns);
   }
 
   // save some memory

src/ansi-c/ansi_c_language.cpp

@@ -34,26 +34,31 @@ Author: Daniel Kroening, [email protected]
 class ansi_c_languaget:public languaget
 {
 public:
-  void set_language_options(const optionst &options) override
+  void
+  set_language_options(const optionst &options, message_handlert &) override
   {
     object_factory_params.set(options);
   }
 
   bool preprocess(
     std::istream &instream,
     const std::string &path,
-    std::ostream &outstream) override;
+    std::ostream &outstream,
+    message_handlert &message_handler) override;
 
   bool parse(
     std::istream &instream,
-    const std::string &path) override;
+    const std::string &path,
+    message_handlert &message_handler) override;
 
   bool generate_support_functions(
-    symbol_tablet &symbol_table) override;
+    symbol_tablet &symbol_table,
+    message_handlert &message_handler) override;
 
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,
+<<<<<<< HEAD
     const bool keep_file_local) override;
 
   bool can_keep_file_local() override
@@ -66,8 +71,11 @@ class ansi_c_languaget:public languaget
   {
     return typecheck(symbol_table, module, true);
   }
+=======
+    message_handlert &message_handler) override;
+>>>>>>> languaget is not a messaget
 
-  void show_parse(std::ostream &out) override;
+  void show_parse(std::ostream &out, message_handlert &) override;
 
   ~ansi_c_languaget() override;
   ansi_c_languaget() { }
@@ -91,7 +99,8 @@ class ansi_c_languaget:public languaget
     const std::string &code,
     const std::string &module,
     exprt &expr,
-    const namespacet &ns) override;
+    const namespacet &ns,
+    message_handlert &message_handler) override;
 
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<ansi_c_languaget>(); }