Skip to content

Commit 3cd2f0b

Browse files
Put interface to cover_blocks in virtual class
This will allow to have two implementations for this functor.
1 parent 8e7f129 commit 3cd2f0b

File tree

1 file changed

+51
-7
lines changed

1 file changed

+51
-7
lines changed

src/goto-instrument/cover_basic_blocks.h

+51-7
Original file line numberDiff line numberDiff line change
@@ -18,44 +18,88 @@ Author: Daniel Kroening
1818

1919
class message_handlert;
2020

21-
class cover_basic_blockst final
21+
class cover_blocks_baset
22+
{
23+
public:
24+
/// \param t a goto instruction
25+
/// \return the block number of the block
26+
/// the given goto instruction is part of
27+
virtual std::size_t block_of(goto_programt::const_targett t) const = 0;
28+
29+
/// \param block_nr a block number
30+
/// \return the instruction selected for
31+
/// instrumentation representative of the given block
32+
virtual optionalt<goto_programt::const_targett>
33+
instruction_of(std::size_t block_nr) const = 0;
34+
35+
/// \param block_nr a block number
36+
/// \return the source location selected for
37+
/// instrumentation representative of the given block
38+
virtual const source_locationt &
39+
source_location_of(std::size_t block_nr) const = 0;
40+
41+
/// Select an instruction to be instrumented for each basic block such that
42+
/// the java bytecode indices for each basic block is unique
43+
/// \param goto_program The goto program
44+
/// \param message_handler The message handler
45+
virtual void select_unique_java_bytecode_indices(
46+
const goto_programt &goto_program,
47+
message_handlert &message_handler)
48+
{
49+
}
50+
51+
/// Outputs the list of blocks
52+
virtual void output(std::ostream &out) const = 0;
53+
54+
/// Output warnings about ignored blocks
55+
/// \param goto_program The goto program
56+
/// \param message_handler The message handler
57+
virtual void report_block_anomalies(
58+
const goto_programt &goto_program,
59+
message_handlert &message_handler)
60+
{
61+
}
62+
};
63+
64+
class cover_basic_blockst final : public cover_blocks_baset
2265
{
2366
public:
2467
explicit cover_basic_blockst(const goto_programt &_goto_program);
2568

2669
/// \param t a goto instruction
2770
/// \return the block number of the block
2871
/// the given goto instruction is part of
29-
std::size_t block_of(goto_programt::const_targett t) const;
72+
std::size_t block_of(goto_programt::const_targett t) const override;
3073

3174
/// \param block_nr a block number
3275
/// \return the instruction selected for
3376
/// instrumentation representative of the given block
3477
optionalt<goto_programt::const_targett>
35-
instruction_of(std::size_t block_nr) const;
78+
instruction_of(std::size_t block_nr) const override;
3679

3780
/// \param block_nr a block number
3881
/// \return the source location selected for
3982
/// instrumentation representative of the given block
40-
const source_locationt &source_location_of(std::size_t block_nr) const;
83+
const source_locationt &
84+
source_location_of(std::size_t block_nr) const override;
4185

4286
/// Select an instruction to be instrumented for each basic block such that
4387
/// the java bytecode indices for each basic block is unique
4488
/// \param goto_program The goto program
4589
/// \param message_handler The message handler
4690
void select_unique_java_bytecode_indices(
4791
const goto_programt &goto_program,
48-
message_handlert &message_handler);
92+
message_handlert &message_handler) override;
4993

5094
/// Output warnings about ignored blocks
5195
/// \param goto_program The goto program
5296
/// \param message_handler The message handler
5397
void report_block_anomalies(
5498
const goto_programt &goto_program,
55-
message_handlert &message_handler);
99+
message_handlert &message_handler) override;
56100

57101
/// Outputs the list of blocks
58-
void output(std::ostream &out) const;
102+
void output(std::ostream &out) const override;
59103

60104
private:
61105
typedef std::map<goto_programt::const_targett, std::size_t> block_mapt;

0 commit comments

Comments
 (0)