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 
21 #include "source_lines.h"
22 
24 {
25 public:
26  virtual ~cover_blocks_baset() = default;
29  // part of
30  virtual std::size_t block_of(goto_programt::const_targett t) const = 0;
31 
36  instruction_of(std::size_t block_nr) const = 0;
37 
41  virtual const source_locationt &
42  source_location_of(std::size_t block_nr) const = 0;
43 
45  virtual void output(std::ostream &out) const = 0;
46 
51  virtual void report_block_anomalies(
52  const irep_idt &function_id,
53  const goto_programt &goto_program,
54  message_handlert &message_handler)
55  {
56  // unused parameters
57  (void)function_id;
58  (void)goto_program;
59  (void)message_handler;
60  }
61 };
62 
64 {
65 public:
66  explicit cover_basic_blockst(const goto_programt &goto_program);
67 
71  std::size_t block_of(goto_programt::const_targett t) const override;
72 
77  instruction_of(std::size_t block_nr) const override;
78 
82  const source_locationt &
83  source_location_of(std::size_t block_nr) const override;
84 
90  const irep_idt &function_id,
91  const goto_programt &goto_program,
92  message_handlert &message_handler) override;
93 
95  void output(std::ostream &out) const override;
96 
97 private:
98  typedef std::map<goto_programt::const_targett, std::size_t> block_mapt;
99 
100  struct block_infot
101  {
104 
109 
111  std::unordered_set<std::size_t> lines;
112 
115  };
116 
120  std::vector<block_infot> block_infos;
121 
123  static void add_block_lines(
125  const goto_programt::instructiont &instruction);
126 
129  static void update_covered_lines(block_infot &block_info);
130 
133  static void update_source_lines(block_infot &block_info);
134 
138  const goto_programt::const_targett &instruction,
140 };
141 
143 {
144 private:
145  // map block number to first instruction of the block
146  std::vector<goto_programt::const_targett> block_infos;
147  // map block number to its location
148  std::vector<source_locationt> block_locations;
149  // map java indexes to block indexes
150  std::unordered_map<irep_idt, std::size_t> index_to_block;
151  // map block number to its source lines
152  std::vector<source_linest> block_source_lines;
153 
154 public:
155  explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
156 
159  std::size_t block_of(goto_programt::const_targett t) const override;
160 
164  instruction_of(std::size_t block_number) const override;
165 
168  const source_locationt &
169  source_location_of(std::size_t block_number) const override;
170 
172  void output(std::ostream &out) const override;
173 };
174 
175 #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
cover_basic_blocks_javat(const goto_programt &_goto_program)
std::vector< goto_programt::const_targett > block_infos
const source_locationt & source_location_of(std::size_t block_number) const override
std::vector< source_locationt > block_locations
void output(std::ostream &out) const override
Outputs the list of blocks.
std::size_t block_of(goto_programt::const_targett t) const override
std::vector< source_linest > block_source_lines
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
std::unordered_map< irep_idt, std::size_t > index_to_block
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
std::map< goto_programt::const_targett, std::size_t > block_mapt
void output(std::ostream &out) const override
Outputs the list of blocks.
cover_basic_blockst(const goto_programt &goto_program)
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,...
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
std::vector< block_infot > block_infos
map block numbers to block information
void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler) override
Output warnings about ignored blocks.
std::size_t block_of(goto_programt::const_targett t) const override
static void add_block_lines(cover_basic_blockst::block_infot &block, const goto_programt::instructiont &instruction)
Adds the lines which.
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,...
const source_locationt & source_location_of(std::size_t block_nr) const override
block_mapt block_map
map program locations to block numbers
virtual void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
virtual void output(std::ostream &out) const =0
Outputs the list of blocks.
virtual ~cover_blocks_baset()=default
virtual optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
virtual const source_locationt & source_location_of(std::size_t block_nr) const =0
virtual std::size_t block_of(goto_programt::const_targett t) const =0
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst::const_iterator const_targett
Definition: goto_program.h:551
Symbol Table + CFG.
nonstd::optional< T > optionalt
Definition: optional.h:35
Set of source code lines contributing to a basic block.
std::unordered_set< std::size_t > lines
the set of lines belonging to this block
source_locationt source_location
the source location representative for this block (we need a separate copy of source locations becaus...
source_linest source_lines
the set of source code lines belonging to this block
optionalt< goto_programt::const_targett > representative_inst
the program location to instrument for this block