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);
70 symbol_table, goal_filters));
79 symbol_table, goal_filters));
84 symbol_table, goal_filters));
97 symbol_table, goal_filters));
156 "cover-include-pattern", cmdline.
get_value(
"cover-include-pattern"));
157 options.
set_option(
"no-trivial-tests", cmdline.
isset(
"no-trivial-tests"));
163 "at most one of --cover-only and --cover-function-only can be used",
167 if(cmdline.
isset(
"cover-function-only"))
171 "cover-traces-must-terminate",
172 cmdline.
isset(
"cover-traces-must-terminate"));
174 "cover-failed-assertions", cmdline.
isset(
"cover-failed-assertions"));
176 options.
set_option(
"show-test-suite", cmdline.
isset(
"show-test-suite"));
194 std::unique_ptr<goal_filterst> &goal_filters =
cover_config.goal_filters;
220 s <<
"assertion coverage cannot currently be used together with other"
221 <<
"coverage criteria";
229 function_filters.
add(
279 s <<
"Argument to --cover-only not recognized: " <<
cover_only;
302 if(
i_it->is_assert())
306 auto successor = std::next(
i_it);
308 successor != function.body.instructions.end() &&
309 successor->is_assume() &&
310 successor->condition() ==
i_it->condition())
312 successor->turn_into_skip();
315 i_it->turn_into_assume();
319 i_it->turn_into_skip();
325 bool changed =
false;
330 msg.
debug() <<
"Instrumenting coverage for function "
387 msg.
status() <<
"Rewriting existing assertions as assumptions"
394 msg.
error() <<
"cover-traces-must-terminate: invalid entry point ["
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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_table_baset &, 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.
A collection of goal filters to be applied in conjunction.
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
::goto_functiont goto_functiont
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.
const irep_idt & get_function_id()
Get function id.
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
void compute_location_numbers()
Re-number our goto_function.
journalling_symbol_tablet & get_symbol_table()
Get 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
The symbol table base class interface.
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.
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