diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index a48e6659f9a..a8ba1febf86 100644 --- a/src/goto-instrument/cover.cpp +++ b/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 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; } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 06fc0ede321..20c67b32ee1 100644 --- a/src/goto-instrument/cover.h +++ b/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 existing_goals;