label_properties now generates a source location if there is none

A source_locationt with id() nil signals that the source location is not
given; an empty string signals that the source location is given.  Goto
instructions without source location are perfectly valid, but we need a
source location to carry the property id.  This fixes label_properties to
create a source location with the right function name if none is given.

Author: kroening

jbmc/src/jbmc/jbmc_parse_options.cpp

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

src/goto-programs/set_properties.cpp

@@ -48,6 +48,7 @@ void label_properties(goto_modelt &goto_model)
 }
 
 void label_properties(
+  const irep_idt function_identifier,
   goto_programt &goto_program,
   std::map<irep_idt, std::size_t> &property_counters)
 {
@@ -59,6 +60,13 @@ void label_properties(
     if(!it->is_assert())
       continue;
 
+    // No source location? Create one.
+    if(it->source_location().is_nil())
+    {
+      it->source_location_nonconst() = source_locationt{};
+      it->source_location_nonconst().set_function(function_identifier);
+    }
+
     irep_idt function = it->source_location().get_function();
 
     std::string prefix=id2string(function);
@@ -89,10 +97,10 @@ void label_properties(
   }
 }
 
-void label_properties(goto_programt &goto_program)
+void label_properties(irep_idt function_identifier, goto_programt &goto_program)
 {
   std::map<irep_idt, std::size_t> property_counters;
-  label_properties(goto_program, property_counters);
+  label_properties(function_identifier, goto_program, property_counters);
 }
 
 void set_properties(
@@ -127,5 +135,5 @@ 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->first, it->second.body, property_counters);
 }

src/goto-programs/set_properties.h

@@ -12,8 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
 #define CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H
 
+#include <util/irep.h>
+
 #include <list>
-#include <string>
 
 class goto_functionst;
 class goto_modelt;
@@ -28,7 +29,7 @@ void set_properties(
   const std::list<std::string> &properties);
 
 void label_properties(goto_functionst &);
-void label_properties(goto_programt &);
+void label_properties(irep_idt function_identifier, goto_programt &);
 void label_properties(goto_modelt &);
 
 #endif // CPROVER_GOTO_PROGRAMS_SET_PROPERTIES_H