#include <cover_basic_blocks.h>

Inheritance diagram for cover_basic_blockst:

Collaboration diagram for cover_basic_blockst:

Classes
struct	block_infot

Public Member Functions
	cover_basic_blockst (const goto_programt &goto_program)

std::size_t	block_of (goto_programt::const_targett t) const override

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

const source_locationt &	source_location_of (std::size_t block_nr) const override

const source_linest &	source_lines_of (std::size_t block_nr) const override

void	report_block_anomalies (const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler) override
	Output warnings about ignored blocks. More...

void	output (std::ostream &out) const override
	Outputs the list of blocks. More...

Public Member Functions inherited from cover_blocks_baset
virtual	~cover_blocks_baset ()=default

Private Types
typedef std::map< goto_programt::const_targett, std::size_t, goto_programt::target_less_than >	block_mapt

Static Private Member Functions
static void	add_block_lines (cover_basic_blockst::block_infot &block, const goto_programt::instructiont &instruction)
	Adds the lines which `instruction` spans to `block`. More...

static std::optional< std::size_t >	continuation_of_block (const goto_programt::const_targett &instruction, block_mapt &block_map)
	If this block is a continuation of a previous block through unconditional forward gotos, return this blocks number. More...

Private Attributes
block_mapt	block_map
	map program locations to block numbers More...

std::vector< block_infot >	block_infos
	map block numbers to block information More...

Detailed Description

Definition at line 65 of file cover_basic_blocks.h.

Member Typedef Documentation

◆ block_mapt

typedef std::map< goto_programt::const_targett, std::size_t, goto_programt::target_less_than> cover_basic_blockst::block_mapt

private

Definition at line 108 of file cover_basic_blocks.h.

Constructor & Destructor Documentation

◆ cover_basic_blockst()

cover_basic_blockst::cover_basic_blockst ( const goto_programt & goto_program )

explicit

Definition at line 38 of file cover_basic_blocks.cpp.

Member Function Documentation

◆ add_block_lines()

void cover_basic_blockst::add_block_lines	(	cover_basic_blockst::block_infot &	block,
		const goto_programt::instructiont &	instruction
	)

staticprivate

Adds the lines which instruction spans to block.

Definition at line 168 of file cover_basic_blocks.cpp.

◆ block_of()

std::size_t cover_basic_blockst::block_of ( goto_programt::const_targett t ) const

overridevirtual

Parameters

t	a goto instruction

Returns: the block number of the block the given goto instruction is part of

Implements cover_blocks_baset.

Definition at line 99 of file cover_basic_blocks.cpp.

◆ continuation_of_block()

std::optional< std::size_t > cover_basic_blockst::continuation_of_block	(	const goto_programt::const_targett &	instruction,
		cover_basic_blockst::block_mapt &	block_map
	)

staticprivate

If this block is a continuation of a previous block through unconditional forward gotos, return this blocks number.

Definition at line 16 of file cover_basic_blocks.cpp.

◆ instruction_of()

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

overridevirtual

Parameters

block_nr a block number

Returns: the instruction selected for instrumentation representative of the given block

Implements cover_blocks_baset.

Definition at line 107 of file cover_basic_blocks.cpp.

◆ output()

void cover_basic_blockst::output ( std::ostream & out ) const

overridevirtual

Outputs the list of blocks.

Implements cover_blocks_baset.

Definition at line 161 of file cover_basic_blocks.cpp.

◆ report_block_anomalies()

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

overridevirtual

Output warnings about ignored blocks.

Parameters

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

Reimplemented from cover_blocks_baset.

Definition at line 127 of file cover_basic_blocks.cpp.

◆ source_lines_of()

const source_linest & cover_basic_blockst::source_lines_of ( std::size_t block_nr ) const

overridevirtual

Parameters

block_nr a block number

Returns: the source lines of the given block

Implements cover_blocks_baset.

Definition at line 121 of file cover_basic_blocks.cpp.

◆ source_location_of()

const source_locationt & cover_basic_blockst::source_location_of ( std::size_t block_nr ) const

overridevirtual

Parameters

block_nr a block number

Returns: the source location selected for instrumentation representative of the given block

Implements cover_blocks_baset.

Definition at line 114 of file cover_basic_blocks.cpp.

Member Data Documentation

◆ block_infos

std::vector<block_infot> cover_basic_blockst::block_infos

private

map block numbers to block information

Definition at line 127 of file cover_basic_blocks.h.

◆ block_map

block_mapt cover_basic_blockst::block_map

private

map program locations to block numbers

Definition at line 125 of file cover_basic_blocks.h.

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

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

Classes

Public Member Functions

Private Types

Static Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ block_mapt

Constructor & Destructor Documentation

◆ cover_basic_blockst()

Member Function Documentation

◆ add_block_lines()

◆ block_of()

◆ continuation_of_block()

◆ instruction_of()

◆ output()

◆ report_block_anomalies()

◆ source_lines_of()

◆ source_location_of()

Member Data Documentation

◆ block_infos

◆ block_map