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 
18 
19 class message_handlert;
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(
51  {
52  }
53 };
54 
56 {
57 public:
58  explicit cover_basic_blockst(const goto_programt &_goto_program);
59 
63  std::size_t block_of(goto_programt::const_targett t) const override;
64 
69  instruction_of(std::size_t block_nr) const override;
70 
74  const source_locationt &
75  source_location_of(std::size_t block_nr) const override;
76 
83 
85  void output(std::ostream &out) const override;
86 
87 private:
88  typedef std::map<goto_programt::const_targett, std::size_t> block_mapt;
89 
90  struct block_infot
91  {
94 
99 
101  std::unordered_set<std::size_t> lines;
102  };
103 
107  std::vector<block_infot> block_infos;
108 
111  static void update_covered_lines(block_infot &block_info);
112 
116  const goto_programt::const_targett &instruction,
118 };
119 
121 {
122 private:
123  // map block number to first instruction of the block
124  std::vector<goto_programt::const_targett> block_infos;
125  // map block number to its location
126  std::vector<source_locationt> block_locations;
127  // map java indexes to block indexes
128  std::unordered_map<irep_idt, std::size_t> index_to_block;
129 
130 public:
131  explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
132 
135  std::size_t block_of(goto_programt::const_targett t) const override;
136 
140  instruction_of(std::size_t block_number) const override;
141 
144  const source_locationt &
145  source_location_of(std::size_t block_number) const override;
146 
148  void output(std::ostream &out) const override;
149 };
150 
151 #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
const source_locationt & source_location_of(std::size_t block_number) const override
std::unordered_set< std::size_t > lines
the set of lines belonging to this block
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
virtual ~cover_blocks_baset()=default
cover_basic_blockst(const goto_programt &_goto_program)
optionalt< goto_programt::const_targett > representative_inst
the program location to instrument for this block
const source_locationt & source_location_of(std::size_t block_nr) const override
std::vector< goto_programt::const_targett > block_infos
virtual optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
Symbol Table + CFG.
virtual void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
nonstd::optional< T > optionalt
Definition: optional.h:35
instructionst::const_iterator const_targett
Definition: goto_program.h:398
std::unordered_map< irep_idt, std::size_t > index_to_block
source_locationt source_location
the source location representative for this block (we need a separate copy of source locations becaus...
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...
virtual std::size_t block_of(goto_programt::const_targett t) const =0
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::vector< source_locationt > block_locations
virtual void output(std::ostream &out) const =0
Outputs the list of blocks.
void output(std::ostream &out) const override
Outputs the list of blocks.
void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler) override
Output warnings about ignored blocks.
cover_basic_blocks_javat(const goto_programt &_goto_program)
void output(std::ostream &out) const override
Outputs the list of blocks.
goto_programt & goto_program
Definition: cover.cpp:63
block_mapt block_map
map program locations to block numbers
std::size_t block_of(goto_programt::const_targett t) const override
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
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...
std::map< goto_programt::const_targett, std::size_t > block_mapt
std::size_t block_of(goto_programt::const_targett t) const override
std::vector< block_infot > block_infos
map block numbers to block information
virtual const source_locationt & source_location_of(std::size_t block_nr) const =0