Skip to content

Commit

Permalink
Remove Java's unnecessary languaget::parse peculiarity
Browse files Browse the repository at this point in the history
We can safely use the three-argument version and thereby avoid a need for casting.
  • Loading branch information
tautschnig committed Aug 7, 2024
1 parent d635850 commit 92799f0
Show file tree
Hide file tree
Showing 5 changed files with 6 additions and 22 deletions.
4 changes: 2 additions & 2 deletions jbmc/src/janalyzer/janalyzer_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Check warning on line 383 in jbmc/src/janalyzer/janalyzer_parse_options.cpp

View check run for this annotation

Codecov / codecov/patch

jbmc/src/janalyzer/janalyzer_parse_options.cpp#L383

Added line #L383 was not covered by tests
if(language.get()->parse(unused, "", ui_message_handler))
{
log.error() << "PARSING ERROR" << messaget::eom;
return CPROVER_EXIT_PARSE_ERROR;
Expand Down
11 changes: 0 additions & 11 deletions jbmc/src/java_bytecode/java_bytecode_language.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
6 changes: 0 additions & 6 deletions jbmc/src/java_bytecode/java_bytecode_language.h
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
3 changes: 2 additions & 1 deletion jbmc/src/java_bytecode/lazy_goto_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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");
}
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Check warning on line 461 in jbmc/src/jbmc/jbmc_parse_options.cpp

View check run for this annotation

Codecov / codecov/patch

jbmc/src/jbmc/jbmc_parse_options.cpp#L461

Added line #L461 was not covered by tests
if(language.get()->parse(unused, "", ui_message_handler))
{
log.error() << "PARSING ERROR" << messaget::eom;
return CPROVER_EXIT_PARSE_ERROR;
Expand Down

0 comments on commit 92799f0

Please sign in to comment.