From 45a710216d80f1721e63c9ddcf753c001f3f6e11 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Feb 2019 11:39:24 +0000 Subject: [PATCH] language_filest 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. --- .../java_bytecode/lazy_goto_functions_map.h | 3 +- jbmc/src/java_bytecode/lazy_goto_model.cpp | 3 +- src/goto-cc/compile.cpp | 4 +-- src/goto-programs/initialize_goto_model.cpp | 5 +-- src/langapi/language_file.cpp | 36 ++++++++++++------- src/langapi/language_file.h | 27 +++++++++----- unit/testing-utils/get_goto_model_from_c.cpp | 4 +-- 7 files changed, 51 insertions(+), 31 deletions(-) diff --git a/jbmc/src/java_bytecode/lazy_goto_functions_map.h b/jbmc/src/java_bytecode/lazy_goto_functions_map.h index 7c805ecb839..d8af53dc9b5 100644 --- a/jbmc/src/java_bytecode/lazy_goto_functions_map.h +++ b/jbmc/src/java_bytecode/lazy_goto_functions_map.h @@ -173,7 +173,8 @@ class lazy_goto_functions_mapt final symbol_table_baset &function_symbol_table) const { // Fill in symbol table entry body if not already done - language_files.convert_lazy_method(name, function_symbol_table); + language_files.convert_lazy_method( + name, function_symbol_table, message_handler); underlying_mapt::iterator it = goto_functions.find(name); if(it != goto_functions.end()) diff --git a/jbmc/src/java_bytecode/lazy_goto_model.cpp b/jbmc/src/java_bytecode/lazy_goto_model.cpp index 0cf1f26b9d2..0252346c1dd 100644 --- a/jbmc/src/java_bytecode/lazy_goto_model.cpp +++ b/jbmc/src/java_bytecode/lazy_goto_model.cpp @@ -57,7 +57,6 @@ lazy_goto_modelt::lazy_goto_modelt( driver_program_generate_function_body), message_handler(message_handler) { - language_files.set_message_handler(message_handler); } lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other) @@ -154,7 +153,7 @@ void lazy_goto_modelt::initialize( msg.status() << "Converting" << messaget::eom; - if(language_files.typecheck(symbol_table)) + if(language_files.typecheck(symbol_table, message_handler)) { throw invalid_input_exceptiont("CONVERSION ERROR"); } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 28866121d31..2dce7452396 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -620,14 +620,14 @@ bool compilet::write_bin_object_file( optionalt compilet::parse_source(const std::string &file_name) { language_filest language_files; - language_files.set_message_handler(log.get_message_handler()); if(parse(file_name, language_files)) return {}; // we just typecheck one file here symbol_tablet file_symbol_table; - if(language_files.typecheck(file_symbol_table, keep_file_local)) + if(language_files.typecheck( + file_symbol_table, keep_file_local, log.get_message_handler())) { log.error() << "CONVERSION ERROR" << messaget::eom; return {}; diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index caf1307dd69..7c782608829 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -108,7 +108,7 @@ void initialize_from_source_files( msg.status() << "Converting" << messaget::eom; - if(language_files.typecheck(symbol_table)) + if(language_files.typecheck(symbol_table, message_handler)) { throw invalid_input_exceptiont("CONVERSION ERROR"); } @@ -200,10 +200,7 @@ goto_modelt initialize_goto_model( } language_filest language_files; - language_files.set_message_handler(message_handler); - goto_modelt goto_model; - initialize_from_source_files( sources, options, language_files, goto_model.symbol_table, message_handler); diff --git a/src/langapi/language_file.cpp b/src/langapi/language_file.cpp index 931f29e69d7..8cad3c7d18b 100644 --- a/src/langapi/language_file.cpp +++ b/src/langapi/language_file.cpp @@ -48,8 +48,10 @@ void language_filest::show_parse(std::ostream &out) file.second.language->show_parse(out); } -bool language_filest::parse() +bool language_filest::parse(message_handlert &message_handler) { + messaget log(message_handler); + for(auto &file : file_map) { // open file @@ -58,7 +60,7 @@ bool language_filest::parse() if(!infile) { - error() << "Failed to open " << file.first << eom; + log.error() << "Failed to open " << file.first << messaget::eom; return true; } @@ -68,7 +70,7 @@ bool language_filest::parse() if(language.parse(infile, file.first)) { - error() << "Parsing of " << file.first << " failed" << eom; + log.error() << "Parsing of " << file.first << " failed" << messaget::eom; return true; } @@ -82,7 +84,8 @@ bool language_filest::parse() bool language_filest::typecheck( symbol_table_baset &symbol_table, - const bool keep_file_local) + const bool keep_file_local, + message_handlert &message_handler) { // typecheck interfaces @@ -153,7 +156,8 @@ bool language_filest::typecheck( for(auto &module : module_map) { - if(typecheck_module(symbol_table, module.second, keep_file_local)) + if(typecheck_module( + symbol_table, module.second, keep_file_local, message_handler)) return true; } @@ -203,7 +207,8 @@ bool language_filest::interfaces(symbol_table_baset &symbol_table) bool language_filest::typecheck_module( symbol_table_baset &symbol_table, const std::string &module, - const bool keep_file_local) + const bool keep_file_local, + message_handlert &message_handler) { // check module map @@ -211,28 +216,34 @@ bool language_filest::typecheck_module( if(it==module_map.end()) { - error() << "found no file that provides module " << module << eom; + messaget log(message_handler); + log.error() << "found no file that provides module " << module + << messaget::eom; return true; } - return typecheck_module(symbol_table, it->second, keep_file_local); + return typecheck_module( + symbol_table, it->second, keep_file_local, message_handler); } bool language_filest::typecheck_module( symbol_table_baset &symbol_table, language_modulet &module, - const bool keep_file_local) + const bool keep_file_local, + message_handlert &message_handler) { // already typechecked? if(module.type_checked) return false; + messaget log(message_handler); + // already in progress? if(module.in_progress) { - error() << "circular dependency in " << module.name << eom; + log.error() << "circular dependency in " << module.name << messaget::eom; return true; } @@ -249,14 +260,15 @@ bool language_filest::typecheck_module( it!=dependency_set.end(); it++) { - module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local); + module.in_progress = + !typecheck_module(symbol_table, *it, keep_file_local, message_handler); if(module.in_progress == false) return true; } // type check it - status() << "Type-checking " << module.name << eom; + log.status() << "Type-checking " << module.name << messaget::eom; if(module.file->language->can_keep_file_local()) { diff --git a/src/langapi/language_file.h b/src/langapi/language_file.h index 186cb14a561..70d1db6fa6e 100644 --- a/src/langapi/language_file.h +++ b/src/langapi/language_file.h @@ -17,9 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include +class message_handlert; class language_filet; class languaget; @@ -58,7 +58,7 @@ class language_filet final ~language_filet(); }; -class language_filest:public messaget +class language_filest { private: typedef std::map file_mapt; @@ -101,15 +101,23 @@ class language_filest:public messaget file_map.clear(); } - bool parse(); + bool parse(message_handlert &message_handler); void show_parse(std::ostream &out); bool generate_support_functions(symbol_table_baset &symbol_table); - bool typecheck( + bool + + typecheck( symbol_table_baset &symbol_table, - const bool keep_file_local = false); + const bool keep_file_local, + message_handlert &message_handler); + bool + typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler) + { + return typecheck(symbol_table, false, message_handler); + } bool final(symbol_table_baset &symbol_table); @@ -120,7 +128,8 @@ class language_filest:public messaget // for this to be legal. void convert_lazy_method( const irep_idt &id, - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { PRECONDITION(symbol_table.has_symbol(id)); lazy_method_mapt::iterator it=lazy_method_map.find(id); @@ -144,12 +153,14 @@ class language_filest:public messaget bool typecheck_module( symbol_table_baset &symbol_table, language_modulet &module, - const bool keep_file_local); + const bool keep_file_local, + message_handlert &message_handler); bool typecheck_module( symbol_table_baset &symbol_table, const std::string &module, - const bool keep_file_local); + const bool keep_file_local, + message_handlert &message_handler); }; #endif // CPROVER_UTIL_LANGUAGE_FILE_H diff --git a/unit/testing-utils/get_goto_model_from_c.cpp b/unit/testing-utils/get_goto_model_from_c.cpp index f6e9c2cd456..e9437bacc80 100644 --- a/unit/testing-utils/get_goto_model_from_c.cpp +++ b/unit/testing-utils/get_goto_model_from_c.cpp @@ -44,7 +44,6 @@ goto_modelt get_goto_model_from_c(std::istream &in) } language_filest language_files; - language_files.set_message_handler(null_message_handler); language_filet &language_file = language_files.add_file(""); @@ -66,7 +65,8 @@ goto_modelt get_goto_model_from_c(std::istream &in) goto_modelt goto_model; { - const bool error = language_files.typecheck(goto_model.symbol_table); + const bool error = + language_files.typecheck(goto_model.symbol_table, null_message_handler); if(error) throw invalid_input_exceptiont("typechecking failed");