cover_blocks_baset Class Reference

#include <cover_basic_blocks.h>

Inheritance diagram for cover_blocks_baset:

Public Member Functions
virtual	~cover_blocks_baset ()=default
virtual std::size_t	block_of (goto_programt::const_targett t) const =0
virtual std::optional< goto_programt::const_targett >	instruction_of (std::size_t block_nr) const =0
virtual const source_locationt &	source_location_of (std::size_t block_nr) const =0
virtual const source_linest &	source_lines_of (std::size_t block_nr) const =0
virtual void	output (std::ostream &out) const =0
	Outputs the list of blocks.
virtual void	report_block_anomalies (const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler)
	Output warnings about ignored blocks.

Detailed Description

Definition at line 21 of file cover_basic_blocks.h.

Constructor & Destructor Documentation

~cover_blocks_baset()

virtual cover_blocks_baset::~cover_blocks_baset ( )

virtualdefault

Member Function Documentation

block_of()

virtual std::size_t cover_blocks_baset::block_of ( goto_programt::const_targett  t ) const

pure virtual

Parameters

t	a goto instruction

Returns

the block number of the block that the given goto instruction is

Implemented in cover_basic_blockst, and cover_basic_blocks_javat.

instruction_of()

virtual std::optional< goto_programt::const_targett > cover_blocks_baset::instruction_of ( std::size_t  block_nr ) const

pure virtual

Parameters

block_nr

a block number

Returns

the instruction selected for instrumentation representative of the given block

Implemented in cover_basic_blockst, and cover_basic_blocks_javat.

output()

virtual void cover_blocks_baset::output ( std::ostream &  out ) const

pure virtual

Outputs the list of blocks.

Implemented in cover_basic_blockst, and cover_basic_blocks_javat.

report_block_anomalies()

virtual void cover_blocks_baset::report_block_anomalies ( const irep_idt &  function_id, const goto_programt &  goto_program, message_handlert &  message_handler  )

inlinevirtual

Output warnings about ignored blocks.

Parameters

function_id	name of goto_program
goto_program	The goto program
message_handler	The message handler

Reimplemented in cover_basic_blockst.

Definition at line 53 of file cover_basic_blocks.h.

source_lines_of()

virtual const source_linest & cover_blocks_baset::source_lines_of ( std::size_t  block_nr ) const

pure virtual

Parameters

block_nr

a block number

Returns

the source lines of the given block

Implemented in cover_basic_blockst, and cover_basic_blocks_javat.

source_location_of()

virtual const source_locationt & cover_blocks_baset::source_location_of ( std::size_t  block_nr ) const

pure virtual

Parameters

block_nr

a block number

Returns

the source location selected for instrumentation representative of the given block

Implemented in cover_basic_blockst, and cover_basic_blocks_javat.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-instrument/cover_basic_blocks.h