cprover
|
MC/DC coverage instrumenter. More...
#include <cover_instrument.h>
Public Member Functions | |
cover_mcdc_instrumentert (const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters) | |
![]() | |
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... | |
Protected Member Functions | |
void | instrument (goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override |
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 |
Additional Inherited Members | |
![]() | |
const irep_idt | property_class = "coverage" |
const irep_idt | coverage_criterion |
![]() | |
const namespacet | ns |
const goal_filterst & | goal_filters |
MC/DC coverage instrumenter.
Definition at line 181 of file cover_instrument.h.
|
inline |
Definition at line 184 of file cover_instrument.h.
|
overrideprotectedvirtual |
Override this method to implement an instrumenter.
Implements cover_instrumenter_baset.
Definition at line 640 of file cover_instrument_mcdc.cpp.
References collect_conditions(), collect_decisions(), collect_mcdc_controlling_nested(), cover_instrumenter_baset::coverage_criterion, from_expr(), goto_program, goto_programt::insert_before_swap(), INVARIANT, is_condition(), cover_instrumenter_baset::is_non_cover_assertion(), minimize_mcdc_controlling(), cover_instrumenter_baset::ns, cover_instrumenter_baset::property_class, remove_repetition(), and source_locationt::set_comment().