Go to the documentation of this file.
40 const std::unique_ptr<cover_blocks_baset> basic_blocks =
41 mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
43 : std::unique_ptr<cover_blocks_baset>(
47 function_id, goto_program, message_handler);
48 instrumenters(function_id, goto_program, *basic_blocks);
64 util_make_unique<cover_location_instrumentert>(
69 util_make_unique<cover_branch_instrumentert>(
symbol_table, goal_filters));
73 util_make_unique<cover_decision_instrumentert>(
78 util_make_unique<cover_condition_instrumentert>(
83 util_make_unique<cover_path_instrumentert>(
symbol_table, goal_filters));
87 util_make_unique<cover_mcdc_instrumentert>(
symbol_table, goal_filters));
91 util_make_unique<cover_assertion_instrumentert>(
96 util_make_unique<cover_cover_instrumentert>(
symbol_table, goal_filters));
108 if(criterion_string ==
"assertion" || criterion_string ==
"assertions")
110 else if(criterion_string ==
"path" || criterion_string ==
"paths")
112 else if(criterion_string ==
"branch" || criterion_string ==
"branches")
114 else if(criterion_string ==
"location" || criterion_string ==
"locations")
116 else if(criterion_string ==
"decision" || criterion_string ==
"decisions")
118 else if(criterion_string ==
"condition" || criterion_string ==
"conditions")
120 else if(criterion_string ==
"mcdc")
122 else if(criterion_string ==
"cover")
127 s <<
"unknown coverage criterion " <<
'\'' << criterion_string <<
'\'';
145 "cover-include-pattern", cmdline.
get_value(
"cover-include-pattern"));
146 options.
set_option(
"no-trivial-tests", cmdline.
isset(
"no-trivial-tests"));
148 std::string cover_only = cmdline.
get_value(
"cover-only");
150 if(!cover_only.empty() && cmdline.
isset(
"cover-function-only"))
152 "at most one of --cover-only and --cover-function-only can be used",
156 if(cmdline.
isset(
"cover-function-only"))
160 "cover-traces-must-terminate",
161 cmdline.
isset(
"cover-traces-must-terminate"));
178 cover_config.cover_configt::function_filters;
179 std::unique_ptr<goal_filterst> &goal_filters = cover_config.
goal_filters;
182 function_filters.
add(
183 util_make_unique<internal_functions_filtert>(message_handler));
185 goal_filters->
add(util_make_unique<internal_goals_filtert>(message_handler));
190 for(
const auto &criterion_string : criteria_strings)
203 s <<
"assertion coverage cannot currently be used together with other"
204 <<
"coverage criteria";
208 std::string cover_include_pattern =
210 if(!cover_include_pattern.empty())
212 function_filters.
add(
213 util_make_unique<include_pattern_filtert>(
214 message_handler, cover_include_pattern));
218 function_filters.
add(
219 util_make_unique<trivial_functions_filtert>(message_handler));
243 std::string cover_only = options.
get_option(
"cover-only");
246 if(cover_only ==
"function")
250 message_handler, main_symbol.
name));
252 else if(cover_only ==
"file")
258 else if(!cover_only.empty())
261 s <<
"Argument to --cover-only not recognized: " << cover_only;
275 const symbolt &function_symbol,
284 if(i_it->is_assert())
286 auto successor = std::next(i_it);
288 successor !=
function.body.instructions.end() &&
289 successor->is_assume() &&
290 successor->get_condition() == i_it->get_condition())
292 successor->turn_into_skip();
300 bool changed =
false;
305 msg.
debug() <<
"Instrumenting coverage for function "
308 function_symbol.
name,
311 function_symbol.
mode,
337 const symbolt function_symbol =
338 function.get_symbol_table().lookup_ref(
function.get_function_id());
345 function.compute_location_numbers();
360 msg.
status() <<
"Rewriting existing assertions as assumptions"
367 msg.
error() <<
"cover-traces-must-terminate: invalid entry point ["
376 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.
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
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
function_mapt function_map
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)
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.
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
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.
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program)
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
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.