Skip to content

Commit fa35ccd

Browse files
Pull continuation_of_block function out
We pull this function out of the cover_basic_blockst constructor, as the constructor is rather long, and having a function for this part of the code makes it clearer.
1 parent 560d712 commit fa35ccd

File tree

2 files changed

+24
-16
lines changed

2 files changed

+24
-16
lines changed

src/goto-instrument/cover_basic_blocks.cpp

+18-16
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,20 @@ Author: Peter Schrammel
1515
#include <util/message.h>
1616
#include <util/string2int.h>
1717

18+
optionalt<unsigned> cover_basic_blockst::continuation_of_block(
19+
const goto_programt::const_targett &instruction,
20+
cover_basic_blockst::block_mapt &block_map)
21+
{
22+
if(instruction->incoming_edges.size() != 1)
23+
return {};
24+
25+
const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
26+
if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true())
27+
return block_map[in_t];
28+
29+
return {};
30+
}
31+
1832
cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
1933
{
2034
bool next_is_target = true;
@@ -25,25 +39,13 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
2539
// Is it a potential beginning of a block?
2640
if(next_is_target || it->is_target())
2741
{
28-
// We keep the block number if this potential block
29-
// is a continuation of a previous block through
30-
// unconditional forward gotos; otherwise we increase the
31-
// block number.
32-
bool increase_block_nr = true;
33-
if(it->incoming_edges.size() == 1)
42+
if(auto block_number = continuation_of_block(it, block_map))
3443
{
35-
goto_programt::targett in_t = *it->incoming_edges.begin();
36-
if(
37-
in_t->is_goto() && !in_t->is_backwards_goto() &&
38-
in_t->guard.is_true())
39-
{
40-
current_block = block_map[in_t];
41-
increase_block_nr = false;
42-
}
44+
current_block = *block_number;
4345
}
44-
if(increase_block_nr)
46+
else
4547
{
46-
block_infos.push_back(block_infot());
48+
block_infos.emplace_back();
4749
block_infos.back().representative_inst = it;
4850
block_infos.back().source_location = source_locationt::nil();
4951
current_block = block_infos.size() - 1;

src/goto-instrument/cover_basic_blocks.h

+6
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,12 @@ class cover_basic_blockst
8383
/// create list of covered lines as CSV string and set as property of source
8484
/// location of basic block, compress to ranges if applicable
8585
static void update_covered_lines(block_infot &block_info);
86+
87+
/// If this block is a continuation of a previous block through unconditional
88+
/// forward gotos, return this blocks number.
89+
static optionalt<unsigned> continuation_of_block(
90+
const goto_programt::const_targett &instruction,
91+
block_mapt &block_map);
8692
};
8793

8894
#endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H

0 commit comments

Comments
 (0)