Move rewrite_union to goto-programs

There is nothing symex-specific about it, and it is safely usable by code that
does not depend on symex. Resolves some known-inappropriate module dependencies.

Author: tautschnig

jbmc/src/jdiff/CMakeLists.txt

@@ -15,7 +15,6 @@ target_link_libraries(jdiff-lib
     goto-diff-lib
     goto-instrument-lib
     goto-programs
-    goto-symex
     analyses
     java_bytecode
     langapi

jbmc/src/jdiff/Makefile

@@ -24,7 +24,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/goto-symex/rewrite_union$(OBJEXT) \
       ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
       ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
       ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -39,13 +39,12 @@ Author: Peter Schrammel
 #include <goto-programs/remove_unused_functions.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/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
 
-#include <goto-symex/rewrite_union.h>
-
 #include <goto-instrument/cover.h>
 
 #include <pointer-analysis/add_failed_symbols.h>

jbmc/src/jdiff/module_dependencies.txt

@@ -4,7 +4,6 @@ jdiff
 goto-diff
 goto-instrument
 goto-programs
-goto-symex # dubious - rewrite_union
 langapi # should go away
 pointer-analysis
 util

src/cbmc/cbmc_parse_options.cpp

@@ -46,15 +46,14 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
 
-#include <goto-symex/rewrite_union.h>
-
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>

src/goto-diff/Makefile

@@ -24,7 +24,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../goto-instrument/cover_instrument_other$(OBJEXT) \
       ../goto-instrument/cover_util$(OBJEXT) \
-      ../goto-symex/rewrite_union$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \

src/goto-diff/goto_diff_parse_options.cpp

@@ -26,26 +26,25 @@ Author: Peter Schrammel
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/instrument_preconditions.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
-#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_vector.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_asm.h>
-#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/show_properties.h>
+#include <goto-programs/remove_unused_functions.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/read_goto_binary.h>
+#include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
-#include <goto-programs/loop_ids.h>
-#include <goto-programs/link_to_library.h>
-
-#include <goto-symex/rewrite_union.h>
 
 #include <goto-instrument/cover.h>
 

src/goto-diff/module_dependencies.txt

@@ -4,7 +4,6 @@ cpp
 goto-diff
 goto-instrument
 goto-programs
-goto-symex # dubious - rewrite_union and adjust_float should be moved to goto-programs
 java_bytecode # will go away
 langapi # should go away
 pointer-analysis

src/goto-programs/Makefile

@@ -50,6 +50,7 @@ SRC = adjust_float_expressions.cpp \
       remove_unused_functions.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
+      rewrite_union.cpp \
       replace_calls.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \

src/goto-symex/rewrite_union.cpp renamed to src/goto-programs/rewrite_union.cpp

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Symbolic Execution
 
-#ifndef CPROVER_GOTO_SYMEX_REWRITE_UNION_H
-#define CPROVER_GOTO_SYMEX_REWRITE_UNION_H
+#ifndef CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H
+#define CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H
 
 #include <goto-programs/goto_functions.h>
 
@@ -24,4 +24,4 @@ void rewrite_union(goto_functionst::goto_functiont &);
 void rewrite_union(goto_functionst &);
 void rewrite_union(goto_modelt &);
 
-#endif // CPROVER_GOTO_SYMEX_REWRITE_UNION_H
+#endif // CPROVER_GOTO_PROGRAMS_REWRITE_UNION_H

src/goto-symex/rewrite_union.h renamed to src/goto-programs/rewrite_union.h

@@ -10,7 +10,6 @@ SRC = auto_objects.cpp \
       path_storage.cpp \
       postcondition.cpp \
       precondition.cpp \
-      rewrite_union.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \