diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp index ff7eb0a4dfc..3774cf8489d 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/goto-programs/remove_asm.cpp @@ -25,15 +25,22 @@ Date: December 2014 class remove_asmt { public: - explicit remove_asmt(symbol_tablet &_symbol_table) - : symbol_table(_symbol_table) + remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions) + : symbol_table(_symbol_table), goto_functions(_goto_functions) { } - void process_function(goto_functionst::goto_functiont &); + void operator()() + { + for(auto &f : goto_functions.function_map) + process_function(f.second); + } protected: symbol_tablet &symbol_table; + goto_functionst &goto_functions; + + void process_function(goto_functionst::goto_functiont &); void process_instruction( goto_programt::instructiont &instruction, @@ -102,6 +109,14 @@ void remove_asmt::gcc_asm_function_call( symbol_table.add(symbol); } + + if( + goto_functions.function_map.find(function_identifier) == + goto_functions.function_map.end()) + { + auto &f = goto_functions.function_map[function_identifier]; + f.type = fkt_type; + } } /// removes assembler @@ -303,21 +318,11 @@ void remove_asmt::process_function( remove_skip(goto_function.body); } -/// removes assembler -void remove_asm( - goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table) -{ - remove_asmt rem(symbol_table); - rem.process_function(goto_function); -} - /// removes assembler void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table) { - remove_asmt rem(symbol_table); - for(auto &f : goto_functions.function_map) - rem.process_function(f.second); + remove_asmt rem(symbol_table, goto_functions); + rem(); } /// removes assembler diff --git a/src/goto-programs/remove_asm.h b/src/goto-programs/remove_asm.h index 49d668c74d9..cfe56e6754b 100644 --- a/src/goto-programs/remove_asm.h +++ b/src/goto-programs/remove_asm.h @@ -20,12 +20,8 @@ Date: December 2014 class goto_modelt; class symbol_tablet; -void remove_asm( - goto_functionst::goto_functiont &goto_function, - symbol_tablet &symbol_table); +void remove_asm(goto_functionst &, symbol_tablet &); -void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table); - -void remove_asm(goto_modelt &goto_model); +void remove_asm(goto_modelt &); #endif // CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H