Move remove_asm.{h,cpp} to assembler/

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 → 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
 {
@@ -74,17 +74,16 @@ void remove_asmt::gcc_asm_function_call(
   const code_asmt &code,
   goto_programt &dest)
 {
-  irep_idt function_identifier=function_base_name;
+  irep_idt function_identifier = function_base_name;
 
   code_function_callt::argumentst arguments;
 
-  const typet void_pointer=
-    pointer_type(void_typet());
+  const typet void_pointer = pointer_type(void_typet());
 
   // outputs
   forall_operands(it, code.op1())
   {
-    if(it->operands().size()==2)
+    if(it->operands().size() == 2)
     {
       arguments.push_back(
         typecast_exprt(address_of_exprt(it->op1()), void_pointer));
@@ -94,7 +93,7 @@ void remove_asmt::gcc_asm_function_call(
   // inputs
   forall_operands(it, code.op2())
   {
-    if(it->operands().size()==2)
+    if(it->operands().size() == 2)
     {
       arguments.push_back(
         typecast_exprt(address_of_exprt(it->op1()), void_pointer));
@@ -108,19 +107,19 @@ void remove_asmt::gcc_asm_function_call(
 
   code_function_callt function_call(std::move(fkt), std::move(arguments));
 
-  goto_programt::targett call=dest.add_instruction(FUNCTION_CALL);
-  call->code=function_call;
-  call->source_location=code.source_location();
+  goto_programt::targett call = dest.add_instruction(FUNCTION_CALL);
+  call->code = function_call;
+  call->source_location = code.source_location();
 
   // do we have it?
   if(!symbol_table.has_symbol(function_identifier))
   {
     symbolt symbol;
 
-    symbol.name=function_identifier;
-    symbol.type=fkt_type;
-    symbol.base_name=function_base_name;
-    symbol.value=nil_exprt();
+    symbol.name = function_identifier;
+    symbol.type = fkt_type;
+    symbol.base_name = function_base_name;
+    symbol.value = nil_exprt();
     symbol.mode = ID_C;
 
     symbol_table.add(symbol);
@@ -195,11 +194,11 @@ void remove_asmt::process_instruction(
   goto_programt::instructiont &instruction,
   goto_programt &dest)
 {
-  const code_asmt &code=to_code_asm(instruction.code);
+  const code_asmt &code = to_code_asm(instruction.code);
 
-  const irep_idt &flavor=code.get_flavor();
+  const irep_idt &flavor = code.get_flavor();
 
-  if(flavor==ID_gcc)
+  if(flavor == ID_gcc)
     process_instruction_gcc(code, dest);
   else if(flavor == ID_msc)
     process_instruction_msc(code, dest);
@@ -497,7 +496,7 @@ void remove_asmt::process_function(
       for(auto &instruction : tmp_dest.instructions)
         instruction.function = it->function;
 
-      goto_programt::targett next=it;
+      goto_programt::targett next = it;
       next++;
 
       goto_function.body.destructive_insert(next, tmp_dest);

src/goto-programs/remove_asm.h → 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