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);
69 util_make_unique<cover_location_instrumentert>(
70 symbol_table, goal_filters));
74 util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
78 util_make_unique<cover_decision_instrumentert>(
79 symbol_table, goal_filters));
83 util_make_unique<cover_condition_instrumentert>(
84 symbol_table, goal_filters));
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>(
97 symbol_table, goal_filters));
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"));
168 "cover-failed-assertions", cmdline.
isset(
"cover-failed-assertions"));
170 options.
set_option(
"show-test-suite", cmdline.
isset(
"show-test-suite"));
187 cover_config.cover_configt::function_filters;
188 std::unique_ptr<goal_filterst> &goal_filters = cover_config.
goal_filters;
191 function_filters.
add(util_make_unique<internal_functions_filtert>());
193 goal_filters->add(util_make_unique<internal_goals_filtert>());
198 for(
const auto &criterion_string : criteria_strings)
211 s <<
"assertion coverage cannot currently be used together with other"
212 <<
"coverage criteria";
216 std::string cover_include_pattern =
218 if(!cover_include_pattern.empty())
220 function_filters.
add(
221 util_make_unique<include_pattern_filtert>(cover_include_pattern));
225 function_filters.
add(util_make_unique<trivial_functions_filtert>());
252 std::string cover_only = options.
get_option(
"cover-only");
255 if(cover_only ==
"function")
259 util_make_unique<single_function_filtert>(main_symbol.
name));
261 else if(cover_only ==
"file")
267 else if(!cover_only.empty())
270 s <<
"Argument to --cover-only not recognized: " << cover_only;
284 const symbolt &function_symbol,
293 if(i_it->is_assert())
297 auto successor = std::next(i_it);
299 successor !=
function.body.instructions.end() &&
300 successor->is_assume() &&
301 successor->get_condition() == i_it->get_condition())
303 successor->turn_into_skip();
309 i_it->turn_into_skip();
315 bool changed =
false;
320 msg.
debug() <<
"Instrumenting coverage for function "
323 function_symbol.
name,
326 function_symbol.
mode,
354 const symbolt function_symbol =
355 function.get_symbol_table().lookup_ref(
function.get_function_id());
359 function.get_goto_function(),
362 function.compute_location_numbers();
377 msg.
status() <<
"Rewriting existing assertions as assumptions"
384 msg.
error() <<
"cover-traces-must-terminate: invalid entry point ["
393 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.
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