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() (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 (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) 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 65 of file cover_instrument.h.
References comment(), coverage_criterion, and property_class.
Referenced by cover_location_instrumentert::instrument(), cover_branch_instrumentert::instrument(), cover_condition_instrumentert::instrument(), cover_decision_instrumentert::instrument(), cover_assertion_instrumentert::instrument(), and cover_cover_instrumentert::instrument().
|
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.
Referenced by operator()().
|
inlineprotected |
Definition at line 77 of file cover_instrument.h.
References property_class.
Referenced by cover_location_instrumentert::instrument(), cover_branch_instrumentert::instrument(), cover_condition_instrumentert::instrument(), cover_decision_instrumentert::instrument(), cover_mcdc_instrumentert::instrument(), cover_path_instrumentert::instrument(), cover_assertion_instrumentert::instrument(), and cover_cover_instrumentert::instrument().
|
inlinevirtual |
Instruments a goto program.
goto_program | a goto program |
basic_blocks | detected basic blocks |
Definition at line 42 of file cover_instrument.h.
References Forall_goto_program_instructions, goto_program, and instrument().
const irep_idt cover_instrumenter_baset::coverage_criterion |
Definition at line 53 of file cover_instrument.h.
Referenced by initialize_source_location(), and cover_mcdc_instrumentert::instrument().
|
protected |
Definition at line 57 of file cover_instrument.h.
Referenced by cover_location_instrumentert::instrument().
|
protected |
Definition at line 56 of file cover_instrument.h.
Referenced by cover_condition_instrumentert::instrument(), cover_decision_instrumentert::instrument(), cover_mcdc_instrumentert::instrument(), and cover_cover_instrumentert::instrument().
const irep_idt cover_instrumenter_baset::property_class = "coverage" |
Definition at line 52 of file cover_instrument.h.
Referenced by initialize_source_location(), cover_mcdc_instrumentert::instrument(), and is_non_cover_assertion().