Go to the documentation of this file.
14 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_H
15 #define CPROVER_GOTO_INSTRUMENT_COVER_H
45 util_make_unique<goal_filterst>();
92 #endif // CPROVER_GOTO_INSTRUMENT_COVER_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
cover_configt get_cover_config(const optionst &, const symbol_tablet &, message_handlert &)
Build data structures controlling coverage from command-line options.
std::unique_ptr< goal_filterst > goal_filters
void parse_cover_options(const cmdlinet &, optionst &)
Parses coverage-related command line options.
cover_instrumenterst cover_instrumenters
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void instrument_cover_goals(const symbol_tablet &, const cover_configt &, goto_functionst &, coverage_criteriont, message_handlert &message_handler)
bool traces_must_terminate
cover_instrumenter_baset::assertion_factoryt make_assertion
Coverage Instrumentation.
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 goto functions.
function_filterst function_filters
A generic container class for the GOTO intermediate representation of one function.
A collection of function filters to be applied in conjunction.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Filters for the Coverage Instrumentation.
A collection of instrumenters to be run.