make_assigns_assertion now gets function identifier

Author: kroening

src/cprover/instrument_contracts.cpp

@@ -41,8 +41,22 @@ static bool is_symbol_member(const exprt &expr)
     return false;
 }
 
-static exprt
-make_assigns_assertion(const exprt::operandst &assigns, const exprt &lhs)
+// add the function to the source location
+exprt add_function(irep_idt function_identifier, exprt src)
+{
+  for(auto &op : src.operands())
+    op = add_function(function_identifier, op);
+
+  if(!src.source_location().get_file().empty())
+    src.add_source_location().set_function(function_identifier);
+
+  return src;
+}
+
+static exprt make_assigns_assertion(
+  irep_idt function_identifier,
+  const exprt::operandst &assigns,
+  const exprt &lhs)
 {
   // trivial match?
   if(is_symbol_member(lhs))
@@ -72,6 +86,7 @@ make_assigns_assertion(const exprt::operandst &assigns, const exprt &lhs)
     }
     else
     {
+      // auto fixed_a = add_function(function_identifier, a);
       auto target_address = make_address(a);
       auto lhs_address = make_address(lhs);
       lhs_address =
@@ -150,18 +165,6 @@ exprt replace_old(
   }
 }
 
-// add the function to the source location
-exprt add_function(irep_idt function_identifier, exprt src)
-{
-  for(auto &op : src.operands())
-    op = add_function(function_identifier, op);
-
-  if(!src.source_location().get_file().empty())
-    src.add_source_location().set_function(function_identifier);
-
-  return src;
-}
-
 void instrument_contract_checks(
   goto_functionst::function_mapt::value_type &f,
   const namespacet &ns)
@@ -246,7 +249,7 @@ void instrument_contract_checks(
 
         // maybe not ok
         auto assigns_assertion =
-          make_assigns_assertion(contract.assigns(), lhs);
+          make_assigns_assertion(f.first, contract.assigns(), lhs);
         auto location = it->source_location();
         location.set_property_class("assigns");
         location.set_comment("assigns clause");