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 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 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 55 of file cover_basic_blocks.h.
|
private |
Definition at line 88 of file cover_basic_blocks.h.
|
explicit |
Definition at line 32 of file cover_basic_blocks.cpp.
References block_infos, block_map, continuation_of_block(), dstringt::empty(), forall_goto_program_instructions, id2string(), INVARIANT, source_locationt::nil(), unsafe_string2unsigned(), and update_covered_lines().
|
overridevirtual |
t | a goto instruction |
Implements cover_blocks_baset.
Definition at line 90 of file cover_basic_blocks.cpp.
References block_map, and INVARIANT.
Referenced by report_block_anomalies().
|
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.
References block_map.
Referenced by cover_basic_blockst().
|
overridevirtual |
block_nr | a block number |
Implements cover_blocks_baset.
Definition at line 98 of file cover_basic_blocks.cpp.
References block_infos, and INVARIANT.
|
overridevirtual |
Outputs the list of blocks.
Implements cover_blocks_baset.
Definition at line 144 of file cover_basic_blocks.cpp.
References block_map.
|
overridevirtual |
Output warnings about ignored blocks.
goto_program | The goto program |
message_handler | The message handler |
Reimplemented from cover_blocks_baset.
Definition at line 111 of file cover_basic_blocks.cpp.
References block_infos, block_of(), messaget::eom(), forall_goto_program_instructions, goto_program, goto_programt::instructions, irept::is_nil(), message_handler, cover_basic_blockst::block_infot::representative_inst, cover_basic_blockst::block_infot::source_location, messaget::mstreamt::source_location, and messaget::warning().
|
overridevirtual |
block_nr | a block number |
Implements cover_blocks_baset.
Definition at line 105 of file cover_basic_blocks.cpp.
References block_infos, and INVARIANT.
|
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 151 of file cover_basic_blocks.cpp.
References format_number_range(), INVARIANT, irept::is_nil(), cover_basic_blockst::block_infot::lines, source_locationt::set_basic_block_covered_lines(), and cover_basic_blockst::block_infot::source_location.
Referenced by cover_basic_blockst().
|
private |
map block numbers to block information
Definition at line 107 of file cover_basic_blocks.h.
Referenced by cover_basic_blockst(), instruction_of(), report_block_anomalies(), and source_location_of().
|
private |
map program locations to block numbers
Definition at line 105 of file cover_basic_blocks.h.
Referenced by block_of(), continuation_of_block(), cover_basic_blockst(), and output().