From b8586a6e3327cff94bc43cb6ef21ada8128eb556 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 21 Apr 2017 15:30:08 +0100 Subject: [PATCH] Move coverage arg-parsing into cover.cpp This unifies test-generator's version of coverage instrumentation with cbmc's base version, which should make future changes to the two easier to keep in sync. An upcoming changeset will update the test-generator tool to use this. --- src/goto-instrument/cover.cpp | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index f84fe3d5f3d..33ce83bc2f7 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1769,10 +1769,33 @@ bool instrument_cover_goals( } } + // check existing test goals + coverage_goalst existing_goals; + if(cmdline.isset("existing-coverage")) + { + msg.status() << "Check existing coverage goals" << messaget::eom; + // get file with covered test goals + const std::string coverage=cmdline.get_value("existing-coverage"); + // get a coverage_goalst object + if(coverage_goalst::get_coverage_goals(coverage, msgh, existing_goals)) + { + msg.error() << "get_coverage_goals failed" << messaget::eom; + return true; + } + } + msg.status() << "Instrumenting coverage goals" << messaget::eom; for(const auto &criterion : criteria) - instrument_cover_goals(symbol_table, goto_functions, criterion); + { + instrument_cover_goals( + symbol_table, + goto_functions, + criterion, + existing_goals, + cmdline.isset("cover-function-only"), + cmdline.isset("no-trivial-tests")); + } goto_functions.update(); return false;