Factorize source location initialization

Author: peterschrammel

src/goto-instrument/cover_instrument.h

@@ -61,6 +61,18 @@ class cover_instrumenter_baset
     goto_programt::targett &,
     const cover_basic_blockst &) const = 0;
 
+  void initialize_source_location(
+    goto_programt::targett t,
+    const std::string &comment,
+    const irep_idt &function) const
+  {
+    t->source_location.set_comment(comment);
+    t->source_location.set(ID_coverage_criterion, coverage_criterion);
+    t->source_location.set_property_class(property_class);
+    t->source_location.set_function(function);
+    t->function = function;
+  }
+
   bool is_non_cover_assertion(goto_programt::const_targett t) const
   {
     return t->is_assert() &&

src/goto-instrument/cover_instrument_branch.cpp

@@ -31,11 +31,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;
-    t->source_location.set_comment(comment);
-    t->source_location.set(ID_coverage_criterion, coverage_criterion);
-    t->source_location.set_property_class(property_class);
-    t->source_location.set_function(i_it->function);
-    t->function = i_it->function;
+    initialize_source_location(t, comment, i_it->function);
   }
 
   if(
@@ -50,23 +46,16 @@ void cover_branch_instrumentert::instrument(
     exprt guard = i_it->guard;
     const irep_idt function = i_it->function;
     source_locationt source_location = i_it->source_location;
-    source_location.set_function(function);
 
     goto_program.insert_before_swap(i_it);
     i_it->make_assertion(not_exprt(guard));
     i_it->source_location = source_location;
-    i_it->source_location.set_comment(true_comment);
-    i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-    i_it->source_location.set_property_class(property_class);
-    i_it->function = function;
+    initialize_source_location(i_it, true_comment, function);
 
     goto_program.insert_before_swap(i_it);
     i_it->make_assertion(guard);
     i_it->source_location = source_location;
-    i_it->source_location.set_comment(false_comment);
-    i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-    i_it->source_location.set_property_class(property_class);
-    i_it->function = function;
+    initialize_source_location(i_it, false_comment, function);
 
     std::advance(i_it, 2);
   }

src/goto-instrument/cover_instrument_condition.cpp

@@ -37,21 +37,13 @@ void cover_condition_instrumentert::instrument(
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(c);
       i_it->source_location = source_location;
-      i_it->source_location.set_comment(comment_t);
-      i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-      i_it->source_location.set_property_class(property_class);
-      i_it->source_location.set_function(function);
-      i_it->function = function;
+      initialize_source_location(i_it, comment_t, function);
 
       const std::string comment_f = "condition `" + c_string + "' false";
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(not_exprt(c));
       i_it->source_location = source_location;
-      i_it->source_location.set_comment(comment_f);
-      i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-      i_it->source_location.set_property_class(property_class);
-      i_it->source_location.set_function(function);
-      i_it->function = function;
+      initialize_source_location(i_it, comment_f, function);
     }
 
     for(std::size_t i = 0; i < conditions.size() * 2; i++)

src/goto-instrument/cover_instrument_decision.cpp

@@ -37,21 +37,13 @@ void cover_decision_instrumentert::instrument(
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(d);
       i_it->source_location = source_location;
-      i_it->source_location.set_comment(comment_t);
-      i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-      i_it->source_location.set_property_class(property_class);
-      i_it->source_location.set_function(function);
-      i_it->function = function;
+      initialize_source_location(i_it, comment_t, function);
 
       const std::string comment_f = "decision `" + d_string + "' false";
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(not_exprt(d));
       i_it->source_location = source_location;
-      i_it->source_location.set_comment(comment_f);
-      i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-      i_it->source_location.set_property_class(property_class);
-      i_it->source_location.set_function(function);
-      i_it->function = function;
+      initialize_source_location(i_it, comment_f, function);
     }
 
     // advance iterator beyond the inserted instructions

src/goto-instrument/cover_instrument_location.cpp

@@ -40,11 +40,7 @@ void cover_location_instrumentert::instrument(
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(false_exprt());
       i_it->source_location = source_location;
-      i_it->source_location.set_comment(comment);
-      i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-      i_it->source_location.set_property_class(property_class);
-      i_it->source_location.set_function(function);
-      i_it->function = function;
+      initialize_source_location(i_it, comment, function);
       i_it++;
     }
   }

src/goto-instrument/cover_instrument_other.cpp

@@ -33,9 +33,8 @@ void cover_assertion_instrumentert::instrument(
   if(is_non_cover_assertion(i_it))
   {
     i_it->guard = false_exprt();
-    i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-    i_it->source_location.set_property_class(property_class);
-    i_it->source_location.set_function(i_it->function);
+    initialize_source_location(
+      i_it, id2string(i_it->source_location.get_comment()), i_it->function);
   }
 }
 
@@ -60,10 +59,7 @@ void cover_cover_instrumentert::instrument(
       i_it->guard = not_exprt(c);
       i_it->type = ASSERT;
       i_it->code.clear();
-      i_it->source_location.set_comment(comment);
-      i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
-      i_it->source_location.set_property_class(property_class);
-      i_it->source_location.set_function(i_it->function);
+      initialize_source_location(i_it, comment, i_it->function);
     }
   }
   else if(is_non_cover_assertion(i_it))