Merge pull request #2642 from diffblue/remove_asm_fix

remove_asm now guarantees that functions called exist

Author: tautschnig

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

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