cprover
Public Member Functions | Private Attributes | List of all members
cover_basic_blocks_javat Class Referencefinal

#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
 
optionalt< 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
 
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
 
virtual void report_block_anomalies (const goto_programt &goto_program, message_handlert &message_handler)
 Output warnings about ignored blocks. More...
 

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
 

Detailed Description

Definition at line 123 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 164 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
ta goto instruction
Returns
block number the given goto instruction is part of

Implements cover_blocks_baset.

Definition at line 181 of file cover_basic_blocks.cpp.

◆ instruction_of()

optionalt< goto_programt::const_targett > cover_basic_blocks_javat::instruction_of ( std::size_t  block_number) const
overridevirtual
Parameters
block_numbera block number
Returns
first instruction of the given block

Implements cover_blocks_baset.

Definition at line 190 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 203 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_numbera block number
Returns
source location corresponding to the given block

Implements cover_blocks_baset.

Definition at line 197 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 127 of file cover_basic_blocks.h.

◆ block_locations

std::vector<source_locationt> cover_basic_blocks_javat::block_locations
private

Definition at line 129 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 131 of file cover_basic_blocks.h.

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