CBMC
cover_instrument.h File Reference

Coverage Instrumentation. More...

#include <util/namespace.h>
#include <goto-programs/goto_program.h>
#include <memory>
+ Include dependency graph for cover_instrument.h:
+ This graph shows which files directly or indirectly include this file:

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 &)
 

Detailed Description

Coverage Instrumentation.

Definition in file cover_instrument.h.

Function Documentation

◆ cover_instrument_end_of_function()

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.