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>(
58 "use instrument_cover_goals(goto_programt &goto_program," 59 "const cover_instrumenterst &instrumenters," 60 "message_handlert &message_handler, const irep_idt mode) instead")
90 util_make_unique<cover_location_instrumentert>(
95 util_make_unique<cover_branch_instrumentert>(
symbol_table, goal_filters));
99 util_make_unique<cover_decision_instrumentert>(
104 util_make_unique<cover_condition_instrumentert>(
109 util_make_unique<cover_path_instrumentert>(
symbol_table, goal_filters));
113 util_make_unique<cover_mcdc_instrumentert>(
symbol_table, goal_filters));
117 util_make_unique<cover_assertion_instrumentert>(
122 util_make_unique<cover_cover_instrumentert>(
symbol_table, goal_filters));
134 if(criterion_string ==
"assertion" || criterion_string ==
"assertions")
136 else if(criterion_string ==
"path" || criterion_string ==
"paths")
138 else if(criterion_string ==
"branch" || criterion_string ==
"branches")
140 else if(criterion_string ==
"location" || criterion_string ==
"locations")
142 else if(criterion_string ==
"decision" || criterion_string ==
"decisions")
144 else if(criterion_string ==
"condition" || criterion_string ==
"conditions")
146 else if(criterion_string ==
"mcdc")
148 else if(criterion_string ==
"cover")
153 s <<
"unknown coverage criterion " <<
'\'' << criterion_string <<
'\'';
166 std::string cover_include_pattern =
167 cmdline.
get_value(
"cover-include-pattern");
168 if(cmdline.
isset(
"cover-function-only"))
170 std::regex special_characters(
171 "\\.|\\\\|\\*|\\+|\\?|\\{|\\}|\\[|\\]|\\(|\\)|\\^|\\$|\\|");
172 cover_include_pattern =
173 ".*" + std::regex_replace(
config.
main, special_characters,
"\\$&") +
".*";
175 options.
set_option(
"cover-include-pattern", cover_include_pattern);
176 options.
set_option(
"no-trivial-tests", cmdline.
isset(
"no-trivial-tests"));
178 "cover-traces-must-terminate",
179 cmdline.
isset(
"cover-traces-must-terminate"));
193 std::unique_ptr<cover_configt>
config = util_make_unique<cover_configt>();
198 function_filters.add(
205 config->keep_assertions =
false;
206 for(
const auto &criterion_string : criteria_strings)
213 config->keep_assertions =
true;
217 catch(
const std::string &e)
224 if(
config->keep_assertions && criteria_strings.size()>1)
226 msg.
error() <<
"assertion coverage cannot currently be used together with " 232 std::string cover_include_pattern =
234 if(!cover_include_pattern.empty())
236 function_filters.add(
237 util_make_unique<include_pattern_filtert>(
242 function_filters.add(
245 config->traces_must_terminate =
262 if(!
config.keep_assertions)
267 if(i_it->is_assert())
269 auto successor = std::next(i_it);
270 if(successor !=
function.body.instructions.end() &&
271 successor->is_assume() &&
272 successor->guard == i_it->guard)
274 successor->make_skip();
281 bool changed =
false;
283 if(
config.function_filters(function_id,
function))
290 if(
config.traces_must_terminate &&
312 function.get_function_id(),
316 function.compute_location_numbers();
331 msg.
status() <<
"Rewriting existing assertions as assumptions" 334 std::unique_ptr<cover_configt>
config =
339 if(
config->traces_must_terminate &&
342 msg.
error() <<
"cover-traces-must-terminate: invalid entry point [" 355 config->function_filters.report_anomalies();
356 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.
static mstreamt & eom(mstreamt &m)
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.
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
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.
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()
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)
goto_programt coverage_criteriont criterion
goto_programt & goto_program
#define Forall_goto_program_instructions(it, program)
Coverage Instrumentation.
goto_programt coverage_criteriont message_handlert & message_handler
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.
cover_instrumenterst instrumenters
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...