source location when using a contract

Author: kroening

src/cprover/instrument_contracts.cpp

@@ -53,6 +53,18 @@ exprt add_function(irep_idt function_identifier, exprt src)
   return src;
 }
 
+exprt replace_source_location(
+  exprt src,
+  const source_locationt &source_location)
+{
+  for(auto &op : src.operands())
+    op = replace_source_location(op, source_location);
+
+  src.add_source_location() = source_location;
+
+  return src;
+}
+
 static exprt make_assigns_assertion(
   irep_idt function_identifier,
   const exprt::operandst &assigns,
@@ -367,9 +379,10 @@ void replace_function_calls_by_contracts(
 
             auto replaced_lhs = lhs;
             replace_symbol(replaced_lhs);
+            auto fixed_lhs = replace_source_location(replaced_lhs, location);
 
             dest.add(
-              goto_programt::make_assignment(replaced_lhs, rhs, location));
+              goto_programt::make_assignment(fixed_lhs, rhs, location));
           }
         }