cprover
|
#include <cover_basic_blocks.h>
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_targett > | instruction_of (std::size_t block_nr) const override |
const source_locationt & | source_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... | |
![]() | |
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_infot > | block_infos |
map block numbers to block information More... | |
Definition at line 63 of file cover_basic_blocks.h.
|
private |
Definition at line 98 of file cover_basic_blocks.h.
|
explicit |
Definition at line 32 of file cover_basic_blocks.cpp.
|
overridevirtual |
t | a goto instruction |
Implements cover_blocks_baset.
Definition at line 96 of file cover_basic_blocks.cpp.
|
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.
|
overridevirtual |
block_nr | a block number |
Implements cover_blocks_baset.
Definition at line 104 of file cover_basic_blocks.cpp.
|
overridevirtual |
Outputs the list of blocks.
Implements cover_blocks_baset.
Definition at line 151 of file cover_basic_blocks.cpp.
|
overridevirtual |
Output warnings about ignored blocks.
function_id | name of goto_program |
goto_program | The goto program |
message_handler | The message handler |
Reimplemented from cover_blocks_baset.
Definition at line 117 of file cover_basic_blocks.cpp.
|
overridevirtual |
block_nr | a block number |
Implements cover_blocks_baset.
Definition at line 111 of file cover_basic_blocks.cpp.
|
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.
|
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.
|
private |
map block numbers to block information
Definition at line 120 of file cover_basic_blocks.h.
|
private |
map program locations to block numbers
Definition at line 118 of file cover_basic_blocks.h.