From 913de981ba3237418e5a3b91c3cc29863b1b7994 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 6 Apr 2017 17:03:44 +0100 Subject: [PATCH 1/2] check for java bytecode index in the existing coverage check whether the java bytecode index matches for the existing coverage goals. --- src/goto-instrument/cover.cpp | 16 +++++++++++----- src/goto-instrument/cover.h | 2 +- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index a48e6659f9a..73813fe776c 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -161,14 +161,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; From a63f2bbd067f83e3b845b9e9af2baa4573ac94bc Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Tue, 27 Jun 2017 09:21:10 +0100 Subject: [PATCH 2/2] replaced assertion by invariant in cover.cpp --- src/goto-instrument/cover.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 73813fe776c..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()};