Skip to content

languaget is not a messaget [blocks: #3800] #4050

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 12, 2023
Merged

languaget is not a messaget [blocks: #3800] #4050

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions jbmc/src/janalyzer/janalyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/ci_lazy_methods.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
Loading