cprover
cover_instrument.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: 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 
18 #include <util/message.h>
19 
20 enum class coverage_criteriont;
21 class cover_blocks_baset;
22 class goal_filterst;
23 
26 {
27 public:
28  virtual ~cover_instrumenter_baset() = default;
30  const symbol_tablet &_symbol_table,
31  const goal_filterst &_goal_filters,
32  const irep_idt &_coverage_criterion)
33  : coverage_criterion(_coverage_criterion),
34  ns(_symbol_table),
35  goal_filters(_goal_filters)
36  {
37  }
38 
42  virtual void operator()(
44  const cover_blocks_baset &basic_blocks) const
45  {
47  {
48  instrument(goto_program, i_it, basic_blocks);
49  }
50  }
51 
52  const irep_idt property_class = "coverage";
54 
55 protected:
56  const namespacet ns;
58 
60  virtual void instrument(
61  goto_programt &,
63  const cover_blocks_baset &) const = 0;
64 
67  const std::string &comment,
68  const irep_idt &function) const
69  {
70  t->source_location.set_comment(comment);
71  t->source_location.set(ID_coverage_criterion, coverage_criterion);
72  t->source_location.set_property_class(property_class);
73  t->source_location.set_function(function);
74  t->function = function;
75  }
76 
78  {
79  return t->is_assert() &&
80  t->source_location.get_property_class() != property_class;
81  }
82 };
83 
86 {
87 public:
88  void add_from_criterion(
90  const symbol_tablet &,
91  const goal_filterst &);
92 
96  void operator()(
98  const cover_blocks_baset &basic_blocks) const
99  {
100  for(const auto &instrumenter : instrumenters)
101  (*instrumenter)(goto_program, basic_blocks);
102  }
103 
104 private:
105  std::vector<std::unique_ptr<cover_instrumenter_baset>> instrumenters;
106 };
107 
110 {
111 public:
113  const symbol_tablet &_symbol_table,
114  const goal_filterst &_goal_filters)
115  : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
116  {
117  }
118 
119 protected:
120  void instrument(
121  goto_programt &,
123  const cover_blocks_baset &) const override;
124 };
125 
128 {
129 public:
131  const symbol_tablet &_symbol_table,
132  const goal_filterst &_goal_filters)
133  : cover_instrumenter_baset(_symbol_table, _goal_filters, "branch")
134  {
135  }
136 
137 protected:
138  void instrument(
139  goto_programt &,
141  const cover_blocks_baset &) const override;
142 };
143 
146 {
147 public:
149  const symbol_tablet &_symbol_table,
150  const goal_filterst &_goal_filters)
151  : cover_instrumenter_baset(_symbol_table, _goal_filters, "condition")
152  {
153  }
154 
155 protected:
156  void instrument(
157  goto_programt &,
159  const cover_blocks_baset &) const override;
160 };
161 
164 {
165 public:
167  const symbol_tablet &_symbol_table,
168  const goal_filterst &_goal_filters)
169  : cover_instrumenter_baset(_symbol_table, _goal_filters, "decision")
170  {
171  }
172 
173 protected:
174  void instrument(
175  goto_programt &,
177  const cover_blocks_baset &) const override;
178 };
179 
182 {
183 public:
185  const symbol_tablet &_symbol_table,
186  const goal_filterst &_goal_filters)
187  : cover_instrumenter_baset(_symbol_table, _goal_filters, "MC/DC")
188  {
189  }
190 
191 protected:
192  void instrument(
193  goto_programt &,
195  const cover_blocks_baset &) const override;
196 };
197 
200 {
201 public:
203  const symbol_tablet &_symbol_table,
204  const goal_filterst &_goal_filters)
205  : cover_instrumenter_baset(_symbol_table, _goal_filters, "path")
206  {
207  }
208 
209 protected:
210  void instrument(
211  goto_programt &,
213  const cover_blocks_baset &) const override;
214 };
215 
218 {
219 public:
221  const symbol_tablet &_symbol_table,
222  const goal_filterst &_goal_filters)
223  : cover_instrumenter_baset(_symbol_table, _goal_filters, "assertion")
224  {
225  }
226 
227 protected:
228  void instrument(
229  goto_programt &,
231  const cover_blocks_baset &) const override;
232 };
233 
236 {
237 public:
239  const symbol_tablet &_symbol_table,
240  const goal_filterst &_goal_filters)
241  : cover_instrumenter_baset(_symbol_table, _goal_filters, "cover")
242  {
243  }
244 
245 protected:
246  void instrument(
247  goto_programt &,
249  const cover_blocks_baset &) const override;
250 };
251 
253  const irep_idt &function,
255 
256 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
coverage_criteriont
Definition: cover.h:25
Branch coverage instrumenter.
virtual void operator()(goto_programt &goto_program, const cover_blocks_baset &basic_blocks) const
Instruments a goto program.
cover_instrumenter_baset(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion)
cover_mcdc_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
Basic block coverage instrumenter.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
void cover_instrument_end_of_function(const irep_idt &function, goto_programt &goto_program)
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
virtual ~cover_instrumenter_baset()=default
__CPROVER_cover coverage instrumenter
Symbol Table + CFG.
cover_cover_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
instructionst::iterator targett
Definition: goto_program.h:397
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
cover_condition_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
cover_assertion_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const irep_idt coverage_criterion
Base class for goto program coverage instrumenters.
cover_location_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:33
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
cover_branch_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Assertion coverage instrumenter.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
void operator()(goto_programt &goto_program, const cover_blocks_baset &basic_blocks) const
Applies all instrumenters to the given goto program.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
MC/DC coverage instrumenter.
const irep_idt property_class
cover_decision_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
const goal_filterst & goal_filters
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Decision coverage instrumenter.
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function) const
A collection of instrumenters to be run.
cover_path_instrumentert(const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters)
Path coverage instrumenter.
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:111
Condition coverage instrumenter.
bool is_non_cover_assertion(goto_programt::const_targett t) const
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:81
virtual void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const =0
Override this method to implement an instrumenter.