From 61c6489187a0696c02e68a044a2bf9251a6cc933 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 20 Sep 2017 15:32:56 +0100 Subject: [PATCH] Verify that language options have been initialized We already had assertions before some of the languaget interface but not for all of them. This can cause errors for regenerating entry points so added assertions. This revealed the problem which is for entry function recreation there is a new languaget that hasn't parsed the cmdline. --- src/cbmc/cbmc_parse_options.cpp | 7 ++++--- src/goto-programs/initialize_goto_model.cpp | 1 + src/goto-programs/rebuild_goto_start_function.cpp | 10 +++++++--- src/goto-programs/rebuild_goto_start_function.h | 3 +++ src/java_bytecode/java_bytecode_language.cpp | 4 ++++ 5 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 265759fc698..886298304f6 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -633,9 +633,10 @@ int cbmc_parse_optionst::get_goto_program( { const std::string &function_id=cmdline.get_value("function"); rebuild_goto_start_functiont start_function_rebuilder( - get_message_handler(), - goto_model.symbol_table, - goto_model.goto_functions); + get_message_handler(), + cmdline, + goto_model.symbol_table, + goto_model.goto_functions); if(start_function_rebuilder(function_id)) { diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 753dff36edb..41e9bce9371 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -138,6 +138,7 @@ bool initialize_goto_model( const std::string &function_id=cmdline.get_value("function"); rebuild_goto_start_functiont start_function_rebuilder( msg.get_message_handler(), + cmdline, goto_model.symbol_table, goto_model.goto_functions); diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index 0949c1da73f..cb4d9e01f3d 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -13,6 +13,7 @@ #include #include #include +#include #include #include @@ -25,11 +26,13 @@ /// body of the _start function). rebuild_goto_start_functiont::rebuild_goto_start_functiont( message_handlert &_message_handler, + const cmdlinet &cmdline, symbol_tablet &symbol_table, goto_functionst &goto_functions): - messaget(_message_handler), - symbol_table(symbol_table), - goto_functions(goto_functions) + messaget(_message_handler), + cmdline(cmdline), + symbol_table(symbol_table), + goto_functions(goto_functions) { } @@ -50,6 +53,7 @@ bool rebuild_goto_start_functiont::operator()( std::unique_ptr language=get_language_from_mode(mode); INVARIANT(language, "No language found for mode: "+id2string(mode)); language->set_message_handler(get_message_handler()); + language->get_language_options(cmdline); // To create a new entry point we must first remove the old one remove_existing_entry_point(); diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h index 870e05a61f6..79086aac570 100644 --- a/src/goto-programs/rebuild_goto_start_function.h +++ b/src/goto-programs/rebuild_goto_start_function.h @@ -10,6 +10,7 @@ #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H #include +class cmdlinet; class symbol_tablet; class goto_functionst; @@ -25,6 +26,7 @@ class rebuild_goto_start_functiont: public messaget public: rebuild_goto_start_functiont( message_handlert &_message_handler, + const cmdlinet &cmdline, symbol_tablet &symbol_table, goto_functionst &goto_functions); @@ -35,6 +37,7 @@ class rebuild_goto_start_functiont: public messaget void remove_existing_entry_point(); + const cmdlinet &cmdline; symbol_tablet &symbol_table; goto_functionst &goto_functions; }; diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 8ea79aafa6d..6d71390627b 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -116,6 +116,7 @@ bool java_bytecode_languaget::generate_start_function( const irep_idt &entry_function_symbol_id, symbol_tablet &symbol_table) { + PRECONDITION(language_options_initialized); const auto res= get_main_symbol( symbol_table, entry_function_symbol_id, get_message_handler()); @@ -200,6 +201,8 @@ bool java_bytecode_languaget::typecheck( symbol_tablet &symbol_table, const std::string &module) { + PRECONDITION(language_options_initialized); + if(string_refinement_enabled) string_preprocess.initialize_conversion_table(); @@ -385,6 +388,7 @@ void java_bytecode_languaget::replace_string_methods( bool java_bytecode_languaget::final(symbol_tablet &symbol_table) { + PRECONDITION(language_options_initialized); java_internal_additions(symbol_table); // replace code of String methods calls by code we generate