cprover
Loading...
Searching...
No Matches
cover_instrument.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
13#define CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
14
15#include <memory>
16
17#include <util/symbol_table.h>
18
20
21enum class coverage_criteriont;
23class goal_filterst;
24
27{
28public:
29 virtual ~cover_instrumenter_baset() = default;
39
41 using assertion_factoryt = std::function<
43 static_assert(
44 std::is_same<
46 std::function<decltype(goto_programt::make_assertion)>>::value,
47 "`assertion_factoryt` is expected to have the same type as "
48 "`goto_programt::make_assertion`.");
49
57 const irep_idt &function_id,
58 goto_programt &goto_program,
60 const assertion_factoryt &make_assertion) const
61 {
63 {
64 instrument(function_id, goto_program, i_it, basic_blocks, make_assertion);
65 }
66 }
67
68 const irep_idt property_class = "coverage";
70
71protected:
74
76 virtual void instrument(
77 const irep_idt &function_id,
80 const cover_blocks_baset &,
81 const assertion_factoryt &) const = 0;
82
85 const std::string &comment,
86 const irep_idt &function_id) const
87 {
88 t->source_location_nonconst().set_comment(comment);
89 t->source_location_nonconst().set(
91 t->source_location_nonconst().set_property_class(property_class);
92 t->source_location_nonconst().set_function(function_id);
93 }
94
96 {
97 return t->is_assert() &&
98 t->source_location().get_property_class() != property_class;
99 }
100};
101
104{
105public:
108 const symbol_tablet &,
109 const goal_filterst &);
110
118 const irep_idt &function_id,
119 goto_programt &goto_program,
121 const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
122 {
123 for(const auto &instrumenter : instrumenters)
124 (*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
125 }
126
127private:
128 std::vector<std::unique_ptr<cover_instrumenter_baset>> instrumenters;
129};
130
133{
134public:
141
142protected:
143 void instrument(
144 const irep_idt &function_id,
147 const cover_blocks_baset &,
148 const assertion_factoryt &) const override;
149};
150
153{
154public:
161
162protected:
163 void instrument(
164 const irep_idt &function_id,
167 const cover_blocks_baset &,
168 const assertion_factoryt &) const override;
169};
170
173{
174public:
181
182protected:
183 void instrument(
184 const irep_idt &function_id,
187 const cover_blocks_baset &,
188 const assertion_factoryt &) const override;
189};
190
193{
194public:
201
202protected:
203 void instrument(
204 const irep_idt &function_id,
207 const cover_blocks_baset &,
208 const assertion_factoryt &) const override;
209};
210
213{
214public:
221
222protected:
223 void instrument(
224 const irep_idt &function_id,
227 const cover_blocks_baset &,
228 const assertion_factoryt &) const override;
229};
230
233{
234public:
241
242protected:
243 void instrument(
244 const irep_idt &function_id,
247 const cover_blocks_baset &,
248 const assertion_factoryt &) const override;
249};
250
253{
254public:
261
262protected:
263 void instrument(
264 const irep_idt &function_id,
267 const cover_blocks_baset &,
268 const assertion_factoryt &) const override;
269};
270
273{
274public:
281
282protected:
283 void instrument(
284 const irep_idt &function_id,
287 const cover_blocks_baset &,
288 const assertion_factoryt &) const override;
289};
290
292 const irep_idt &function_id,
293 goto_programt &goto_program,
295
296// assume-instructions instrumenter.
298{
299public:
306
307protected:
308 void instrument(
309 const irep_idt &,
312 const cover_blocks_baset &,
313 const assertion_factoryt &) const override;
314};
315
316#endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Assertion coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_assertion_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
cover_assume_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Instrument program to check coverage of assume statements.
Branch coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_branch_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Condition coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_condition_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
__CPROVER_cover coverage instrumenter
cover_cover_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
Decision coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_decision_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Base class for goto program coverage instrumenters.
cover_instrumenter_baset(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion)
virtual void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const =0
Override this method to implement an instrumenter.
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
void operator()(const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks, const assertion_factoryt &make_assertion) const
Instruments a goto program.
const goal_filterst & goal_filters
const irep_idt coverage_criterion
bool is_non_cover_assertion(goto_programt::const_targett t) const
virtual ~cover_instrumenter_baset()=default
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
A collection of instrumenters to be run.
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
void add_from_criterion(coverage_criteriont, const symbol_tablet &, const goal_filterst &)
Create and add an instrumenter based on the given criterion.
Definition cover.cpp:60
void operator()(const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks, const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
Applies all instrumenters to the given goto program.
Basic block coverage instrumenter.
cover_location_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
MC/DC coverage instrumenter.
cover_mcdc_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
Path coverage instrumenter.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
cover_path_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
A collection of goal filters to be applied in conjunction.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table.
coverage_criteriont
Definition cover.h:43
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &)
Concrete Goto Program.
#define Forall_goto_program_instructions(it, program)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Author: Diffblue Ltd.