Populate function name in source locations for function contracts

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

Author: Nathan Wetzler

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);

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;

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;