cover_basic_blocks_javat Class Reference

#include <cover_basic_blocks.h>

Inheritance diagram for cover_basic_blocks_javat:

Collaboration diagram for cover_basic_blocks_javat:

Public Member Functions
	cover_basic_blocks_javat (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_number) const override
const source_locationt &	source_location_of (std::size_t block_number) const override
const source_linest &	source_lines_of (std::size_t block_number) const override
void	output (std::ostream &out) const override
	Outputs the list of blocks.
Public Member Functions inherited from cover_blocks_baset
virtual	~cover_blocks_baset ()=default
virtual void	report_block_anomalies (const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler)
	Output warnings about ignored blocks.

Private Attributes
std::vector< goto_programt::const_targett >	block_infos
std::vector< source_locationt >	block_locations
std::unordered_map< irep_idt, std::size_t >	index_to_block
std::vector< source_linest >	block_source_lines

Detailed Description

Definition at line 141 of file cover_basic_blocks.h.

Constructor & Destructor Documentation

cover_basic_blocks_javat()

cover_basic_blocks_javat::cover_basic_blocks_javat ( const goto_programt &  _goto_program )

explicit

Definition at line 185 of file cover_basic_blocks.cpp.

Member Function Documentation

block_of()

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

overridevirtual

Parameters

t	a goto instruction

Returns

block number the given goto instruction is part of

Implements cover_blocks_baset.

Definition at line 207 of file cover_basic_blocks.cpp.

instruction_of()

std::optional< goto_programt::const_targett > cover_basic_blocks_javat::instruction_of ( std::size_t  block_number ) const

overridevirtual

Parameters

block_number

a block number

Returns

first instruction of the given block

Implements cover_blocks_baset.

Definition at line 216 of file cover_basic_blocks.cpp.

output()

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

overridevirtual

Outputs the list of blocks.

Implements cover_blocks_baset.

Definition at line 236 of file cover_basic_blocks.cpp.

source_lines_of()

const source_linest & cover_basic_blocks_javat::source_lines_of ( std::size_t  block_number ) const

overridevirtual

Parameters

block_number

a block number

Returns

the source lines of the given block

Implements cover_blocks_baset.

Definition at line 230 of file cover_basic_blocks.cpp.

source_location_of()

const source_locationt & cover_basic_blocks_javat::source_location_of ( std::size_t  block_number ) const

overridevirtual

Parameters

block_number

a block number

Returns

source location corresponding to the given block

Implements cover_blocks_baset.

Definition at line 223 of file cover_basic_blocks.cpp.

Member Data Documentation

block_infos

std::vector<goto_programt::const_targett> cover_basic_blocks_javat::block_infos

private

Definition at line 145 of file cover_basic_blocks.h.

block_locations

std::vector<source_locationt> cover_basic_blocks_javat::block_locations

private

Definition at line 147 of file cover_basic_blocks.h.

block_source_lines

std::vector<source_linest> cover_basic_blocks_javat::block_source_lines

private

Definition at line 151 of file cover_basic_blocks.h.

index_to_block

std::unordered_map<irep_idt, std::size_t> cover_basic_blocks_javat::index_to_block

private

Definition at line 149 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