Populate function name in source locations for function contracts

Nathan Wetzler · Nathan Wetzler · commit 3880b9895525 · 2022-07-28T18:50:36.000-05:00
Added function to C type-checking class that will recursively set the function name in source locations of function contract declaration expressions. Previously, function contract declarations would not store an associated function name in the source location because the function name was not known during parsing. CBMC Viewer reports a failure when analyzing the incomplete coverage report, causing the CMBC Starter Kit to fail during a standard build. Also removed source location from "end function" command during contract checking and added proper source location to function contract instrumentation. Resolves issue #7032
diff --git a/regression/contracts/assigns_repeated_ignored/test.desc b/regression/contracts/assigns_repeated_ignored/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^Ignored duplicate expression '\*x' in assigns clause spec at file main.c line \d+$
+^Ignored duplicate expression '\*x' in assigns clause spec at file main.c line \d+ function .*$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[baz.assigns.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
diff --git a/regression/contracts/contracts_with_function_pointers/test.desc b/regression/contracts/contracts_with_function_pointers/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract bar
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*return\_value\_baz is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/function-calls-05/test.desc b/regression/contracts/function-calls-05/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion foo\(\&x, \&y\) \=\= 10: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/history-pointer-enforce-09/test.desc b/regression/contracts/history-pointer-enforce-09/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^\[foo.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc
@@ -3,9 +3,9 @@ main.c
 --enforce-contract foo --enforce-contract bar --enforce-contract baz
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
+^\[baz.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
+^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS$
diff --git a/regression/contracts/history-pointer-replace-01/test.desc b/regression/contracts/history-pointer-replace-01/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 ASSERT \*\(address_of.*n.*\) > 0
-ASSUME \*\(address_of.*n.*\) = tmp_cc[\$\d]? \+ 2
+ASSUME \*\(address_of.*n.*\) = .*tmp_cc[\$\d]? \+ 2
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-replace-02/test.desc b/regression/contracts/history-pointer-replace-02/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 ASSERT \*\(address_of.*n.*\) = 0
-ASSUME \*\(address_of.*n.*\) ≥ tmp_cc[\$\d]? \+ 2
+ASSUME \*\(address_of.*n.*\) ≥ .*tmp_cc[\$\d]? \+ 2
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-replace-04/test.desc b/regression/contracts/history-pointer-replace-04/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
+^\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/quantifiers-exists-both-enforce/test.desc b/regression/contracts/quantifiers-exists-both-enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-exists-both-replace/test.desc b/regression/contracts/quantifiers-exists-both-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-exists-requires-enforce/test.desc b/regression/contracts/quantifiers-exists-requires-enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-exists-requires-replace/test.desc b/regression/contracts/quantifiers-exists-requires-replace/test.desc
@@ -3,8 +3,8 @@ main.c
 --replace-call-with-contract f1 --replace-call-with-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
-^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
-^\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE$
+^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[f2.precondition.\d+\] line \d+ Check requires clause: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-both-enforce/test.desc b/regression/contracts/quantifiers-forall-both-enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-both-replace/test.desc b/regression/contracts/quantifiers-forall-both-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/quantifiers-forall-requires-enforce/test.desc b/regression/contracts/quantifiers-forall-requires-enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-requires-replace/test.desc b/regression/contracts/quantifiers-forall-requires-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/test_aliasing_enforce/test.desc b/regression/contracts/test_aliasing_enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS
diff --git a/regression/contracts/test_aliasing_ensure/test.desc b/regression/contracts/test_aliasing_ensure/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS
diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/test_aliasing_replace/test.desc b/regression/contracts/test_aliasing_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE
+\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/test_array_memory_enforce/test.desc b/regression/contracts/test_array_memory_enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS
diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
+\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE
+\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/test_possibly_aliased_arguments/test.desc b/regression/contracts/test_possibly_aliased_arguments/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract sub_ptr_values
 ^EXIT=0$
 ^SIGNAL=0$
-\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
+\[sub_ptr_values.precondition.\d+\] line \d+ Check requires clause: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/test_scalar_memory_enforce/test.desc b/regression/contracts/test_scalar_memory_enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/test_scalar_memory_replace/test.desc b/regression/contracts/test_scalar_memory_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
+\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \_\_CPROVER\_r\_ok\(n, sizeof\(int\)\): SUCCESS
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/test_struct_enforce/test.desc b/regression/contracts/test_struct_enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that x->baz is assignable: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that x->qux is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion rval \=\= 10: SUCCESS
diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
+\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS
 \[foo.assigns.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/test_struct_replace/test.desc b/regression/contracts/test_struct_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
+\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion rval \=\= x->baz \+ x->qux: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \*x \=\= \*y: SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --apply-loop-contracts --replace-call-with-contract ackermann
-^\[precondition\.\d+\] .* line 17 Check requires clause: SUCCESS$
-^\[precondition\.\d+\] .* line 17 Check requires clause: SUCCESS$
+^\[ackermann.precondition\.\d+\] line 17 Check requires clause: SUCCESS$
+^\[ackermann.precondition\.\d+\] line 17 Check requires clause: SUCCESS$
 ^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
 ^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$
 ^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
@@ -674,6 +674,28 @@ void c_typecheck_baset::apply_asm_label(
   }
 }
 
+/// Recursively set function name in source locations of expression
+/// tree.  The function is not fully defined during parsing of
+/// function contract declarations, so type-checking is the first
+/// point in time when we can populate the function name in source
+/// locations.
+/// \param [in,out] expr: An expression, with possible subexpressions
+///   as operands.
+/// \param function_name: The function name to add to source locations
+void c_typecheck_baset::populate_function_in_expr(
+  exprt &expr,
+  irep_idt function_name)
+{
+  source_locationt source_location = expr.source_location();
+  source_location.set_function(function_name);
+  expr.add_source_location() = source_location;
+  for(exprt &e : expr.operands())
+  {
+    populate_function_in_expr(e, function_name);
+  }
+  return;
+}
+
 void c_typecheck_baset::typecheck_declaration(
   ansi_c_declarationt &declaration)
 {
@@ -833,6 +855,7 @@ void c_typecheck_baset::typecheck_declaration(
           typecheck_expr(requires);
           implicit_typecast_bool(requires);
           check_history_expr(requires);
+          populate_function_in_expr(requires, identifier);
           lambda_exprt lambda{temporary_parameter_symbols, requires};
           lambda.add_source_location() = requires.source_location();
           requires.swap(lambda);
@@ -841,6 +864,7 @@ void c_typecheck_baset::typecheck_declaration(
         typecheck_spec_assigns(code_type.assigns());
         for(auto &assigns : code_type.assigns())
         {
+          populate_function_in_expr(assigns, identifier);
           lambda_exprt lambda{temporary_parameter_symbols, assigns};
           lambda.add_source_location() = assigns.source_location();
           assigns.swap(lambda);
@@ -866,6 +890,7 @@ void c_typecheck_baset::typecheck_declaration(
             ensures,
             ID_loop_entry,
             CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
+          populate_function_in_expr(ensures, identifier);
           lambda_exprt lambda{temporary_parameter_symbols, ensures};
           lambda.add_source_location() = ensures.source_location();
           ensures.swap(lambda);
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
@@ -153,6 +153,9 @@ class c_typecheck_baset:
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
 
+  // Recursively set function name in source locations of expression
+  void populate_function_in_expr(exprt &expr, irep_idt function_name);
+
   bool break_is_allowed;
   bool continue_is_allowed;
   bool case_is_allowed;
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -1382,15 +1382,12 @@ void code_contractst::enforce_contract(const irep_idt &function)
   goto_functions.function_map.erase(old_function);
 
   // Place a new symbol with the mangled name into the symbol table
-  source_locationt sl;
-  sl.set_file("instrumented for code contracts");
-  sl.set_line("0");
   symbolt mangled_sym;
   const symbolt *original_sym = symbol_table.lookup(original);
   mangled_sym = *original_sym;
   mangled_sym.name = mangled;
   mangled_sym.base_name = mangled;
-  mangled_sym.location = sl;
+  mangled_sym.location = original_sym->location;
   const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
   INVARIANT(
     mangled_found.second,
@@ -1414,7 +1411,7 @@ void code_contractst::enforce_contract(const irep_idt &function)
 
   goto_functiont &wrapper = goto_functions.function_map[original];
   wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
-  wrapper.body.add(goto_programt::make_end_function(sl));
+  wrapper.body.add(goto_programt::make_end_function());
   add_contract_check(original, mangled, wrapper.body);
 }
 
@@ -1485,7 +1482,9 @@ void code_contractst::add_contract_check(
   // with expressions from the call site (e.g. the return value).
   exprt::operandst instantiation_values;
 
-  const auto &source_location = function_symbol.location;
+  source_locationt source_location = function_symbol.location;
+  // Set function in source location to original function
+  source_location.set_function(wrapper_function);
 
   // decl ret
   optionalt<code_returnt> return_stmt;
