cprover
cover_basic_blocks.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
13 #define CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
14 
15 #include <unordered_set>
16 
17 #include <util/message.h>
18 
20 
22 {
23 public:
24  virtual ~cover_blocks_baset() = default;
28  virtual std::size_t block_of(goto_programt::const_targett t) const = 0;
29 
34  instruction_of(std::size_t block_nr) const = 0;
35 
39  virtual const source_locationt &
40  source_location_of(std::size_t block_nr) const = 0;
41 
43  virtual void output(std::ostream &out) const = 0;
44 
48  virtual void report_block_anomalies(
49  const goto_programt &goto_program,
50  message_handlert &message_handler)
51  {
52  // unused parameters
53  (void)goto_program;
54  (void)message_handler;
55  }
56 };
57 
59 {
60 public:
61  explicit cover_basic_blockst(const goto_programt &_goto_program);
62 
66  std::size_t block_of(goto_programt::const_targett t) const override;
67 
72  instruction_of(std::size_t block_nr) const override;
73 
77  const source_locationt &
78  source_location_of(std::size_t block_nr) const override;
79 
84  const goto_programt &goto_program,
85  message_handlert &message_handler) override;
86 
88  void output(std::ostream &out) const override;
89 
90 private:
91  typedef std::map<goto_programt::const_targett, std::size_t> block_mapt;
92 
93  struct block_infot
94  {
97 
102 
104  std::unordered_set<std::size_t> lines;
105  };
106 
110  std::vector<block_infot> block_infos;
111 
114  static void update_covered_lines(block_infot &block_info);
115 
119  const goto_programt::const_targett &instruction,
121 };
122 
124 {
125 private:
126  // map block number to first instruction of the block
127  std::vector<goto_programt::const_targett> block_infos;
128  // map block number to its location
129  std::vector<source_locationt> block_locations;
130  // map java indexes to block indexes
131  std::unordered_map<irep_idt, std::size_t> index_to_block;
132 
133 public:
134  explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
135 
138  std::size_t block_of(goto_programt::const_targett t) const override;
139 
143  instruction_of(std::size_t block_number) const override;
144 
147  const source_locationt &
148  source_location_of(std::size_t block_number) const override;
149 
151  void output(std::ostream &out) const override;
152 };
153 
154 #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
cover_basic_blockst::instruction_of
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:98
cover_basic_blocks_javat::index_to_block
std::unordered_map< irep_idt, std::size_t > index_to_block
Definition: cover_basic_blocks.h:131
cover_blocks_baset::source_location_of
virtual const source_locationt & source_location_of(std::size_t block_nr) const =0
cover_basic_blocks_javat::cover_basic_blocks_javat
cover_basic_blocks_javat(const goto_programt &_goto_program)
Definition: cover_basic_blocks.cpp:164
cover_basic_blockst::block_infot::source_location
source_locationt source_location
the source location representative for this block (we need a separate copy of source locations becaus...
Definition: cover_basic_blocks.h:101
cover_blocks_baset::output
virtual void output(std::ostream &out) const =0
Outputs the list of blocks.
goto_model.h
cover_basic_blockst::cover_basic_blockst
cover_basic_blockst(const goto_programt &_goto_program)
Definition: cover_basic_blocks.cpp:32
cover_basic_blockst::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:90
cover_basic_blocks_javat
Definition: cover_basic_blocks.h:123
cover_basic_blockst::block_map
block_mapt block_map
map program locations to block numbers
Definition: cover_basic_blocks.h:108
cover_blocks_baset::report_block_anomalies
virtual void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
Definition: cover_basic_blocks.h:48
cover_basic_blockst::continuation_of_block
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,...
Definition: cover_basic_blocks.cpp:18
cover_basic_blockst::block_infos
std::vector< block_infot > block_infos
map block numbers to block information
Definition: cover_basic_blocks.h:110
cover_blocks_baset::instruction_of
virtual optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
cover_basic_blockst::source_location_of
const source_locationt & source_location_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:105
cover_blocks_baset
Definition: cover_basic_blocks.h:21
cover_basic_blocks_javat::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:181
cover_basic_blocks_javat::block_locations
std::vector< source_locationt > block_locations
Definition: cover_basic_blocks.h:129
message_handlert
Definition: message.h:24
cover_basic_blocks_javat::block_infos
std::vector< goto_programt::const_targett > block_infos
Definition: cover_basic_blocks.h:127
cover_basic_blockst::report_block_anomalies
void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler) override
Output warnings about ignored blocks.
Definition: cover_basic_blocks.cpp:111
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
source_locationt
Definition: source_location.h:20
cover_basic_blocks_javat::source_location_of
const source_locationt & source_location_of(std::size_t block_number) const override
Definition: cover_basic_blocks.cpp:197
cover_basic_blockst
Definition: cover_basic_blocks.h:58
cover_basic_blocks_javat::instruction_of
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
Definition: cover_basic_blocks.cpp:190
cover_basic_blockst::block_mapt
std::map< goto_programt::const_targett, std::size_t > block_mapt
Definition: cover_basic_blocks.h:91
cover_basic_blockst::block_infot::lines
std::unordered_set< std::size_t > lines
the set of lines belonging to this block
Definition: cover_basic_blocks.h:104
cover_basic_blocks_javat::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:203
cover_basic_blockst::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:144
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
cover_blocks_baset::~cover_blocks_baset
virtual ~cover_blocks_baset()=default
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
message.h
cover_blocks_baset::block_of
virtual std::size_t block_of(goto_programt::const_targett t) const =0
cover_basic_blockst::update_covered_lines
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,...
Definition: cover_basic_blocks.cpp:151
cover_basic_blockst::block_infot::representative_inst
optionalt< goto_programt::const_targett > representative_inst
the program location to instrument for this block
Definition: cover_basic_blocks.h:96
cover_basic_blockst::block_infot
Definition: cover_basic_blocks.h:93