From fa80f58e97fce0a23e843bc9618a11168f389bc3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 11 Feb 2019 16:30:27 +0000
Subject: [PATCH] Put current goto binary version in a single place

Updates to the goto binary version should always be consistent, and shouldn't
require changes in multiple places. Also we never support more than one version
at a time.
---
 src/goto-programs/read_bin_goto_object.cpp | 25 ++++++++++------------
 src/goto-programs/write_goto_binary.cpp    |  7 +++---
 2 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
index 76c47e6b00e..201a3074c5b 100644
--- a/src/goto-programs/read_bin_goto_object.cpp
+++ b/src/goto-programs/read_bin_goto_object.cpp
@@ -19,11 +19,12 @@ Date: June 2006
 #include <util/irep_serialization.h>
 
 #include "goto_functions.h"
+#include "write_goto_binary.h"
 
-/// read goto binary format v5
+/// read goto binary format
 /// \par parameters: input stream, symbol_table, functions
 /// \return true on error, false otherwise
-static bool read_bin_goto_object_v5(
+static bool read_bin_goto_object(
   std::istream &in,
   symbol_tablet &symbol_table,
   goto_functionst &functions,
@@ -218,23 +219,19 @@ bool read_bin_goto_object(
   {
     std::size_t version=irepconverter.read_gb_word(in);
 
-    switch(version)
+    if(version < GOTO_BINARY_VERSION)
     {
-    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 5:
-      return read_bin_goto_object_v5(
-        in, symbol_table, functions, irepconverter);
-      break;
-
-    default:
+    }
+    else if(version == GOTO_BINARY_VERSION)
+    {
+      return read_bin_goto_object(in, symbol_table, functions, irepconverter);
+    }
+    else
+    {
       message.error() <<
           "The input was compiled with an unsupported version of "
           "goto-cc; please recompile" << messaget::eom;
diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp
index 4a5fa525410..374991da80a 100644
--- a/src/goto-programs/write_goto_binary.cpp
+++ b/src/goto-programs/write_goto_binary.cpp
@@ -21,8 +21,8 @@ Author: CM Wintersteiger
 
 #include <goto-programs/goto_model.h>
 
-/// Writes a goto program to disc, using goto binary format ver 5
-bool write_goto_binary_v5(
+/// Writes a goto program to disc, using goto binary format
+bool write_goto_binary(
   std::ostream &out,
   const symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
@@ -157,8 +157,7 @@ bool write_goto_binary(
       "unknown goto binary version " + std::to_string(version),
       "supported version = " + std::to_string(GOTO_BINARY_VERSION));
   else
-    return write_goto_binary_v5(
-      out, symbol_table, goto_functions, irepconverter);
+    return write_goto_binary(out, symbol_table, goto_functions, irepconverter);
 }
 
 /// Writes a goto program to disc