Merge pull request #6902 from diffblue/label_properties_source_location

label_properties now generates a source location if there is none

Author: kroening

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -720,7 +720,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();

regression/contracts/function-pointer-contracts-replace/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --replace-call-with-contract foo
-^\[precondition.\d+] Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
+^\[precondition.\d+] file main.c line 19 Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
 ^\[main.assertion.\d+].* assertion outfun1 == contract: SUCCESS$
 ^\[main.assertion.\d+].* assertion outfun2 == contract: SUCCESS$
 ^EXIT=0$

src/ansi-c/parser.y

@@ -3303,6 +3303,7 @@ cprover_function_contract:
           exprt tmp(ID_function_pointer_obeys_contract);
           tmp.add_to_operands(std::move(parser_stack($3)));
           tmp.add_to_operands(std::move(parser_stack($5)));
+          tmp.add_source_location()=parser_stack($$).source_location();
           parser_stack($$).add_to_operands(std::move(tmp));
         }
         | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression ')'
@@ -3312,6 +3313,7 @@ cprover_function_contract:
           exprt tmp(ID_function_pointer_obeys_contract);
           tmp.add_to_operands(std::move(parser_stack($3)));
           tmp.add_to_operands(std::move(parser_stack($5)));
+          tmp.add_source_location()=parser_stack($$).source_location();
           parser_stack($$).add_to_operands(std::move(tmp));
         }
         | cprover_contract_assigns

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, [email protected]
 #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