Loading...

Searching...

No Matches

cover_basic_blockst Class Referencefinal

#include <cover_basic_blocks.h>

+ Inheritance diagram for cover_basic_blockst:

[フレーム]

[legend]

+ Collaboration diagram for cover_basic_blockst:

[フレーム]

[legend]

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.

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

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.

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.

Private Attributes

block_mapt block_map

map program locations to block numbers

std::vector< block_infot > block_infos

map block numbers to block information

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 36 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 166 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 97 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 105 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 159 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 125 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 119 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 112 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