remove two fields from goto-binary function format

This removes the name of the function in every instruction (it's known from
the function that's being read), and an unused field. This also increases
version number of goto binary format to 5.

Author: Daniel Kroening

regression/ansi-c/arch_flags_mcpu_bad/object.intel

@@ -1,6 +1,6 @@
 CORE
-b.gb
-a.gb
+b.c
+a.c
 // Enable multi-line checking
 activate-multi-line-match
 EXIT=0

regression/ansi-c/arch_flags_mcpu_good/object.arm

@@ -20,10 +20,10 @@ Date: June 2006
 
 #include "goto_functions.h"
 
-/// read goto binary format v4
+/// read goto binary format v5
 /// \par parameters: input stream, symbol_table, functions
 /// \return true on error, false otherwise
-static bool read_bin_goto_object_v4(
+static bool read_bin_goto_object_v5(
   std::istream &in,
   symbol_tablet &symbol_table,
   goto_functionst &functions,
@@ -100,13 +100,11 @@ static bool read_bin_goto_object_v4(
       goto_programt::instructiont &instruction=*itarget;
 
       irepconverter.reference_convert(in, instruction.code);
-      irepconverter.read_string_ref(in); // former function
       irepconverter.reference_convert(in, instruction.source_location);
       instruction.type = (goto_program_instruction_typet)
                               irepconverter.read_gb_word(in);
       instruction.guard.make_nil();
       irepconverter.reference_convert(in, instruction.guard);
-      irepconverter.read_string_ref(in); // former event
       instruction.target_number = irepconverter.read_gb_word(in);
       if(instruction.is_target() &&
          rev_target_map.insert(
@@ -225,13 +223,14 @@ bool read_bin_goto_object(
     case 1:
     case 2:
     case 3:
+    case 4:
       message.error() <<
           "The input was compiled with an old version of "
           "goto-cc; please recompile" << messaget::eom;
       return true;
 
-    case 4:
-      return read_bin_goto_object_v4(
+    case 5:
+      return read_bin_goto_object_v5(
         in, symbol_table, functions, irepconverter);
       break;
 

regression/ansi-c/arch_flags_mthumb_bad/object.intel

@@ -21,8 +21,8 @@ Author: CM Wintersteiger
 
 #include <goto-programs/goto_model.h>
 
-/// Writes a goto program to disc, using goto binary format ver 4
-bool write_goto_binary_v4(
+/// Writes a goto program to disc, using goto binary format ver 5
+bool write_goto_binary_v5(
   std::ostream &out,
   const symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
@@ -97,11 +97,9 @@ bool write_goto_binary_v4(
         const goto_programt::instructiont &instruction = *i_it;
 
         irepconverter.reference_convert(instruction.code, out);
-        irepconverter.write_string_ref(out, fct.first);
         irepconverter.reference_convert(instruction.source_location, out);
         write_gb_word(out, (long)instruction.type);
         irepconverter.reference_convert(instruction.guard, out);
-        irepconverter.write_string_ref(out, irep_idt()); // former event
         write_gb_word(out, instruction.target_number);
 
         write_gb_word(out, instruction.targets.size());
@@ -150,17 +148,16 @@ bool write_goto_binary(
   irep_serializationt::ireps_containert irepc;
   irep_serializationt irepconverter(irepc);
 
-  const int current_goto_version = 4;
-  if(version < current_goto_version)
+  if(version < GOTO_BINARY_VERSION)
     throw invalid_command_line_argument_exceptiont(
       "version " + std::to_string(version) + " no longer supported",
-      "supported version = " + std::to_string(current_goto_version));
-  else if(version > current_goto_version)
+      "supported version = " + std::to_string(GOTO_BINARY_VERSION));
+  else if(version > GOTO_BINARY_VERSION)
     throw invalid_command_line_argument_exceptiont(
       "unknown goto binary version " + std::to_string(version),
-      "supported version = " + std::to_string(current_goto_version));
+      "supported version = " + std::to_string(GOTO_BINARY_VERSION));
   else
-    return write_goto_binary_v4(
+    return write_goto_binary_v5(
       out, symbol_table, goto_functions, irepconverter);
 }
 

regression/ansi-c/arch_flags_mthumb_good/object.arm

@@ -12,7 +12,7 @@ Author: CM Wintersteiger
 #ifndef CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
 #define CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
 
-#define GOTO_BINARY_VERSION 4
+#define GOTO_BINARY_VERSION 5
 
 #include <iosfwd>
 #include <string>