new interface for read_goto_binary()

Author: Daniel Kroening

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -898,10 +898,13 @@ void goto_instrument_parse_optionst::get_goto_program()
 {
   status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
 
-  if(read_goto_binary(cmdline.args[0],
-    goto_model, get_message_handler()))
+  auto result = read_goto_binary(cmdline.args[0], get_message_handler());
+
+  if(!result.has_value())
     throw 0;
 
+  goto_model = std::move(result.value());
+
   config.set(cmdline);
 }
 

src/goto-programs/read_goto_binary.cpp

@@ -36,6 +36,18 @@ bool read_goto_binary(
     filename, dest.symbol_table, dest.goto_functions, message_handler);
 }
 
+optionalt<goto_modelt>
+read_goto_binary(const std::string &filename, message_handlert &message_handler)
+{
+  goto_modelt dest;
+
+  if(read_goto_binary(
+       filename, dest.symbol_table, dest.goto_functions, message_handler))
+    return {};
+  else
+    return dest;
+}
+
 bool read_goto_binary(
   const std::string &filename,
   symbol_tablet &symbol_table,

src/goto-programs/read_goto_binary.h

@@ -14,6 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
+#include <util/deprecate.h>
+#include <util/optional.h>
+
 class goto_functionst;
 class goto_modelt;
 class message_handlert;
@@ -25,11 +28,15 @@ bool read_goto_binary(
   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 &);
+
 bool is_goto_binary(const std::string &filename);
 
 bool read_object_and_link(