MC/DC coverage instrumenter. More...

Inheritance diagram for cover_mcdc_instrumentert:

Collaboration diagram for cover_mcdc_instrumentert:

Public Member Functions
	cover_mcdc_instrumentert (const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)

Public Member Functions inherited from cover_instrumenter_baset
virtual	~cover_instrumenter_baset ()=default

	cover_instrumenter_baset (const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion)

void	operator() (const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks, const assertion_factoryt &make_assertion) const
	Instruments a goto program. More...

Protected Member Functions
void	instrument (const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
	Override this method to implement an instrumenter. More...

Protected Member Functions inherited from cover_instrumenter_baset
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

Additional Inherited Members
Public Types inherited from cover_instrumenter_baset
using	assertion_factoryt = std::function< goto_programt::instructiont(const exprt &, const source_locationt &)>
	The type of function used to make goto_program assertions. More...

Public Attributes inherited from cover_instrumenter_baset
const irep_idt	property_class = "coverage"

const irep_idt	coverage_criterion

Protected Attributes inherited from cover_instrumenter_baset
const namespacet	ns

const goal_filterst &	goal_filters

Detailed Description

MC/DC coverage instrumenter.

Definition at line 212 of file cover_instrument.h.

Constructor & Destructor Documentation

cover_mcdc_instrumentert::cover_mcdc_instrumentert	(	const symbol_tablet &	_symbol_table,
		const goal_filterst &	_goal_filters
	)

inline

Definition at line 215 of file cover_instrument.h.

void cover_mcdc_instrumentert::instrument	(	const irep_idt &	function_id,
		goto_programt &	,
		goto_programt::targett &	,
		const cover_blocks_baset &	,
		const assertion_factoryt &
	)		const

overrideprotectedvirtual

Override this method to implement an instrumenter.

Definition at line 622 of file cover_instrument_mcdc.cpp.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/cover_instrument.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/cover_instrument_mcdc.cpp