Move remove_asm.{h,cpp} to assembler/

Encapsulate assembler-related code in this folder, and make those driver
programs that need to use it load it from there. Notably, jbmc does not actually
use it, it just had a spurious include.

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -37,7 +37,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/set_properties.h>

jbmc/unit/Makefile

@@ -86,7 +86,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \
@@ -132,7 +131,6 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
               $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
               $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
-              $(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \
               $(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
               $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
               $(BMC_DEPS) \

src/assembler/Makefile

@@ -1,5 +1,6 @@
 SRC = assembler_lex.yy.cpp \
       assembler_parser.cpp \
+      remove_asm.cpp \
       # Empty last line
 INCLUDES= -I ..
 

src/assembler/module_dependencies.txt

@@ -1,2 +1,3 @@
 assembler
+goto-programs
 util

src/goto-programs/remove_asm.cpp renamed to src/assembler/remove_asm.cpp

@@ -18,10 +18,10 @@ Date:   December 2014
 #include <util/c_types.h>
 #include <util/string_constant.h>
 
-#include <assembler/assembler_parser.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_skip.h>
 
-#include "goto_model.h"
-#include "remove_skip.h"
+#include "assembler_parser.h"
 
 class remove_asmt
 {

src/goto-programs/remove_asm.h renamed to src/assembler/remove_asm.h

@@ -49,8 +49,8 @@ Date:   December 2014
 /// Unrecognised assembly instructions are ignored (i.e., they are simply
 /// removed from the goto program).
 
-#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H
-#define CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H
+#ifndef CPROVER_ASSEMBLER_REMOVE_ASM_H
+#define CPROVER_ASSEMBLER_REMOVE_ASM_H
 
 #include <goto-programs/goto_functions.h>
 
@@ -61,4 +61,4 @@ void remove_asm(goto_functionst &, symbol_tablet &);
 
 void remove_asm(goto_modelt &);
 
-#endif // CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H
+#endif // CPROVER_ASSEMBLER_REMOVE_ASM_H

src/cbmc/cbmc_parse_options.cpp

@@ -28,6 +28,8 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_preprocess.h>
 #include <ansi-c/cprover_library.h>
 
+#include <assembler/remove_asm.h>
+
 #include <cpp/cprover_library.h>
 
 #include <goto-checker/all_properties_verifier.h>
@@ -46,7 +48,6 @@ Author: Daniel Kroening, [email protected]
 #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/rewrite_union.h>

src/cbmc/module_dependencies.txt

@@ -1,5 +1,6 @@
 analyses
 ansi-c
+assembler
 cpp
 goto-checker
 goto-instrument

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -19,6 +19,8 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/cprover_library.h>
 
+#include <assembler/remove_asm.h>
+
 #include <cpp/cpp_language.h>
 #include <cpp/cprover_library.h>
 
@@ -30,7 +32,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.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_returns.h>

src/goto-analyzer/module_dependencies.txt

@@ -1,5 +1,6 @@
 ansi-c
 analyses
+assembler
 cpp
 goto-analyzer
 goto-programs

src/goto-diff/goto_diff_parse_options.cpp

@@ -32,7 +32,6 @@ Author: Peter Schrammel
 #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_returns.h>
@@ -53,6 +52,9 @@ Author: Peter Schrammel
 #include <langapi/mode.h>
 
 #include <ansi-c/cprover_library.h>
+
+#include <assembler/remove_asm.h>
+
 #include <cpp/cprover_library.h>
 
 #include "goto_diff.h"

src/goto-diff/module_dependencies.txt

@@ -1,5 +1,6 @@
 analyses
 ansi-c
+assembler
 cpp
 goto-diff
 goto-instrument

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -39,7 +39,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/parameter_assignments.h>
 #include <goto-programs/slice_global_inits.h>
@@ -67,6 +66,9 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
+
+#include <assembler/remove_asm.h>
+
 #include <cpp/cprover_library.h>
 
 #include "accelerate/accelerate.h"

src/goto-instrument/module_dependencies.txt

@@ -1,6 +1,7 @@
 accelerate
 analyses
 ansi-c
+assembler
 cpp
 goto-instrument
 goto-programs

src/goto-programs/Makefile

@@ -39,7 +39,6 @@ SRC = adjust_float_expressions.cpp \
       read_bin_goto_object.cpp \
       read_goto_binary.cpp \
       rebuild_goto_start_function.cpp \
-      remove_asm.cpp \
       remove_calls_no_body.cpp \
       remove_complex.cpp \
       remove_const_function_pointers.cpp \

src/goto-programs/module_dependencies.txt

@@ -1,5 +1,4 @@
 analyses # dubious - concerns call_graph and does_remove_const
-assembler # should go away
 goto-programs
 goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness
 json