cprover
Loading...
Searching...
No Matches
cover_basic_blocks.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: 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 <util/optional.h>
16
18
19#include "source_lines.h"
20
22
24{
25public:
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
46 virtual const source_linest &source_lines_of(std::size_t block_nr) const = 0;
47
49 virtual void output(std::ostream &out) const = 0;
50
56 const irep_idt &function_id,
57 const goto_programt &goto_program,
58 message_handlert &message_handler)
59 {
60 // unused parameters
61 (void)function_id;
62 (void)goto_program;
63 (void)message_handler;
64 }
65};
66
68{
69public:
70 explicit cover_basic_blockst(const goto_programt &goto_program);
71
75 std::size_t block_of(goto_programt::const_targett t) const override;
76
81 instruction_of(std::size_t block_nr) const override;
82
86 const source_locationt &
87 source_location_of(std::size_t block_nr) const override;
88
91 const source_linest &source_lines_of(std::size_t block_nr) const override;
92
98 const irep_idt &function_id,
99 const goto_programt &goto_program,
100 message_handlert &message_handler) override;
101
103 void output(std::ostream &out) const override;
104
105private:
106 typedef std::map<
108 std::size_t,
111
125
129 std::vector<block_infot> block_infos;
130
132 static void add_block_lines(
134 const goto_programt::instructiont &instruction);
135
139 const goto_programt::const_targett &instruction,
141};
142
144{
145private:
146 // map block number to first instruction of the block
147 std::vector<goto_programt::const_targett> block_infos;
148 // map block number to its location
149 std::vector<source_locationt> block_locations;
150 // map java indexes to block indexes
151 std::unordered_map<irep_idt, std::size_t> index_to_block;
152 // map block number to its source lines
153 std::vector<source_linest> block_source_lines;
154
155public:
157
160 std::size_t block_of(goto_programt::const_targett t) const override;
161
165 instruction_of(std::size_t block_number) const override;
166
169 const source_locationt &
170 source_location_of(std::size_t block_number) const override;
171
174 const source_linest &source_lines_of(std::size_t block_number) const override;
175
177 void output(std::ostream &out) const override;
178};
179
180#endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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
const source_linest & source_lines_of(std::size_t block_number) 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
void output(std::ostream &out) const override
Outputs the list of blocks.
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::map< goto_programt::const_targett, std::size_t, goto_programt::target_less_than > block_mapt
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.
const source_linest & source_lines_of(std::size_t block_nr) const override
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 instruction spans to 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 optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
virtual ~cover_blocks_baset()=default
virtual const source_linest & source_lines_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:39
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
Concrete Goto Program.
Set of source code lines contributing to a basic 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
A total order over targett and const_targett.