cprover
cover_basic_blockst Class Referencefinal

#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
 
optionalt< goto_programt::const_targettinstruction_of (std::size_t block_nr) const override
 
const source_locationtsource_location_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 > block_mapt
 

Static Private Member Functions

static void update_covered_lines (block_infot &block_info)
 create list of covered lines as CSV string and set as property of source location of basic block, compress to ranges if applicable More...
 
static void update_source_lines (block_infot &block_info)
 create a string representing source lines and set as a property of source location of basic block More...
 
static optionalt< 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_infotblock_infos
 map block numbers to block information More...
 

Detailed Description

Definition at line 63 of file cover_basic_blocks.h.

Member Typedef Documentation

◆ block_mapt

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

Definition at line 98 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 32 of file cover_basic_blocks.cpp.

Member Function Documentation

◆ block_of()

std::size_t cover_basic_blockst::block_of ( goto_programt::const_targett  t) const
overridevirtual
Parameters
ta goto instruction
Returns
the block number of the block the given goto instruction is part of

Implements cover_blocks_baset.

Definition at line 96 of file cover_basic_blocks.cpp.

◆ continuation_of_block()

optionalt< 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 18 of file cover_basic_blocks.cpp.

◆ instruction_of()

optionalt< goto_programt::const_targett > cover_basic_blockst::instruction_of ( std::size_t  block_nr) const
overridevirtual
Parameters
block_nra block number
Returns
the instruction selected for instrumentation representative of the given block

Implements cover_blocks_baset.

Definition at line 104 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 151 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_idname of goto_program
goto_programThe goto program
message_handlerThe message handler

Reimplemented from cover_blocks_baset.

Definition at line 117 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_nra block number
Returns
the source location selected for instrumentation representative of the given block

Implements cover_blocks_baset.

Definition at line 111 of file cover_basic_blocks.cpp.

◆ update_covered_lines()

void cover_basic_blockst::update_covered_lines ( block_infot block_info)
staticprivate

create list of covered lines as CSV string and set as property of source location of basic block, compress to ranges if applicable

Definition at line 158 of file cover_basic_blocks.cpp.

◆ update_source_lines()

void cover_basic_blockst::update_source_lines ( block_infot block_info)
staticprivate

create a string representing source lines and set as a property of source location of basic block

Definition at line 171 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 120 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 118 of file cover_basic_blocks.h.


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