Inheritance diagram for cover_assume_instrumentert:

Collaboration diagram for cover_assume_instrumentert:

Public Member Functions
	cover_assume_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 &, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
	Instrument program to check coverage of assume statements. 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

Definition at line 297 of file cover_instrument.h.

Constructor & Destructor Documentation

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

inline

Definition at line 300 of file cover_instrument.h.

void cover_assume_instrumentert::instrument	(	const irep_idt &	function_id,
		goto_programt &	goto_program,
		goto_programt::targett &	i_it,
		const cover_blocks_baset &	,
		const assertion_factoryt &	make_assertion
	)		const

overrideprotectedvirtual

Instrument program to check coverage of assume statements.

Parameters

function_id	The name of the function under instrumentation.
goto_program	The goto-program (function under instrumentation).
i_it	The current instruction (instruction under instrumentation).
make_assertion	The assertion generator function.

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_assume.cpp