coverage instrumentation now passes a function identifier

Author: kroening

src/goto-instrument/cover.cpp

@@ -31,6 +31,7 @@ Date: May 2016
 ///        ID_java)
 /// \param message_handler: a message handler
 void instrument_cover_goals(
+  const irep_idt &function,
   goto_programt &goto_program,
   const cover_instrumenterst &instrumenters,
   const irep_idt &mode,
@@ -42,8 +43,8 @@ void instrument_cover_goals(
                     : std::unique_ptr<cover_blocks_baset>(
                         new cover_basic_blockst(goto_program));
 
-  basic_blocks->report_block_anomalies(goto_program, message_handler);
-  instrumenters(goto_program, *basic_blocks);
+  basic_blocks->report_block_anomalies(function, goto_program, message_handler);
+  instrumenters(function, goto_program, *basic_blocks);
 }
 
 /// Instruments goto program for a given coverage criterion
@@ -60,6 +61,7 @@ DEPRECATED(
   "message_handlert &message_handler, const irep_idt mode) instead")
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
+  const irep_idt &function,
   goto_programt &goto_program,
   coverage_criteriont criterion,
   message_handlert &message_handler)
@@ -71,7 +73,7 @@ void instrument_cover_goals(
   instrumenters.add_from_criterion(criterion, symbol_table, goal_filters);
 
   instrument_cover_goals(
-    goto_program, instrumenters, ID_unknown, message_handler);
+    function, goto_program, instrumenters, ID_unknown, message_handler);
 }
 
 /// Create and add an instrumenter based on the given criterion
@@ -283,7 +285,7 @@ static void instrument_cover_goals(
   if(config.function_filters(function_id, function))
   {
     instrument_cover_goals(
-      function.body, config.cover_instrumenters, config.mode, message_handler);
+      function_id, function.body, config.cover_instrumenters, config.mode, message_handler);
     changed = true;
   }
 

src/goto-instrument/cover_basic_blocks.cpp

@@ -109,6 +109,7 @@ cover_basic_blockst::source_location_of(const std::size_t block_nr) const
 }
 
 void cover_basic_blockst::report_block_anomalies(
+  const irep_idt &function,
   const goto_programt &goto_program,
   message_handlert &message_handler)
 {
@@ -133,7 +134,7 @@ void cover_basic_blockst::report_block_anomalies(
       block_info.source_location.is_nil())
     {
       msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
-                    << it->location_number << " " << it->function
+                    << it->location_number << " " << function
                     << " (missing source location)" << messaget::eom;
     }
     // The location numbers printed here are those

src/goto-instrument/cover_basic_blocks.h

@@ -46,6 +46,7 @@ class cover_blocks_baset
   /// \param goto_program The goto program
   /// \param message_handler The message handler
   virtual void report_block_anomalies(
+    const irep_idt &function,
     const goto_programt &goto_program,
     message_handlert &message_handler)
   {
@@ -78,6 +79,7 @@ class cover_basic_blockst final : public cover_blocks_baset
   /// \param goto_program The goto program
   /// \param message_handler The message handler
   void report_block_anomalies(
+    const irep_idt &function,
     const goto_programt &goto_program,
     message_handlert &message_handler) override;
 

src/goto-instrument/cover_instrument.h

@@ -40,12 +40,13 @@ class cover_instrumenter_baset
   /// \param goto_program: a goto program
   /// \param basic_blocks: detected basic blocks
   virtual void operator()(
+    const irep_idt &function,
     goto_programt &goto_program,
     const cover_blocks_baset &basic_blocks) const
   {
     Forall_goto_program_instructions(i_it, goto_program)
     {
-      instrument(goto_program, i_it, basic_blocks);
+      instrument(function, goto_program, i_it, basic_blocks);
     }
   }
 
@@ -58,6 +59,7 @@ class cover_instrumenter_baset
 
   /// Override this method to implement an instrumenter
   virtual void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const = 0;
@@ -94,11 +96,12 @@ class cover_instrumenterst
   /// \param goto_program: a goto program
   /// \param basic_blocks: detected basic blocks of the goto program
   void operator()(
+    const irep_idt &function,
     goto_programt &goto_program,
     const cover_blocks_baset &basic_blocks) const
   {
     for(const auto &instrumenter : instrumenters)
-      (*instrumenter)(goto_program, basic_blocks);
+      (*instrumenter)(function, goto_program, basic_blocks);
   }
 
 private:
@@ -118,6 +121,7 @@ class cover_location_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -136,6 +140,7 @@ class cover_branch_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -154,6 +159,7 @@ class cover_condition_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -172,6 +178,7 @@ class cover_decision_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -190,6 +197,7 @@ class cover_mcdc_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -208,6 +216,7 @@ class cover_path_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -226,6 +235,7 @@ class cover_assertion_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;
@@ -244,6 +254,7 @@ class cover_cover_instrumentert : public cover_instrumenter_baset
 
 protected:
   void instrument(
+    const irep_idt &function,
     goto_programt &,
     goto_programt::targett &,
     const cover_blocks_baset &) const override;

src/goto-instrument/cover_instrument_branch.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening
 #include "cover_basic_blocks.h"
 
 void cover_branch_instrumentert::instrument(
+  const irep_idt &function,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
   const cover_blocks_baset &basic_blocks) const
@@ -31,7 +32,7 @@ void cover_branch_instrumentert::instrument(
     goto_programt::targett t = goto_program.insert_before(i_it);
     t->make_assertion(false_exprt());
     t->source_location = source_location;
-    initialize_source_location(t, comment, i_it->function);
+    initialize_source_location(t, comment, function);
   }
 
   if(
@@ -44,7 +45,6 @@ void cover_branch_instrumentert::instrument(
     std::string false_comment = "block " + b + " branch false";
 
     exprt guard = i_it->guard;
-    const irep_idt function = i_it->function;
     source_locationt source_location = i_it->source_location;
 
     goto_program.insert_before_swap(i_it);

src/goto-instrument/cover_instrument_condition.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include "cover_basic_blocks.h"
 
 void cover_condition_instrumentert::instrument(
+  const irep_idt &function,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
   const cover_blocks_baset &) const
@@ -33,10 +34,9 @@ void cover_condition_instrumentert::instrument(
 
     for(const auto &c : conditions)
     {
-      const std::string c_string = from_expr(ns, i_it->function, c);
+      const std::string c_string = from_expr(ns, function, c);
 
       const std::string comment_t = "condition `" + c_string + "' true";
-      const irep_idt function = i_it->function;
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(c);
       i_it->source_location = source_location;

src/goto-instrument/cover_instrument_decision.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening
 #include "cover_util.h"
 
 void cover_decision_instrumentert::instrument(
+  const irep_idt &function,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
   const cover_blocks_baset &) const
@@ -32,10 +33,9 @@ void cover_decision_instrumentert::instrument(
 
     for(const auto &d : decisions)
     {
-      const std::string d_string = from_expr(ns, i_it->function, d);
+      const std::string d_string = from_expr(ns, function, d);
 
       const std::string comment_t = "decision `" + d_string + "' true";
-      const irep_idt function = i_it->function;
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(d);
       i_it->source_location = source_location;

src/goto-instrument/cover_instrument_location.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening
 #include "cover_filter.h"
 
 void cover_location_instrumentert::instrument(
+  const irep_idt &function,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
   const cover_blocks_baset &basic_blocks) const
@@ -28,14 +29,13 @@ void cover_location_instrumentert::instrument(
   if(representative_instruction && *representative_instruction == i_it)
   {
     const std::string b = std::to_string(block_nr + 1); // start with 1
-    const std::string id = id2string(i_it->function) + "#" + b;
+    const std::string id = id2string(function) + "#" + b;
     const auto source_location = basic_blocks.source_location_of(block_nr);
 
     // filter goals
     if(goal_filters(source_location))
     {
       const std::string comment = "block " + b;
-      const irep_idt function = i_it->function;
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(false_exprt());
       i_it->source_location = source_location;

src/goto-instrument/cover_instrument_mcdc.cpp

@@ -621,6 +621,7 @@ void minimize_mcdc_controlling(
 }
 
 void cover_mcdc_instrumentert::instrument(
+  const irep_idt &function,
   goto_programt &goto_program,
   goto_programt::targett &i_it,
   const cover_blocks_baset &) const
@@ -657,10 +658,9 @@ void cover_mcdc_instrumentert::instrument(
                                   ? "decision/condition"
                                   : is_decision ? "decision" : "condition";
 
-      std::string p_string = from_expr(ns, i_it->function, p);
+      std::string p_string = from_expr(ns, function, p);
 
       std::string comment_t = description + " `" + p_string + "' true";
-      const irep_idt function = i_it->function;
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(not_exprt(p));
       i_it->source_location = source_location;
@@ -693,12 +693,11 @@ void cover_mcdc_instrumentert::instrument(
 
     for(const auto &p : controlling)
     {
-      std::string p_string = from_expr(ns, i_it->function, p);
+      std::string p_string = from_expr(ns, function, p);
 
       std::string description =
         "MC/DC independence condition `" + p_string + "'";
 
-      const irep_idt function = i_it->function;
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(not_exprt(p));
       i_it->source_location = source_location;

src/goto-instrument/cover_instrument_other.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening
 #include "cover_util.h"
 
 void cover_path_instrumentert::instrument(
+  const irep_idt &,
   goto_programt &,
   goto_programt::targett &i_it,
   const cover_blocks_baset &) const
@@ -27,6 +28,7 @@ void cover_path_instrumentert::instrument(
 }
 
 void cover_assertion_instrumentert::instrument(
+  const irep_idt &function,
   goto_programt &,
   goto_programt::targett &i_it,
   const cover_blocks_baset &) const
@@ -36,11 +38,12 @@ void cover_assertion_instrumentert::instrument(
   {
     i_it->guard = false_exprt();
     initialize_source_location(
-      i_it, id2string(i_it->source_location.get_comment()), i_it->function);
+      i_it, id2string(i_it->source_location.get_comment()), function);
   }
 }
 
 void cover_cover_instrumentert::instrument(
+  const irep_idt &function,
   goto_programt &,
   goto_programt::targett &i_it,
   const cover_blocks_baset &) const
@@ -58,11 +61,11 @@ void cover_cover_instrumentert::instrument(
     {
       const exprt c = code_function_call.arguments()[0];
       std::string comment =
-        "condition `" + from_expr(ns, i_it->function, c) + "'";
+        "condition `" + from_expr(ns, function, c) + "'";
       i_it->guard = not_exprt(c);
       i_it->type = ASSERT;
       i_it->code.clear();
-      initialize_source_location(i_it, comment, i_it->function);
+      initialize_source_location(i_it, comment, function);
     }
   }
   else if(is_non_cover_assertion(i_it))