label_properties: do not rely on source_locationt's get_function()

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.

In this vein, 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

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

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[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

@@ -100,7 +100,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

@@ -67,13 +67,12 @@ void label_properties(
       it->source_location_nonconst().set_function(function_identifier);
     }
 
-    irep_idt function = it->source_location().get_function();
+    PRECONDITION(!function_identifier.empty());
+    std::string prefix = id2string(function_identifier);
 
-    std::string prefix=id2string(function);
     if(!it->source_location().get_property_class().empty())
     {
-      if(!prefix.empty())
-        prefix+=".";
+      prefix += ".";
 
       std::string class_infix =
         id2string(it->source_location().get_property_class());
@@ -84,8 +83,7 @@ void label_properties(
       prefix+=class_infix;
     }
 
-    if(!prefix.empty())
-      prefix+=".";
+    prefix += ".";
 
     std::size_t &count=property_counters[prefix];
 

src/goto-programs/show_properties.cpp

@@ -19,9 +19,8 @@ Author: Daniel Kroening, [email protected]
 
 #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)
   {
@@ -33,7 +32,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

@@ -45,11 +45,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/ssa_step.cpp

@@ -197,14 +197,13 @@ irep_idt 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
   {