Go to the documentation of this file.
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>(
52 function_id, goto_program, message_handler);
53 instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
69 util_make_unique<cover_location_instrumentert>(
74 util_make_unique<cover_branch_instrumentert>(
symbol_table, goal_filters));
78 util_make_unique<cover_decision_instrumentert>(
83 util_make_unique<cover_condition_instrumentert>(
88 util_make_unique<cover_path_instrumentert>(
symbol_table, goal_filters));
92 util_make_unique<cover_mcdc_instrumentert>(
symbol_table, goal_filters));
96 util_make_unique<cover_assertion_instrumentert>(
101 util_make_unique<cover_cover_instrumentert>(
symbol_table, goal_filters));
113 if(criterion_string ==
"assertion" || criterion_string ==
"assertions")
115 else if(criterion_string ==
"path" || criterion_string ==
"paths")
117 else if(criterion_string ==
"branch" || criterion_string ==
"branches")
119 else if(criterion_string ==
"location" || criterion_string ==
"locations")
121 else if(criterion_string ==
"decision" || criterion_string ==
"decisions")
123 else if(criterion_string ==
"condition" || criterion_string ==
"conditions")
125 else if(criterion_string ==
"mcdc")
127 else if(criterion_string ==
"cover")
132 s <<
"unknown coverage criterion " <<
'\'' << criterion_string <<
'\'';
150 "cover-include-pattern", cmdline.
get_value(
"cover-include-pattern"));
151 options.
set_option(
"no-trivial-tests", cmdline.
isset(
"no-trivial-tests"));
153 std::string cover_only = cmdline.
get_value(
"cover-only");
155 if(!cover_only.empty() && cmdline.
isset(
"cover-function-only"))
157 "at most one of --cover-only and --cover-function-only can be used",
161 if(cmdline.
isset(
"cover-function-only"))
165 "cover-traces-must-terminate",
166 cmdline.
isset(
"cover-traces-must-terminate"));
183 cover_config.cover_configt::function_filters;
184 std::unique_ptr<goal_filterst> &goal_filters = cover_config.
goal_filters;
187 function_filters.
add(
188 util_make_unique<internal_functions_filtert>(message_handler));
190 goal_filters->
add(util_make_unique<internal_goals_filtert>(message_handler));
195 for(
const auto &criterion_string : criteria_strings)
208 s <<
"assertion coverage cannot currently be used together with other"
209 <<
"coverage criteria";
213 std::string cover_include_pattern =
215 if(!cover_include_pattern.empty())
217 function_filters.
add(
218 util_make_unique<include_pattern_filtert>(
219 message_handler, cover_include_pattern));
223 function_filters.
add(
224 util_make_unique<trivial_functions_filtert>(message_handler));
248 std::string cover_only = options.
get_option(
"cover-only");
251 if(cover_only ==
"function")
255 message_handler, main_symbol.
name));
257 else if(cover_only ==
"file")
263 else if(!cover_only.empty())
266 s <<
"Argument to --cover-only not recognized: " << cover_only;
280 const symbolt &function_symbol,
289 if(i_it->is_assert())
291 auto successor = std::next(i_it);
293 successor !=
function.body.instructions.end() &&
294 successor->is_assume() &&
295 successor->get_condition() == i_it->get_condition())
297 successor->turn_into_skip();
305 bool changed =
false;
310 msg.
debug() <<
"Instrumenting coverage for function "
313 function_symbol.
name,
316 function_symbol.
mode,
344 const symbolt function_symbol =
345 function.get_symbol_table().lookup_ref(
function.get_function_id());
352 function.compute_location_numbers();
367 msg.
status() <<
"Rewriting existing assertions as assumptions"
374 msg.
error() <<
"cover-traces-must-terminate: invalid entry point ["
383 cover_config, function_symbol, f_it->second, message_handler);
Class that provides messages with a built-in verbosity 'level'.
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Coverage Instrumentation.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
virtual bool isset(char option) const
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &)
std::unique_ptr< goal_filterst > goal_filters
const std::string get_option(const std::string &option) const
mstreamt & status() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
void compute_location_numbers()
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
void add_from_criterion(coverage_criteriont, const symbol_tablet &, const goal_filterst &)
Create and add an instrumenter based on the given criterion.
void set_option(const std::string &option, const bool value)
std::list< std::string > value_listt
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.
function_mapt function_map
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.
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
cover_instrumenterst cover_instrumenters
irep_idt mode
Language mode.
const std::string & id2string(const irep_idt &d)
bool traces_must_terminate
cover_instrumenter_baset::assertion_factoryt make_assertion
std::string get_value(char option) const
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
A collection of goal filters to be applied in conjunction.
virtual void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
#define Forall_goto_functions(it, functions)
::goto_functiont goto_functiont
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
function_filterst function_filters
source_locationt location
Source code location of definition of symbol.
bool get_bool_option(const std::string &option) const
Basic blocks detection for Coverage Instrumentation.
A generic container class for the GOTO intermediate representation of one function.
const irep_idt & get_file() const
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A collection of function filters to be applied in conjunction.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const std::list< std::string > & get_values(const std::string &option) const
symbol_tablet symbol_table
Symbol table.
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
const value_listt & get_list_option(const std::string &option) const
irep_idt name
The unique identifier.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
A collection of instrumenters to be run.