From 2f29c99a136bc8d4fa42aa725b5310f31474ec91 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Tue, 30 May 2017 17:28:46 +0100
Subject: [PATCH] Assign function in instructions introduced by MM I/O
 instrumentation

E.g. the full slicer relies on function being set and will abort
with an assertion violation in that case.
---
 src/goto-programs/mm_io.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp
index fd60525d82f..c3be47553c5 100644
--- a/src/goto-programs/mm_io.cpp
+++ b/src/goto-programs/mm_io.cpp
@@ -74,6 +74,7 @@ void mm_io(
         {
           const dereference_exprt &d=*deref_expr_r.begin();
           source_locationt source_location=it->source_location;
+          irep_idt function=it->function;
           code_function_callt fc;
           const code_typet &ct=to_code_type(mm_io_r.type());
 
@@ -93,6 +94,7 @@ void mm_io(
           goto_function.body.insert_before_swap(it);
           it->make_function_call(fc);
           it->source_location=source_location;
+          it->function=function;
           it++;
         }
       }
@@ -103,6 +105,7 @@ void mm_io(
         {
           const dereference_exprt &d=to_dereference_expr(a.lhs());
           source_locationt source_location=it->source_location;
+          irep_idt function=it->function;
           code_function_callt fc;
           const code_typet &ct=to_code_type(mm_io_w.type());
           const typet &pt=ct.parameters()[0].type();
@@ -117,6 +120,7 @@ void mm_io(
           goto_function.body.insert_before_swap(it);
           it->make_function_call(fc);
           it->source_location=source_location;
+          it->function=function;
           it++;
         }
       }