cprover
|
Base class for goto program coverage instrumenters. More...
#include <cover_instrument.h>
Public Member Functions | |
virtual | ~cover_instrumenter_baset ()=default |
cover_instrumenter_baset (const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion) | |
virtual void | operator() (const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks) const |
Instruments a goto program. More... | |
Public Attributes | |
const irep_idt | property_class = "coverage" |
const irep_idt | coverage_criterion |
Protected Member Functions | |
virtual void | instrument (const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const =0 |
Override this method to implement an instrumenter. More... | |
void | initialize_source_location (goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const |
bool | is_non_cover_assertion (goto_programt::const_targett t) const |
Protected Attributes | |
const namespacet | ns |
const goal_filterst & | goal_filters |
Base class for goto program coverage instrumenters.
Definition at line 25 of file cover_instrument.h.
|
virtualdefault |
|
inline |
Definition at line 29 of file cover_instrument.h.
|
inlineprotected |
Definition at line 68 of file cover_instrument.h.
|
protectedpure virtual |
Override this method to implement an instrumenter.
Implemented in cover_cover_instrumentert, cover_assertion_instrumentert, cover_path_instrumentert, cover_mcdc_instrumentert, cover_decision_instrumentert, cover_condition_instrumentert, cover_branch_instrumentert, and cover_location_instrumentert.
|
inlineprotected |
Definition at line 79 of file cover_instrument.h.
|
inlinevirtual |
Instruments a goto program.
function_id | name of goto_program |
goto_program | a goto program |
basic_blocks | detected basic blocks |
Definition at line 43 of file cover_instrument.h.
const irep_idt cover_instrumenter_baset::coverage_criterion |
Definition at line 55 of file cover_instrument.h.
|
protected |
Definition at line 59 of file cover_instrument.h.
|
protected |
Definition at line 58 of file cover_instrument.h.
const irep_idt cover_instrumenter_baset::property_class = "coverage" |
Definition at line 54 of file cover_instrument.h.