diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 356baf1b0d5..8b6acc24d75 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -292,13 +292,13 @@ int jdiff_parse_optionst::get_goto_program( if(is_goto_binary(cmdline.args[0])) { - if(read_goto_binary( - cmdline.args[0], - goto_model.symbol_table, - goto_model.goto_functions, - languages.get_message_handler())) + auto tmp_goto_model = + read_goto_binary(cmdline.args[0], languages.get_message_handler()); + if(!tmp_goto_model.has_value()) return CPROVER_EXIT_INCORRECT_TASK; + goto_model = std::move(*tmp_goto_model); + config.set(cmdline); // This one is done. diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index ce19a847cc0..46f921ff285 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -57,22 +57,20 @@ int linker_script_merget::add_linker_script_definitions() return fail; } - goto_modelt original_goto_model; + auto original_goto_model = + read_goto_binary(goto_binary, get_message_handler()); - fail = - read_goto_binary(goto_binary, original_goto_model, get_message_handler()); - - if(fail!=0) + if(!original_goto_model.has_value()) { error() << "Unable to read goto binary for linker script merging" << eom; - return fail; + return 1; } fail=1; linker_valuest linker_values; const auto &pair = - original_goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION); - if(pair == original_goto_model.goto_functions.function_map.end()) + original_goto_model->goto_functions.function_map.find(INITIALIZE_FUNCTION); + if(pair == original_goto_model->goto_functions.function_map.end()) { error() << "No " << INITIALIZE_FUNCTION << " found in goto_functions" << eom; @@ -82,7 +80,7 @@ int linker_script_merget::add_linker_script_definitions() data, cmdline.get_value('T'), pair->second.body, - original_goto_model.symbol_table, + original_goto_model->symbol_table, linker_values); if(fail!=0) { @@ -97,7 +95,7 @@ int linker_script_merget::add_linker_script_definitions() // The keys of linker_values are exactly the elements of // linker_defined_symbols, so iterate over linker_values from now on. - fail = pointerize_linker_defined_symbols(original_goto_model, linker_values); + fail = pointerize_linker_defined_symbols(*original_goto_model, linker_values); if(fail!=0) { @@ -105,7 +103,7 @@ int linker_script_merget::add_linker_script_definitions() return fail; } - fail = compiler.write_bin_object_file(goto_binary, original_goto_model); + fail = compiler.write_bin_object_file(goto_binary, *original_goto_model); if(fail!=0) error() << "Could not write linkerscript-augmented binary" << eom; diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 1fc55a1280b..b16b494d80a 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -332,13 +332,13 @@ int goto_diff_parse_optionst::get_goto_program( if(is_goto_binary(cmdline.args[0])) { - if(read_goto_binary( - cmdline.args[0], - goto_model.symbol_table, - goto_model.goto_functions, - languages.get_message_handler())) + auto tmp_goto_model = + read_goto_binary(cmdline.args[0], languages.get_message_handler()); + if(!tmp_goto_model.has_value()) return CPROVER_EXIT_INCORRECT_TASK; + goto_model = std::move(*tmp_goto_model); + config.set(cmdline); // This one is done. diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index ee714c3762d..4263bd239f1 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -27,20 +27,11 @@ Module: Read Goto Programs #include "elf_reader.h" #include "osx_fat_reader.h" -/// \brief Read a goto binary from a file, but do not update \ref config -/// \param filename: the file name of the goto binary -/// \param dest: the goto model returned -/// \param message_handler: for diagnostics -/// \deprecated Use read_goto_binary(file, message_handler) instead -/// \return true on failure, false on success -bool read_goto_binary( +static bool read_goto_binary( const std::string &filename, - goto_modelt &dest, - message_handlert &message_handler) -{ - return read_goto_binary( - filename, dest.symbol_table, dest.goto_functions, message_handler); -} + symbol_tablet &, + goto_functionst &, + message_handlert &); /// \brief Read a goto binary from a file, but do not update \ref config /// \param filename: the file name of the goto binary @@ -66,7 +57,7 @@ read_goto_binary(const std::string &filename, message_handlert &message_handler) /// \param goto_functions: the goto functions from the goto binary /// \param message_handler: for diagnostics /// \return true on failure, false on success -bool read_goto_binary( +static bool read_goto_binary( const std::string &filename, symbol_tablet &symbol_table, goto_functionst &goto_functions, @@ -240,17 +231,13 @@ bool read_object_and_link( << file_name << messaget::eom; // we read into a temporary model - goto_modelt temp_model; - - if(read_goto_binary( - file_name, - temp_model, - message_handler)) + auto temp_model = read_goto_binary(file_name, message_handler); + if(!temp_model.has_value()) return true; try { - link_goto_model(dest, temp_model, message_handler); + link_goto_model(dest, *temp_model, message_handler); } catch(...) { diff --git a/src/goto-programs/read_goto_binary.h b/src/goto-programs/read_goto_binary.h index 802af17d648..7487119a250 100644 --- a/src/goto-programs/read_goto_binary.h +++ b/src/goto-programs/read_goto_binary.h @@ -22,18 +22,6 @@ class goto_modelt; class message_handlert; class symbol_tablet; -bool read_goto_binary( - const std::string &filename, - symbol_tablet &, - goto_functionst &, - message_handlert &); - -DEPRECATED("use two-parameter variant instead") -bool read_goto_binary( - const std::string &filename, - goto_modelt &dest, - message_handlert &); - optionalt read_goto_binary(const std::string &filename, message_handlert &);