From ef4bb3cd1acba420c28e21cecc180753f37ec528 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 15 Aug 2018 10:51:37 +0100
Subject: [PATCH] properly set function id on instructions added by remove_asm

fixes issue #2653
---
 regression/goto-instrument/remove_asm1/main.c    | 9 +++++++++
 regression/goto-instrument/remove_asm1/test.desc | 8 ++++++++
 src/analyses/flow_insensitive_analysis.cpp       | 3 +++
 src/goto-programs/remove_asm.cpp                 | 3 +++
 4 files changed, 23 insertions(+)
 create mode 100644 regression/goto-instrument/remove_asm1/main.c
 create mode 100644 regression/goto-instrument/remove_asm1/test.desc

diff --git a/regression/goto-instrument/remove_asm1/main.c b/regression/goto-instrument/remove_asm1/main.c
new file mode 100644
index 00000000000..0f44d116833
--- /dev/null
+++ b/regression/goto-instrument/remove_asm1/main.c
@@ -0,0 +1,9 @@
+void func()
+{
+  asm("mfence");
+}
+
+int main(void)
+{
+  func();
+}
diff --git a/regression/goto-instrument/remove_asm1/test.desc b/regression/goto-instrument/remove_asm1/test.desc
new file mode 100644
index 00000000000..3793f7374e1
--- /dev/null
+++ b/regression/goto-instrument/remove_asm1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index 15204ee1c90..ef2acdb9e9d 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/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);
 
diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp
index 4e5d13a57e8..cdf36734ff1 100644
--- a/src/goto-programs/remove_asm.cpp
+++ b/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++;