Make the call to rewrite-union configurable

Rewrite union converts union member access to byte extracts.  This is
(apparently) good for CBMC and goto-diff but it makes analysis harder
for goto-analyzer.  So to make them consistent we add an option which
controls whether it is run or not.  This is fixed in each tool but it
takes us closer to common processing of goto programs.

Author: martin

src/cbmc/cbmc_parse_options.cpp

@@ -531,6 +531,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("show-points-to-sets", true);
 
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
+
+  // Options for process_goto_program
+  options.set_option("rewrite-union", true);
 }
 
 /// invoke main modules
@@ -958,7 +961,8 @@ bool cbmc_parse_optionst::process_goto_program(
   remove_returns(goto_model);
   remove_vector(goto_model);
   remove_complex(goto_model);
-  rewrite_union(goto_model);
+  if(options.get_bool_option("rewrite-union"))
+    rewrite_union(goto_model);
 
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -41,6 +41,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
@@ -610,6 +611,7 @@ int goto_analyzer_parse_optionst::doit()
 
   // Perserve backwards compatability in processing
   options.set_option("partial-inline", true);
+  options.set_option("rewrite-union", false);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
@@ -919,6 +921,8 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_returns(goto_model);
     remove_vector(goto_model);
     remove_complex(goto_model);
+    if(options.get_bool_option("rewrite-union"))
+      rewrite_union(goto_model);
 
 #if 0
     // add generic checks

src/goto-diff/goto_diff_parse_options.cpp

@@ -169,6 +169,9 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   }
 
   options.set_option("show-properties", cmdline.isset("show-properties"));
+
+  // Options for process_goto_program
+  options.set_option("rewrite-union", true);
 }
 
 /// invoke main modules
@@ -313,7 +316,8 @@ bool goto_diff_parse_optionst::process_goto_program(
     remove_returns(goto_model);
     remove_vector(goto_model);
     remove_complex(goto_model);
-    rewrite_union(goto_model);
+    if(options.get_bool_option("rewrite-union"))
+      rewrite_union(goto_model);
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;