14 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_H
15 #define CPROVER_GOTO_INSTRUMENT_COVER_H
29 "(cover-failed-assertions)" \
33 " {y--cover} {uCC} \t " \
34 "create test-suite with coverage criterion {uCC}, where {uCC} is one of " \
35 "{yassertion}[{ys}], {yassume}[{ys}], {ybranch}[{yes}], " \
36 "{ycondition}[{ys}], {ycover}, {decision}[{ys}], {ylocation}[{ys}], " \
38 " {y--cover-failed-assertions} \t " \
39 "do not stop coverage checking at failed assertions (this is the default " \
40 "for {y--cover} {yassertions})\n" \
41 " {y--show-test-suite} \t " \
42 "print test suite for coverage criterion (requires {y--cover})\n"
66 std::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