Skip to content

Commit b8586a6

Browse files
committed
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.
1 parent 466f629 commit b8586a6

File tree

1 file changed

+24
-1
lines changed

1 file changed

+24
-1
lines changed

src/goto-instrument/cover.cpp

+24-1
Original file line numberDiff line numberDiff line change
@@ -1769,10 +1769,33 @@ bool instrument_cover_goals(
17691769
}
17701770
}
17711771

1772+
// check existing test goals
1773+
coverage_goalst existing_goals;
1774+
if(cmdline.isset("existing-coverage"))
1775+
{
1776+
msg.status() << "Check existing coverage goals" << messaget::eom;
1777+
// get file with covered test goals
1778+
const std::string coverage=cmdline.get_value("existing-coverage");
1779+
// get a coverage_goalst object
1780+
if(coverage_goalst::get_coverage_goals(coverage, msgh, existing_goals))
1781+
{
1782+
msg.error() << "get_coverage_goals failed" << messaget::eom;
1783+
return true;
1784+
}
1785+
}
1786+
17721787
msg.status() << "Instrumenting coverage goals" << messaget::eom;
17731788

17741789
for(const auto &criterion : criteria)
1775-
instrument_cover_goals(symbol_table, goto_functions, criterion);
1790+
{
1791+
instrument_cover_goals(
1792+
symbol_table,
1793+
goto_functions,
1794+
criterion,
1795+
existing_goals,
1796+
cmdline.isset("cover-function-only"),
1797+
cmdline.isset("no-trivial-tests"));
1798+
}
17761799

17771800
goto_functions.update();
17781801
return false;

0 commit comments

Comments
 (0)