Merge pull request #3883 from tautschnig/deprecation-read_goto_binary

Use non-deprecated variants of read_goto_binary [blocks: #3800]

Author: tautschnig

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.

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,15 +95,15 @@ 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)
   {
     error() << "Could not pointerize all linker-defined expressions" << eom;
     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;

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.

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(...)
   {

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<goto_modelt>
 read_goto_binary(const std::string &filename, message_handlert &);