diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 48937bbc51b..e9ee849d176 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -37,7 +37,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 1dbcd830f4f..b060ca349d3 100644 --- a/jbmc/unit/Makefile +++ b/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) \ diff --git a/src/assembler/Makefile b/src/assembler/Makefile index ab8ac02a9bd..57638617bdd 100644 --- a/src/assembler/Makefile +++ b/src/assembler/Makefile @@ -1,5 +1,6 @@ SRC = assembler_lex.yy.cpp \ assembler_parser.cpp \ + remove_asm.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/assembler/module_dependencies.txt b/src/assembler/module_dependencies.txt index b3f6e3a4261..9b8ceceb0ae 100644 --- a/src/assembler/module_dependencies.txt +++ b/src/assembler/module_dependencies.txt @@ -1,2 +1,3 @@ assembler +goto-programs util diff --git a/src/goto-programs/remove_asm.cpp b/src/assembler/remove_asm.cpp similarity index 94% rename from src/goto-programs/remove_asm.cpp rename to src/assembler/remove_asm.cpp index 4e218bdb43e..3e618544626 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -18,10 +18,10 @@ Date: December 2014 #include #include -#include +#include +#include -#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); diff --git a/src/goto-programs/remove_asm.h b/src/assembler/remove_asm.h similarity index 93% rename from src/goto-programs/remove_asm.h rename to src/assembler/remove_asm.h index 93b610957eb..eb36468cccb 100644 --- a/src/goto-programs/remove_asm.h +++ b/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 @@ -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 diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index dcd3202c0a0..26ff8e7f573 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -28,6 +28,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include @@ -46,7 +48,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt index 0878747a92b..791561138b6 100644 --- a/src/cbmc/module_dependencies.txt +++ b/src/cbmc/module_dependencies.txt @@ -1,5 +1,6 @@ analyses ansi-c +assembler cpp goto-checker goto-instrument diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 84825f590c4..68266c0fe8d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include @@ -30,7 +32,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include diff --git a/src/goto-analyzer/module_dependencies.txt b/src/goto-analyzer/module_dependencies.txt index fbe3c1b8b0a..72778a5e8df 100644 --- a/src/goto-analyzer/module_dependencies.txt +++ b/src/goto-analyzer/module_dependencies.txt @@ -1,5 +1,6 @@ ansi-c analyses +assembler cpp goto-analyzer goto-programs diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index ad12b42d223..d04221789df 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -32,7 +32,6 @@ Author: Peter Schrammel #include #include #include -#include #include #include #include @@ -53,6 +52,9 @@ Author: Peter Schrammel #include #include + +#include + #include #include "goto_diff.h" diff --git a/src/goto-diff/module_dependencies.txt b/src/goto-diff/module_dependencies.txt index 201ea83e478..da2f874da4a 100644 --- a/src/goto-diff/module_dependencies.txt +++ b/src/goto-diff/module_dependencies.txt @@ -1,5 +1,6 @@ analyses ansi-c +assembler cpp goto-diff goto-instrument diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 867e514010d..96b627eb448 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -39,7 +39,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -67,6 +66,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include + +#include + #include #include "accelerate/accelerate.h" diff --git a/src/goto-instrument/module_dependencies.txt b/src/goto-instrument/module_dependencies.txt index a5e8c9fa445..5d9e0a710aa 100644 --- a/src/goto-instrument/module_dependencies.txt +++ b/src/goto-instrument/module_dependencies.txt @@ -1,6 +1,7 @@ accelerate analyses ansi-c +assembler cpp goto-instrument goto-programs diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index da48da7c821..53062d0b374 100644 --- a/src/goto-programs/Makefile +++ b/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 \ diff --git a/src/goto-programs/module_dependencies.txt b/src/goto-programs/module_dependencies.txt index bfdc19df2c8..817a766a240 100644 --- a/src/goto-programs/module_dependencies.txt +++ b/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