Skip to content

Replace cover-function-only by cover-include-pattern #1348

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

Replace cover-function-only by cover-include-pattern #1348

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 28 additions & 39 deletions src/goto-instrument/cover.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1190,18 +1190,15 @@ void instrument_cover_goals(
const symbol_tablet &symbol_table,
goto_programt &goto_program,
coverage_criteriont criterion,
message_handlert &message_handler,
bool function_only)
message_handlert &message_handler)
{
coverage_goalst goals; // empty already covered goals
instrument_cover_goals(
symbol_table,
goto_program,
criterion,
message_handler,
goals,
function_only,
false);
goals);
}

/// Call a goto_program trivial unless it has: * Any declarations * At least 2
Expand Down Expand Up @@ -1235,14 +1232,8 @@ void instrument_cover_goals(
goto_programt &goto_program,
coverage_criteriont criterion,
message_handlert &message_handler,
coverage_goalst &goals,
bool function_only,
bool ignore_trivial)
coverage_goalst &goals)
{
// exclude trivial coverage goals of a goto program
if(ignore_trivial && program_is_trivial(goto_program))
return;

// ignore if built-in library
if(!goto_program.instructions.empty() &&
goto_program.instructions.front().source_location.is_built_in())
Expand All @@ -1259,19 +1250,11 @@ void instrument_cover_goals(

Forall_goto_program_instructions(i_it, goto_program)
{
std::string curr_function=id2string(i_it->function);

// if the --cover-function-only flag is set, then we only add coverage
// instrumentation for the entry function
bool cover_curr_function=
!function_only ||
curr_function.find(config.main)!=std::string::npos;

switch(criterion)
{
case coverage_criteriont::ASSERTION:
// turn into 'assert(false)' to avoid simplification
if(i_it->is_assert() && cover_curr_function)
if(i_it->is_assert())
{
i_it->guard=false_exprt();
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
Expand All @@ -1282,7 +1265,7 @@ void instrument_cover_goals(

case coverage_criteriont::COVER:
// turn __CPROVER_cover(x) into 'assert(!x)'
if(i_it->is_function_call() && cover_curr_function)
if(i_it->is_function_call())
{
const code_function_callt &code_function_call=
to_code_function_call(i_it->code);
Expand Down Expand Up @@ -1324,8 +1307,7 @@ void instrument_cover_goals(
// check whether the current goal already exists
if(!goals.is_existing_goal(source_location) &&
!source_location.get_file().empty() &&
!source_location.is_built_in() &&
cover_curr_function)
!source_location.is_built_in())
{
std::string comment="block "+b;
const irep_idt function=i_it->function;
Expand All @@ -1348,8 +1330,7 @@ void instrument_cover_goals(
if(i_it->is_assert())
i_it->make_skip();

if(i_it==goto_program.instructions.begin() &&
cover_curr_function)
if(i_it==goto_program.instructions.begin())
{
// we want branch coverage to imply 'entry point of function'
// coverage
Expand All @@ -1367,7 +1348,7 @@ void instrument_cover_goals(
t->function=i_it->function;
}

if(i_it->is_goto() && !i_it->guard.is_true() && cover_curr_function &&
if(i_it->is_goto() && !i_it->guard.is_true() &&
!i_it->source_location.is_built_in())
{
std::string b=
Expand Down Expand Up @@ -1406,7 +1387,7 @@ void instrument_cover_goals(
i_it->make_skip();

// Conditions are all atomic predicates in the programs.
if(cover_curr_function && !i_it->source_location.is_built_in())
if(!i_it->source_location.is_built_in())
{
const std::set<exprt> conditions=collect_conditions(i_it);

Expand Down Expand Up @@ -1448,7 +1429,7 @@ void instrument_cover_goals(
i_it->make_skip();

// Decisions are maximal Boolean combinations of conditions.
if(cover_curr_function && !i_it->source_location.is_built_in())
if(!i_it->source_location.is_built_in())
{
const std::set<exprt> decisions=collect_decisions(i_it);

Expand Down Expand Up @@ -1494,7 +1475,7 @@ void instrument_cover_goals(
// 3. Each condition in a decision takes every possible outcome
// 4. Each condition in a decision is shown to independently
// affect the outcome of the decision.
if(cover_curr_function && !i_it->source_location.is_built_in())
if(!i_it->source_location.is_built_in())
{
const std::set<exprt> conditions=collect_conditions(i_it);
const std::set<exprt> decisions=collect_decisions(i_it);
Expand Down Expand Up @@ -1594,7 +1575,6 @@ void instrument_cover_goals(
coverage_criteriont criterion,
message_handlert &message_handler,
coverage_goalst &goals,
bool function_only,
bool ignore_trivial,
const std::string &cover_include_pattern)
{
Expand All @@ -1604,6 +1584,10 @@ void instrument_cover_goals(

Forall_goto_functions(f_it, goto_functions)
{
// exclude trivial coverage goals of a goto program
if(ignore_trivial && program_is_trivial(f_it->second.body))
return;

if(f_it->first==goto_functions.entry_point() ||
f_it->first==(CPROVER_PREFIX "initialize") ||
f_it->second.is_hidden() ||
Expand All @@ -1619,18 +1603,15 @@ void instrument_cover_goals(
f_it->second.body,
criterion,
message_handler,
goals,
function_only,
ignore_trivial);
goals);
}
}

void instrument_cover_goals(
const symbol_tablet &symbol_table,
goto_functionst &goto_functions,
coverage_criteriont criterion,
message_handlert &message_handler,
bool function_only)
message_handlert &message_handler)
{
// empty set of existing goals
coverage_goalst goals;
Expand All @@ -1640,7 +1621,6 @@ void instrument_cover_goals(
criterion,
message_handler,
goals,
function_only,
false,
"");
}
Expand Down Expand Up @@ -1714,6 +1694,16 @@ bool instrument_cover_goals(
}
}

// cover entry point function only
std::string cover_include_pattern=cmdline.get_value("cover-include-pattern");
if(cmdline.isset("cover-function-only"))
{
std::regex special_characters(
"\\.|\\\\|\\*|\\+|\\?|\\{|\\}|\\[|\\]|\\(|\\)|\\^|\\$|\\|");
cover_include_pattern=
std::regex_replace(config.main, special_characters, "\\$&");
}

// check existing test goals
coverage_goalst existing_goals;
if(cmdline.isset("existing-coverage"))
Expand Down Expand Up @@ -1744,9 +1734,8 @@ bool instrument_cover_goals(
criterion,
message_handler,
existing_goals,
cmdline.isset("cover-function-only"),
cmdline.isset("no-trivial-tests"),
cmdline.get_value("cover-include-pattern"));
cover_include_pattern);
}

// check whether all existing goals match with instrumented goals
Expand Down
13 changes: 4 additions & 9 deletions src/goto-instrument/cover.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,34 +49,29 @@ void instrument_cover_goals(
const symbol_tablet &,
goto_functionst &,
coverage_criteriont,
message_handlert &message_handler,
bool function_only=false);
message_handlert &message_handler);

void instrument_cover_goals(
const symbol_tablet &,
goto_programt &,
coverage_criteriont,
message_handlert &message_handler,
bool function_only=false);
message_handlert &message_handler);

void instrument_cover_goals(
const symbol_tablet &,
goto_functionst &,
coverage_criteriont,
message_handlert &message_handler,
coverage_goalst &,
bool function_only=false,
bool ignore_trivial=false,
const std::string &cover_inclue_pattern="");
const std::string &cover_include_pattern="");

void instrument_cover_goals(
const symbol_tablet &,
goto_programt &,
coverage_criteriont,
message_handlert &message_handler,
coverage_goalst &goals,
bool function_only=false,
bool ignore_trivial=false);
coverage_goalst &goals);

bool instrument_cover_goals(
const cmdlinet &,
Expand Down