diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 258b790a887..33b6ac8d969 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1190,8 +1190,7 @@ 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( @@ -1199,9 +1198,7 @@ void instrument_cover_goals( goto_program, criterion, message_handler, - goals, - function_only, - false); + goals); } /// Call a goto_program trivial unless it has: * Any declarations * At least 2 @@ -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()) @@ -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); @@ -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); @@ -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; @@ -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 @@ -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= @@ -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 conditions=collect_conditions(i_it); @@ -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 decisions=collect_decisions(i_it); @@ -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 conditions=collect_conditions(i_it); const std::set decisions=collect_decisions(i_it); @@ -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) { @@ -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() || @@ -1619,9 +1603,7 @@ void instrument_cover_goals( f_it->second.body, criterion, message_handler, - goals, - function_only, - ignore_trivial); + goals); } } @@ -1629,8 +1611,7 @@ 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; @@ -1640,7 +1621,6 @@ void instrument_cover_goals( criterion, message_handler, goals, - function_only, false, ""); } @@ -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")) @@ -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 diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index a7e0a960726..957dd2476b6 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -49,15 +49,13 @@ 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 &, @@ -65,18 +63,15 @@ void instrument_cover_goals( 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 &,