39 const std::unique_ptr<cover_blocks_baset> basic_blocks =
40 mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
42 : std::unique_ptr<cover_blocks_baset>(
46 instrumenters(goto_program, *basic_blocks);
57 DEPRECATED(
"use instrument_cover_goals(goto_programt &...) instead")
65 goal_filters.
add(util_make_unique<internal_goals_filtert>(message_handler));
71 goto_program, instrumenters, ID_unknown, message_handler);
87 util_make_unique<cover_location_instrumentert>(
92 util_make_unique<cover_branch_instrumentert>(
symbol_table, goal_filters));
96 util_make_unique<cover_decision_instrumentert>(
101 util_make_unique<cover_condition_instrumentert>(
106 util_make_unique<cover_path_instrumentert>(
symbol_table, goal_filters));
110 util_make_unique<cover_mcdc_instrumentert>(
symbol_table, goal_filters));
114 util_make_unique<cover_assertion_instrumentert>(
119 util_make_unique<cover_cover_instrumentert>(
symbol_table, goal_filters));
131 if(criterion_string ==
"assertion" || criterion_string ==
"assertions")
133 else if(criterion_string ==
"path" || criterion_string ==
"paths")
135 else if(criterion_string ==
"branch" || criterion_string ==
"branches")
137 else if(criterion_string ==
"location" || criterion_string ==
"locations")
139 else if(criterion_string ==
"decision" || criterion_string ==
"decisions")
141 else if(criterion_string ==
"condition" || criterion_string ==
"conditions")
143 else if(criterion_string ==
"mcdc")
145 else if(criterion_string ==
"cover")
150 s <<
"unknown coverage criterion " <<
'\'' << criterion_string <<
'\'';
163 std::string cover_include_pattern =
164 cmdline.
get_value(
"cover-include-pattern");
165 if(cmdline.
isset(
"cover-function-only"))
167 std::regex special_characters(
168 "\\.|\\\\|\\*|\\+|\\?|\\{|\\}|\\[|\\]|\\(|\\)|\\^|\\$|\\|");
169 cover_include_pattern =
170 ".*" + std::regex_replace(
config.
main, special_characters,
"\\$&") +
".*";
172 options.
set_option(
"cover-include-pattern", cover_include_pattern);
173 options.
set_option(
"no-trivial-tests", cmdline.
isset(
"no-trivial-tests"));
175 "cover-traces-must-terminate",
176 cmdline.
isset(
"cover-traces-must-terminate"));
190 std::unique_ptr<cover_configt>
config = util_make_unique<cover_configt>();
195 function_filters.add(
196 util_make_unique<internal_functions_filtert>(message_handler));
198 goal_filters.
add(util_make_unique<internal_goals_filtert>(message_handler));
202 config->keep_assertions =
false;
203 for(
const auto &criterion_string : criteria_strings)
210 config->keep_assertions =
true;
214 catch(
const std::string &e)
221 if(
config->keep_assertions && criteria_strings.size()>1)
223 msg.
error() <<
"assertion coverage cannot currently be used together with " 229 std::string cover_include_pattern =
231 if(!cover_include_pattern.empty())
233 function_filters.add(
234 util_make_unique<include_pattern_filtert>(
235 message_handler, cover_include_pattern));
239 function_filters.add(
240 util_make_unique<trivial_functions_filtert>(message_handler));
242 config->traces_must_terminate =
259 if(!
config.keep_assertions)
264 if(i_it->is_assert())
266 auto successor = std::next(i_it);
267 if(successor !=
function.body.instructions.end() &&
268 successor->is_assume() &&
269 successor->guard == i_it->guard)
271 successor->make_skip();
278 bool changed =
false;
280 if(
config.function_filters(function_id,
function))
283 function.body,
config.cover_instrumenters,
config.mode, message_handler);
287 if(
config.traces_must_terminate &&
309 function.get_function_id(),
313 function.compute_location_numbers();
328 msg.
status() <<
"Rewriting existing assertions as assumptions" 331 std::unique_ptr<cover_configt>
config =
336 if(
config->traces_must_terminate &&
339 msg.
error() <<
"cover-traces-must-terminate: invalid entry point [" 348 *
config, f_it->first, f_it->second, message_handler);
352 config->function_filters.report_anomalies();
353 config->goal_filters.report_anomalies();
const std::list< std::string > & get_values(const std::string &option) const
A collection of function filters to be applied in conjunction.
irep_idt mode
Language mode.
std::string get_value(char option) const
function_mapt function_map
const value_listt & get_list_option(const std::string &option) const
symbol_tablet symbol_table
Symbol table.
void cover_instrument_end_of_function(const irep_idt &function, goto_programt &goto_program)
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
Basic blocks detection for Coverage Instrumentation.
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
void compute_location_numbers()
virtual bool isset(char option) const
virtual void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
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.
const std::string get_option(const std::string &option) const
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
bool get_bool_option(const std::string &option) const
std::list< std::string > value_listt
::goto_functiont goto_functiont
coverage_criteriont parse_coverage_criterion(const std::string &criterion_string)
Parses a coverage criterion.
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler)
Applies instrumenters to given goto program.
A generic container class for the GOTO intermediate representation of one function.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
mstreamt & status() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Coverage Instrumentation.
void set_option(const std::string &option, const bool value)
A collection of instrumenters to be run.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
A collection of goal filters to be applied in conjunction.
goto_functionst goto_functions
GOTO functions.
std::unique_ptr< 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 add_from_criterion(coverage_criteriont, const symbol_tablet &, const goal_filterst &)
Create and add an instrumenter based on the given criterion.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...