Base class for goto program coverage instrumenters. More...

#include <cover_instrument.h>

Inheritance diagram for cover_instrumenter_baset:

Collaboration diagram for cover_instrumenter_baset:

Public Types
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 Member Functions
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...

Public Attributes
const irep_idt	property_class = "coverage"

const irep_idt	coverage_criterion

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

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

Protected Attributes
const namespacet	ns

const goal_filterst &	goal_filters

Detailed Description

Base class for goto program coverage instrumenters.

Definition at line 26 of file cover_instrument.h.

Member Typedef Documentation

◆ assertion_factoryt

using cover_instrumenter_baset::assertion_factoryt = std::function< goto_programt::instructiont(const exprt &, const source_locationt &)>

The type of function used to make goto_program assertions.

Definition at line 41 of file cover_instrument.h.

Constructor & Destructor Documentation

◆ ~cover_instrumenter_baset()

virtual cover_instrumenter_baset::~cover_instrumenter_baset ( )

virtualdefault

◆ cover_instrumenter_baset()

cover_instrumenter_baset::cover_instrumenter_baset	(	const symbol_table_baset &	_symbol_table,
		const goal_filterst &	_goal_filters,
		const irep_idt &	_coverage_criterion
	)

inline

Definition at line 30 of file cover_instrument.h.

Member Function Documentation

◆ initialize_source_location()

void cover_instrumenter_baset::initialize_source_location	(	source_locationt &	source_location,
		const std::string &	comment,
		const irep_idt &	function_id
	)		const

inlineprotected

Definition at line 83 of file cover_instrument.h.

◆ instrument()

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

protectedpure virtual

Override this method to implement an instrumenter.

Implemented in cover_cover_instrumentert, cover_assertion_instrumentert, cover_path_instrumentert, cover_mcdc_instrumentert, cover_decision_instrumentert, cover_condition_instrumentert, cover_branch_instrumentert, cover_location_instrumentert, and cover_assume_instrumentert.

◆ is_non_cover_assertion()

bool cover_instrumenter_baset::is_non_cover_assertion ( goto_programt::const_targett t ) const

inlineprotected

Definition at line 94 of file cover_instrument.h.

◆ operator()()

void cover_instrumenter_baset::operator()	(	const irep_idt &	function_id,
		goto_programt &	goto_program,
		const cover_blocks_baset &	basic_blocks,
		const assertion_factoryt &	make_assertion
	)		const

inline

Instruments a goto program.

Parameters

function_id	name of `goto_program`
goto_program	a goto program
basic_blocks	detected basic blocks
make_assertion	A function which makes goto program assertions. This parameter may be used to customise the expressions asserted.

Definition at line 56 of file cover_instrument.h.

Member Data Documentation

◆ coverage_criterion

const irep_idt cover_instrumenter_baset::coverage_criterion

Definition at line 69 of file cover_instrument.h.

◆ goal_filters

const goal_filterst& cover_instrumenter_baset::goal_filters

protected

Definition at line 73 of file cover_instrument.h.

◆ ns

const namespacet cover_instrumenter_baset::ns

protected

Definition at line 72 of file cover_instrument.h.

◆ property_class

const irep_idt cover_instrumenter_baset::property_class = "coverage"

Definition at line 68 of file cover_instrument.h.

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

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

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes