From 92799f018578ffbf41035c59abea57450b228c1e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Aug 2024 07:55:12 +0000 Subject: [PATCH] Remove Java's unnecessary languaget::parse peculiarity We can safely use the three-argument version and thereby avoid a need for casting. --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 4 ++-- jbmc/src/java_bytecode/java_bytecode_language.cpp | 11 ----------- jbmc/src/java_bytecode/java_bytecode_language.h | 6 ------ jbmc/src/java_bytecode/lazy_goto_model.cpp | 3 ++- jbmc/src/jbmc/jbmc_parse_options.cpp | 4 ++-- 5 files changed, 6 insertions(+), 22 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index d18666c435c..4c63681b1eb 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -380,8 +380,8 @@ int janalyzer_parse_optionst::doit() log.status() << "Parsing ..." << messaget::eom; - if(static_cast(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; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 7d9e8262da6..9f3497313f5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/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: diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index b2f7c95cbe3..8eefa379e75 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/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, diff --git a/jbmc/src/java_bytecode/lazy_goto_model.cpp b/jbmc/src/java_bytecode/lazy_goto_model.cpp index 66da36b57bd..0b49f17ddb2 100644 --- a/jbmc/src/java_bytecode/lazy_goto_model.cpp +++ b/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(language).parse(message_handler)) + std::istringstream unused; + if(language.parse(unused, "", message_handler)) { throw invalid_input_exceptiont("PARSING ERROR"); } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index acd61b63ff4..1ae828e5341 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -458,8 +458,8 @@ int jbmc_parse_optionst::doit() log.status() << "Parsing ..." << messaget::eom; - if(static_cast(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;