Only use source_locationt's get_function() for user output

A source location is a place in a text file, and the function information stored
in there need not coincide with the name we use in the goto model.

Part 1: label_properties should use the actual function name so that properties
in different instantiations of a function (as may happen when linking static
functions) get unique names.

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -869,7 +869,7 @@ void jbmc_parse_optionst::process_goto_function(
     if(using_symex_driven_loading)
     {
       // label the assertions
-      label_properties(goto_function.body);
+      label_properties(goto_function.body, function.get_function_id());
 
       goto_function.body.update();
       function.compute_location_numbers();

regression/cbmc/unique_labels1/bar.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(1 < 0);
+}
+
+void bar()
+{
+  foo();
+}

regression/cbmc/unique_labels1/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(0);
+}
+
+void bar();
+
+int main()
+{
+  foo();
+  bar();
+}

regression/cbmc/unique_labels1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+bar.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+assertion\.2
+--
+Each of the assertions in the two functions named "foo" should have a unique
+prefix, and thus be numbered "<prefix>.assertion.1."

regression/contracts/function_check_04/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --apply-code-contracts
 ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$
-^\[foo.1\] line 9 .*: FAILURE$
+^\[__CPROVER_initialize.1\] line 9 .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

src/goto-instrument/aggressive_slicer.cpp

@@ -92,7 +92,7 @@ void aggressive_slicert::doit()
     auto property_loc = find_property(p, goto_model.goto_functions);
     if(!property_loc.has_value())
       throw "unable to find property in call graph";
-    note_functions_to_keep(property_loc.value().get_function());
+    note_functions_to_keep(property_loc->first);
   }
 
   // Add functions within distance of shortest path functions

src/goto-programs/set_properties.cpp

@@ -47,6 +47,7 @@ void label_properties(goto_modelt &goto_model)
 
 void label_properties(
   goto_programt &goto_program,
+  const irep_idt &function_id,
   std::map<irep_idt, std::size_t> &property_counters)
 {
   for(goto_programt::instructionst::iterator
@@ -57,9 +58,7 @@ void label_properties(
     if(!it->is_assert())
       continue;
 
-    irep_idt function=it->source_location.get_function();
-
-    std::string prefix=id2string(function);
+    std::string prefix = id2string(function_id);
     if(it->source_location.get_property_class()!="")
     {
       if(prefix!="")
@@ -87,10 +86,10 @@ void label_properties(
   }
 }
 
-void label_properties(goto_programt &goto_program)
+void label_properties(goto_programt &goto_program, const irep_idt &function_id)
 {
   std::map<irep_idt, std::size_t> property_counters;
-  label_properties(goto_program, property_counters);
+  label_properties(goto_program, function_id, property_counters);
 }
 
 void set_properties(
@@ -126,7 +125,7 @@ void label_properties(goto_functionst &goto_functions)
       it=goto_functions.function_map.begin();
       it!=goto_functions.function_map.end();
       it++)
-    label_properties(it->second.body, property_counters);
+    label_properties(it->second.body, it->first, property_counters);
 }
 
 void make_assertions_false(goto_modelt &goto_model)

src/goto-programs/set_properties.h

@@ -26,7 +26,7 @@ void make_assertions_false(goto_functionst &);
 void make_assertions_false(goto_modelt &);
 
 void label_properties(goto_functionst &);
-void label_properties(goto_programt &);
+void label_properties(goto_programt &, const irep_idt &);
 void label_properties(goto_modelt &);
 
 #endif // CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H

src/goto-programs/show_properties.cpp

@@ -21,10 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include "goto_functions.h"
 #include "goto_model.h"
 
-
-optionalt<source_locationt> find_property(
-    const irep_idt &property,
-    const goto_functionst & goto_functions)
+optionalt<std::pair<irep_idt, source_locationt>>
+find_property(const irep_idt &property, const goto_functionst &goto_functions)
 {
   for(const auto &fct : goto_functions.function_map)
   {
@@ -36,7 +34,7 @@ optionalt<source_locationt> find_property(
       {
         if(ins.source_location.get_property_id() == property)
         {
-          return ins.source_location;
+          return std::make_pair(fct.first, ins.source_location);
         }
       }
     }

src/goto-programs/show_properties.h

@@ -46,11 +46,10 @@ void show_properties(
 /// \param property: irep_idt that identifies property
 /// \param goto_functions: program in which to search for
 ///   the property
-/// \return optional<source_locationt> the location of the
+/// \return A pair of function identifier and source location of the
 ///   property, if found.
-optionalt<source_locationt> find_property(
-    const irep_idt &property,
-    const goto_functionst &goto_functions);
+optionalt<std::pair<irep_idt, source_locationt>>
+find_property(const irep_idt &property, const goto_functionst &goto_functions);
 
 /// \brief Collects the properties in the goto program into a `json_arrayt`
 /// \param json_properties: JSON array to hold the properties

src/goto-symex/symex_target_equation.cpp

@@ -992,14 +992,13 @@ irep_idt symex_target_equationt::SSA_stept::get_property_id() const
   else if(source.pc->is_goto())
   {
     // this is likely an unwinding assertion
-    property_id = id2string(source.pc->source_location.get_function()) +
-                  ".unwind." + std::to_string(source.pc->loop_number);
+    property_id = id2string(source.function_id) + ".unwind." +
+                  std::to_string(source.pc->loop_number);
   }
   else if(source.pc->is_function_call())
   {
     // this is likely a recursion unwinding assertion
-    property_id =
-      id2string(source.pc->source_location.get_function()) + ".recursion";
+    property_id = id2string(source.function_id) + ".recursion";
   }
   else
   {