Basic block coverage instrumenter. More...

Inheritance diagram for cover_location_instrumentert:

Collaboration diagram for cover_location_instrumentert:

Public Member Functions
	cover_location_instrumentert (const symbol_table_baset &_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_table_baset &_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 (source_locationt &source_location, 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

Basic block coverage instrumenter.

Definition at line 131 of file cover_instrument.h.

Constructor & Destructor Documentation

cover_location_instrumentert::cover_location_instrumentert	(	const symbol_table_baset &	_symbol_table,
		const goal_filterst &	_goal_filters
	)

inline

Definition at line 134 of file cover_instrument.h.

void cover_location_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.

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