check for java bytecode index in the existing coverage

src/goto-instrument/cover.cpp

@@ -64,7 +64,8 @@ class basic_blockst
     format_number_ranget format_lines;
     for(const auto &cover_set : block_line_cover_map)
     {
-      assert(!cover_set.second.empty());
+      INVARIANT(!cover_set.second.empty(),
+        "covered lines set must not be empty");
       std::vector<unsigned>
         line_list{cover_set.second.begin(), cover_set.second.end()};
 
@@ -161,14 +162,20 @@ void coverage_goalst::add_goal(source_locationt goal)
   existing_goals.push_back(goal);
 }
 
-bool coverage_goalst::is_existing_goal(source_locationt source_location) const
+/// compare the value of the current goal to the existing ones
+/// \param source_loc: source location of the current goal
+/// \return true : if the current goal exists false : otherwise
+bool coverage_goalst::is_existing_goal(source_locationt source_loc) const
 {
   for(const auto &existing_loc : existing_goals)
   {
-    if(source_location.get_file()==existing_loc.get_file() &&
-       source_location.get_function()==existing_loc.get_function() &&
-       source_location.get_line()==existing_loc.get_line())
-      return true;
+    if((source_loc.get_file()==existing_loc.get_file()) &&
+       (source_loc.get_function()==existing_loc.get_function()) &&
+       (source_loc.get_line()==existing_loc.get_line()) &&
+       (source_loc.get_java_bytecode_index().empty() ||
+         (source_loc.get_java_bytecode_index()==
+           existing_loc.get_java_bytecode_index())))
+        return true;
   }
   return false;
 }

src/goto-instrument/cover.h

@@ -25,7 +25,7 @@ class coverage_goalst
     message_handlert &message_handler,
     coverage_goalst &goals);
   void add_goal(source_locationt goal);
-  bool is_existing_goal(source_locationt source_location) const;
+  bool is_existing_goal(source_locationt source_loc) const;
 
 private:
   std::vector<source_locationt> existing_goals;