Reading/writing goto binaries: consistently use return values

Always use the return value to communicate errors, not a mix of return
values and exceptions.

Author: tautschnig

src/goto-analyzer/static_simplifier.cpp

@@ -190,7 +190,6 @@ bool static_simplifier(
   goto_model.goto_functions.update();
 
   m.status() << "Writing goto binary" << messaget::eom;
-  return write_goto_binary(out,
-                           ns.get_symbol_table(),
-                           goto_model.goto_functions);
+  return write_goto_binary(
+    out, ns.get_symbol_table(), goto_model.goto_functions, message_handler);
 }

src/goto-cc/compile.cpp

@@ -601,7 +601,7 @@ bool compilet::write_bin_object_file(
     return true;
   }
 
-  if(write_goto_binary(outfile, src_goto_model))
+  if(write_goto_binary(outfile, src_goto_model, message_handler))
     return true;
 
   const auto cnt = function_body_count(src_goto_model.goto_functions);

src/goto-harness/goto_harness_parse_options.cpp

@@ -163,8 +163,13 @@ int goto_harness_parse_optionst::doit()
   }
   else
   {
-    write_goto_binary(
-      got_harness_config.out_file, goto_model, log.get_message_handler());
+    if(write_goto_binary(
+         got_harness_config.out_file, goto_model, log.get_message_handler()))
+    {
+      throw deserialization_exceptiont{
+        "failed to write goto program to file '" + got_harness_config.out_file +
+        "'"};
+    }
   }
 
   return CPROVER_EXIT_SUCCESS;

src/goto-programs/read_bin_goto_object.h

@@ -14,13 +14,16 @@ Date: May 2007
 #ifndef CPROVER_GOTO_PROGRAMS_READ_BIN_GOTO_OBJECT_H
 #define CPROVER_GOTO_PROGRAMS_READ_BIN_GOTO_OBJECT_H
 
+#include <util/nodiscard.h>
+
 #include <iosfwd>
 #include <string>
 
 class symbol_table_baset;
 class goto_functionst;
 class message_handlert;
 
+NODISCARD
 bool read_bin_goto_object(
   std::istream &in,
   const std::string &filename,

src/goto-programs/read_goto_binary.h

@@ -12,11 +12,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
 #define CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
 
+#include <util/nodiscard.h>
+#include <util/optional.h>
+
 #include <list>
 #include <string>
 
-#include <util/optional.h>
-
 class goto_modelt;
 class message_handlert;
 
@@ -30,6 +31,7 @@ bool is_goto_binary(const std::string &filename, message_handlert &);
 /// \param [out] dest: GOTO model to update.
 /// \param message_handler: for diagnostics
 /// \return True on error, false otherwise
+NODISCARD
 bool read_objects_and_link(
   const std::list<std::string> &file_names,
   goto_modelt &dest,

src/goto-programs/write_goto_binary.cpp

@@ -13,7 +13,6 @@ Author: CM Wintersteiger
 
 #include <fstream>
 
-#include <util/exception_utils.h>
 #include <util/irep_serialization.h>
 #include <util/message.h>
 
@@ -144,12 +143,14 @@ static void write_goto_binary(
 bool write_goto_binary(
   std::ostream &out,
   const goto_modelt &goto_model,
+  message_handlert &message_handler,
   int version)
 {
   return write_goto_binary(
     out,
     goto_model.symbol_table,
     goto_model.goto_functions,
+    message_handler,
     version);
 }
 
@@ -158,6 +159,7 @@ bool write_goto_binary(
   std::ostream &out,
   const symbol_table_baset &symbol_table,
   const goto_functionst &goto_functions,
+  message_handlert &message_handler,
   int version)
 {
   // header
@@ -169,15 +171,19 @@ bool write_goto_binary(
 
   if(version < GOTO_BINARY_VERSION)
   {
-    throw invalid_command_line_argument_exceptiont(
-      "version " + std::to_string(version) + " no longer supported",
-      "supported version = " + std::to_string(GOTO_BINARY_VERSION));
+    messaget message{message_handler};
+    message.error() << "version " << version << " no longer supported; "
+                    << "supported version = " << GOTO_BINARY_VERSION
+                    << messaget::eom;
+    return true;
   }
   if(version > GOTO_BINARY_VERSION)
   {
-    throw invalid_command_line_argument_exceptiont(
-      "unknown goto binary version " + std::to_string(version),
-      "supported version = " + std::to_string(GOTO_BINARY_VERSION));
+    messaget message{message_handler};
+    message.error() << "unknown goto binary version " << version << "; "
+                    << "supported version = " << GOTO_BINARY_VERSION
+                    << messaget::eom;
+    return true;
   }
   write_goto_binary(out, symbol_table, goto_functions, irepconverter);
   return false;
@@ -198,5 +204,5 @@ bool write_goto_binary(
     return true;
   }
 
-  return write_goto_binary(out, goto_model);
+  return write_goto_binary(out, goto_model, message_handler);
 }

src/goto-programs/write_goto_binary.h

@@ -14,6 +14,8 @@ Author: CM Wintersteiger
 
 #define GOTO_BINARY_VERSION 5
 
+#include <util/nodiscard.h>
+
 #include <iosfwd>
 #include <string>
 
@@ -22,17 +24,22 @@ class goto_modelt;
 class message_handlert;
 class symbol_table_baset;
 
+NODISCARD
 bool write_goto_binary(
   std::ostream &out,
   const goto_modelt &,
-  int version=GOTO_BINARY_VERSION);
+  message_handlert &,
+  int version = GOTO_BINARY_VERSION);
 
+NODISCARD
 bool write_goto_binary(
   std::ostream &out,
   const symbol_table_baset &,
   const goto_functionst &,
+  message_handlert &,
   int version = GOTO_BINARY_VERSION);
 
+NODISCARD
 bool write_goto_binary(
   const std::string &filename,
   const goto_modelt &,

src/symtab2gb/symtab2gb_parse_options.cpp

@@ -106,7 +106,7 @@ static void run_symtab2gb(
   linked_goto_model.symbol_table.swap(linked_symbol_table);
   goto_convert(linked_goto_model, message_handler);
 
-  if(failed(write_goto_binary(out_file, linked_goto_model)))
+  if(failed(write_goto_binary(out_file, linked_goto_model, message_handler)))
   {
     throw system_exceptiont{"failed to write goto binary to " + gb_filename};
   }