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++; } }