Merge pull request #2741 from diffblue/remove_asm_function_id

properly set function id on instructions added by remove_asm

Author: Daniel Kroening

regression/goto-instrument/remove_asm1/main.c

@@ -0,0 +1,9 @@
+void func()
+{
+  asm("mfence");
+}
+
+int main(void)
+{
+  func();
+}

regression/goto-instrument/remove_asm1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/analyses/flow_insensitive_analysis.cpp

@@ -240,6 +240,9 @@ bool flow_insensitive_analysis_baset::do_function_call(
     // get the state at the beginning of the function
     locationt l_begin=goto_function.body.instructions.begin();
 
+    DATA_INVARIANT(
+      l_begin->function == f_it->first, "function names have to match");
+
     // do the edge from the call site to the beginning of the function
     new_data=state.transform(ns, l_call, l_begin);
 

src/goto-programs/remove_asm.cpp

@@ -467,6 +467,9 @@ void remove_asmt::process_function(
       it->make_skip();
       did_something = true;
 
+      for(auto &instruction : tmp_dest.instructions)
+        instruction.function = it->function;
+
       goto_programt::targett next=it;
       next++;