14 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_H
15 #define CPROVER_GOTO_INSTRUMENT_COVER_H
29 "(cover-failed-assertions)" \
33 " --cover CC create test-suite with coverage criterion " \
35 " --cover-failed-assertions do not stop coverage checking at failed " \
37 " (this is the default for --cover " \
39 " --show-test-suite print test suite for coverage criterion " \
40 "(requires --cover)\n"
64 util_make_unique<goal_filterst>();
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.
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.
A collection of goto functions.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void parse_cover_options(const cmdlinet &, optionst &)
Parses coverage-related command line options.
void instrument_cover_goals(const symbol_tablet &, const cover_configt &, goto_functionst &, coverage_criteriont, message_handlert &message_handler)
cover_configt get_cover_config(const optionst &, const symbol_tablet &, message_handlert &)
Build data structures controlling coverage from command-line options.
Filters for the Coverage Instrumentation.
Coverage Instrumentation.
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