Merge pull request #8407 from tautschnig/java-no-dynamic_cast

Remove Java's unnecessary languaget::parse peculiarity

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -380,8 +380,8 @@ int janalyzer_parse_optionst::doit()
 
     log.status() << "Parsing ..." << messaget::eom;
 
-    if(static_cast<java_bytecode_languaget *>(language.get())
-         ->parse(ui_message_handler))
+    std::istringstream unused;
+    if(language.get()->parse(unused, "", ui_message_handler))
     {
       log.error() << "PARSING ERROR" << messaget::eom;
       return CPROVER_EXIT_PARSE_ERROR;

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -362,17 +362,6 @@ void java_bytecode_languaget::parse_from_main_class(
   }
 }
 
-/// We set the main class (i.e.\ class to start the class loading analysis,
-/// see \ref java_class_loadert) when we have have been given a main class.
-bool java_bytecode_languaget::parse(message_handlert &message_handler)
-{
-  PRECONDITION(language_options.has_value());
-  initialize_class_loader(message_handler);
-  main_class = config.java.main_class;
-  parse_from_main_class(message_handler);
-  return false;
-}
-
 /// We set the main class (i.e.\ class to start the class loading analysis,
 /// see \ref java_class_loadert)
 /// when we have a JAR file given via the -jar option:

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -267,12 +267,6 @@ class java_bytecode_languaget:public languaget
     std::ostream &outstream,
     message_handlert &message_handler) override;
 
-  // This is an extension to languaget
-  // required because parsing of Java programs can be initiated without
-  // opening a file first or providing a path to a file
-  // as dictated by \ref languaget.
-  virtual bool parse(message_handlert &);
-
   bool parse(
     std::istream &instream,
     const std::string &path,

jbmc/src/java_bytecode/lazy_goto_model.cpp

@@ -145,7 +145,8 @@ void lazy_goto_modelt::initialize(
 
     msg.status() << "Parsing ..." << messaget::eom;
 
-    if(dynamic_cast<java_bytecode_languaget &>(language).parse(message_handler))
+    std::istringstream unused;
+    if(language.parse(unused, "", message_handler))
     {
       throw invalid_input_exceptiont("PARSING ERROR");
     }

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -458,8 +458,8 @@ int jbmc_parse_optionst::doit()
 
     log.status() << "Parsing ..." << messaget::eom;
 
-    if(static_cast<java_bytecode_languaget *>(language.get())
-         ->parse(ui_message_handler))
+    std::istringstream unused;
+    if(language.get()->parse(unused, "", ui_message_handler))
     {
       log.error() << "PARSING ERROR" << messaget::eom;
       return CPROVER_EXIT_PARSE_ERROR;