Loading...

Searching...

No Matches

Public Member Functions | List of all members

cover_blocks_baset Class Referenceabstract

#include <cover_basic_blocks.h>

+ Inheritance diagram for cover_blocks_baset:

[フレーム]

[legend]

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