45 const std::unique_ptr<cover_blocks_baset> basic_blocks =
46 mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
48 : std::unique_ptr<cover_blocks_baset>(
51 basic_blocks->report_block_anomalies(
52 function_id, goto_program, message_handler);
53 instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
67 case coverage_criteriont::LOCATION:
69 util_make_unique<cover_location_instrumentert>(
70 symbol_table, goal_filters));
72 case coverage_criteriont::BRANCH:
74 util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
76 case coverage_criteriont::DECISION:
78 util_make_unique<cover_decision_instrumentert>(
79 symbol_table, goal_filters));
81 case coverage_criteriont::CONDITION:
83 util_make_unique<cover_condition_instrumentert>(
84 symbol_table, goal_filters));
86 case coverage_criteriont::PATH:
88 util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
90 case coverage_criteriont::MCDC:
92 util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
94 case coverage_criteriont::ASSERTION:
96 util_make_unique<cover_assertion_instrumentert>(
97 symbol_table, goal_filters));
99 case coverage_criteriont::COVER:
101 util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
103 case coverage_criteriont::ASSUME:
105 util_make_unique<cover_assume_instrumentert>(symbol_table, goal_filters));
117 if(criterion_string ==
"assertion" || criterion_string ==
"assertions")
119 else if(criterion_string ==
"path" || criterion_string ==
"paths")
121 else if(criterion_string ==
"branch" || criterion_string ==
"branches")
123 else if(criterion_string ==
"location" || criterion_string ==
"locations")
125 else if(criterion_string ==
"decision" || criterion_string ==
"decisions")
127 else if(criterion_string ==
"condition" || criterion_string ==
"conditions")
129 else if(criterion_string ==
"mcdc")
131 else if(criterion_string ==
"cover")
133 else if(criterion_string ==
"assume")
138 s <<
"unknown coverage criterion " <<
'\'' << criterion_string <<
'\'';
156 "cover-include-pattern", cmdline.
get_value(
"cover-include-pattern"));
157 options.
set_option(
"no-trivial-tests", cmdline.
isset(
"no-trivial-tests"));
159 std::string cover_only = cmdline.
get_value(
"cover-only");
161 if(!cover_only.empty() && cmdline.
isset(
"cover-function-only"))
163 "at most one of --cover-only and --cover-function-only can be used",
167 if(cmdline.
isset(
"cover-function-only"))
171 "cover-traces-must-terminate",
172 cmdline.
isset(
"cover-traces-must-terminate"));
174 "cover-failed-assertions", cmdline.
isset(
"cover-failed-assertions"));
176 options.
set_option(
"show-test-suite", cmdline.
isset(
"show-test-suite"));
193 cover_config.cover_configt::function_filters;
194 std::unique_ptr<goal_filterst> &goal_filters = cover_config.
goal_filters;
197 function_filters.
add(util_make_unique<internal_functions_filtert>());
199 goal_filters->add(util_make_unique<internal_goals_filtert>());
204 for(
const auto &criterion_string : criteria_strings)
220 s <<
"assertion coverage cannot currently be used together with other"
221 <<
"coverage criteria";
225 std::string cover_include_pattern =
227 if(!cover_include_pattern.empty())
229 function_filters.
add(
230 util_make_unique<include_pattern_filtert>(cover_include_pattern));
234 function_filters.
add(util_make_unique<trivial_functions_filtert>());
261 std::string cover_only = options.
get_option(
"cover-only");
264 if(cover_only ==
"function")
268 util_make_unique<single_function_filtert>(main_symbol.
name));
270 else if(cover_only ==
"file")
276 else if(!cover_only.empty())
279 s <<
"Argument to --cover-only not recognized: " << cover_only;
293 const symbolt &function_symbol,
302 if(i_it->is_assert())
306 auto successor = std::next(i_it);
308 successor != function.body.instructions.end() &&
309 successor->is_assume() &&
310 successor->get_condition() == i_it->get_condition())
312 successor->turn_into_skip();
315 i_it->turn_into_assume();
319 i_it->turn_into_skip();
325 bool changed =
false;
330 msg.
debug() <<
"Instrumenting coverage for function "
333 function_symbol.
name,
336 function_symbol.
mode,
364 const symbolt function_symbol =
387 msg.
status() <<
"Rewriting existing assertions as assumptions"
394 msg.
error() <<
"cover-traces-must-terminate: invalid entry point ["
403 cover_config, function_symbol, gf_entry.second, message_handler);
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &option) const
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
A collection of instrumenters to be run.
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
void add_from_criterion(coverage_criteriont, const symbol_tablet &, const goal_filterst &)
Create and add an instrumenter based on the given criterion.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of function filters to be applied in conjunction.
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
A collection of goal filters to be applied in conjunction.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
const irep_idt & get_function_id()
Get function id.
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
void compute_location_numbers()
Re-number our goto_function.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
mstreamt & status() const
bool get_bool_option(const std::string &option) const
void set_option(const std::string &option, const bool value)
const std::string get_option(const std::string &option) const
const value_listt & get_list_option(const std::string &option) const
std::list< std::string > value_listt
const irep_idt & get_file() const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
source_locationt location
Source code location of definition of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
Coverage Instrumentation.
Basic blocks detection for Coverage Instrumentation.
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
bool traces_must_terminate
cover_instrumenterst cover_instrumenters
bool cover_failed_assertions
cover_instrumenter_baset::assertion_factoryt make_assertion
function_filterst function_filters
std::unique_ptr< goal_filterst > goal_filters