diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel index 0ddb17184a..2ba432c93b 100644 Binary files a/regression/ansi-c/arch_flags_mcpu_bad/object.intel and b/regression/ansi-c/arch_flags_mcpu_bad/object.intel differ diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm index d417b14bad..6593905c6b 100644 Binary files a/regression/ansi-c/arch_flags_mcpu_good/object.arm and b/regression/ansi-c/arch_flags_mcpu_good/object.arm differ diff --git a/regression/ansi-c/arch_flags_mthumb_bad/object.intel b/regression/ansi-c/arch_flags_mthumb_bad/object.intel index fc2d521766..d1b887e5be 100644 Binary files a/regression/ansi-c/arch_flags_mthumb_bad/object.intel and b/regression/ansi-c/arch_flags_mthumb_bad/object.intel differ diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm index d0104c3b60..6a398a5058 100644 Binary files a/regression/ansi-c/arch_flags_mthumb_good/object.arm and b/regression/ansi-c/arch_flags_mthumb_good/object.arm differ diff --git a/regression/goto-diff/syntactic-diff1/a.gb b/regression/goto-diff/syntactic-diff1/a.gb deleted file mode 100644 index 0cfbfe7718..0000000000 Binary files a/regression/goto-diff/syntactic-diff1/a.gb and /dev/null differ diff --git a/regression/goto-diff/syntactic-diff1/b.gb b/regression/goto-diff/syntactic-diff1/b.gb deleted file mode 100644 index 98582db0d4..0000000000 Binary files a/regression/goto-diff/syntactic-diff1/b.gb and /dev/null differ diff --git a/regression/goto-diff/syntactic-diff1/test.desc b/regression/goto-diff/syntactic-diff1/test.desc index 6a47a3b1a3..c3b12e93b7 100644 --- a/regression/goto-diff/syntactic-diff1/test.desc +++ b/regression/goto-diff/syntactic-diff1/test.desc @@ -1,6 +1,6 @@ CORE -b.gb -a.gb +b.c +a.c // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 6bf63367ee..76c47e6b00 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -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; diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index 5b42fce4e5..4a5fa52541 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 -/// 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); } diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h index c700f41cc0..a770e7bd39 100644 --- a/src/goto-programs/write_goto_binary.h +++ b/src/goto-programs/write_goto_binary.h @@ -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 #include