@@ -21,6 +21,21 @@ class message_handlert;
21
21
class cover_basic_blockst
22
22
{
23
23
public:
24
+ struct block_infot
25
+ {
26
+ // / the program location to instrument for this block
27
+ optionalt<goto_programt::const_targett> representative_inst;
28
+
29
+ // / the source location representative for this block
30
+ // (we need a separate copy of source locations because we attach
31
+ // the line number ranges to them)
32
+ source_locationt source_location;
33
+
34
+ // map block numbers to source code locations
35
+ // / the set of lines belonging to this block
36
+ std::unordered_set<unsigned > lines;
37
+ };
38
+
24
39
explicit cover_basic_blockst (const goto_programt &_goto_program);
25
40
26
41
// / \param t a goto instruction
@@ -62,27 +77,9 @@ class cover_basic_blockst
62
77
typedef std::map<goto_programt::const_targett, unsigned > block_mapt;
63
78
block_mapt block_map;
64
79
65
- struct block_infot
66
- {
67
- // / the program location to instrument for this block
68
- optionalt<goto_programt::const_targett> representative_inst;
69
-
70
- // / the source location representative for this block
71
- // (we need a separate copy of source locations because we attach
72
- // the line number ranges to them)
73
- source_locationt source_location;
74
-
75
- // map block numbers to source code locations
76
- // / the set of lines belonging to this block
77
- std::unordered_set<unsigned > lines;
78
- };
79
-
80
80
typedef std::vector<block_infot> block_infost;
81
81
block_infost block_infos;
82
82
83
- // / create list of covered lines as CSV string and set as property of source
84
- // / location of basic block, compress to ranges if applicable
85
- void update_covered_lines (block_infot &block_info);
86
83
};
87
84
88
85
#endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
0 commit comments