CBMC
|
Coverage Instrumentation. More...
Go to the source code of this file.
Classes | |
class | cover_instrumenter_baset |
Base class for goto program coverage instrumenters. More... | |
class | cover_instrumenterst |
A collection of instrumenters to be run. More... | |
class | cover_location_instrumentert |
Basic block coverage instrumenter. More... | |
class | cover_branch_instrumentert |
Branch coverage instrumenter. More... | |
class | cover_condition_instrumentert |
Condition coverage instrumenter. More... | |
class | cover_decision_instrumentert |
Decision coverage instrumenter. More... | |
class | cover_mcdc_instrumentert |
MC/DC coverage instrumenter. More... | |
class | cover_path_instrumentert |
Path coverage instrumenter. More... | |
class | cover_assertion_instrumentert |
Assertion coverage instrumenter. More... | |
class | cover_cover_instrumentert |
__CPROVER_cover coverage instrumenter More... | |
class | cover_assume_instrumentert |
Functions | |
void | cover_instrument_end_of_function (const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &) |
Coverage Instrumentation.
Definition in file cover_instrument.h.
void cover_instrument_end_of_function | ( | const irep_idt & | function_id, |
goto_programt & | goto_program, | ||
const cover_instrumenter_baset::assertion_factoryt & | make_assertion | ||
) |
Definition at line 78 of file cover_instrument_other.cpp.