Skip to content

Commit 31f542a

Browse files
committed
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.
1 parent d7099ae commit 31f542a

36 files changed

+489
-352
lines changed

jbmc/src/janalyzer/janalyzer_parse_options.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -375,18 +375,18 @@ int janalyzer_parse_optionst::doit()
375375
{
376376
std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
377377
CHECK_RETURN(language != nullptr);
378-
language->set_language_options(options);
379-
language->set_message_handler(ui_message_handler);
378+
language->set_language_options(options, ui_message_handler);
380379

381380
log.status() << "Parsing ..." << messaget::eom;
382381

383-
if(static_cast<java_bytecode_languaget *>(language.get())->parse())
382+
if(static_cast<java_bytecode_languaget *>(language.get())
383+
->parse(ui_message_handler))
384384
{
385385
log.error() << "PARSING ERROR" << messaget::eom;
386386
return CPROVER_EXIT_PARSE_ERROR;
387387
}
388388

389-
language->show_parse(std::cout);
389+
language->show_parse(std::cout, ui_message_handler);
390390
return CPROVER_EXIT_SUCCESS;
391391
}
392392

jbmc/src/java_bytecode/README.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -674,10 +674,10 @@ determine which loading strategy to use.
674674
If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is
675675
\ref LAZY_METHODS_MODE_EAGER then eager loading is
676676
used. Under eager loading
677-
\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &)
677+
\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &)
678678
is called once for each method listed in method_bytecode (described above). This
679679
then calls
680-
\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &);
680+
\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 &);
681681

682682
without a ci_lazy_methods_neededt object, which calls
683683
\ref java_bytecode_convert_method, passing in the method parse tree. This in

jbmc/src/java_bytecode/ci_lazy_methods.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
99
#include "ci_lazy_methods.h"
1010

1111
#include <util/expr_iterator.h>
12+
#include <util/message.h>
1213
#include <util/namespace.h>
1314
#include <util/suffix.h>
1415
#include <util/symbol_table.h>

0 commit comments

Comments
 (0)