Merge pull request #3113 from diffblue/goto-binary-v5

remove two fields from goto-binary function format

Author: tautschnig

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>