cprover
cover_filter.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
13 #define CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
14 
15 #include <regex>
16 #include <memory>
17 
18 #include <util/invariant.h>
19 #include <util/message.h>
20 #include <util/symbol.h>
21 
23 
26 {
27 public:
30  {
31  }
32 
34  {
35  }
36 
38  virtual bool operator()(
39  const symbolt &identifier,
40  const goto_functionst::goto_functiont &goto_function) const = 0;
41 
44  virtual void report_anomalies() const
45  {
46  // do nothing by default
47  }
48 };
49 
52 {
53 public:
56  {
57  }
58 
60  {
61  }
62 
64  virtual bool operator()(const source_locationt &) const = 0;
65 
68  virtual void report_anomalies() const
69  {
70  // do nothing by default
71  }
72 };
73 
76 {
77 public:
80  void add(std::unique_ptr<function_filter_baset> filter)
81  {
82  filters.push_back(std::move(filter));
83  }
84 
88  bool operator()(
89  const symbolt &identifier,
90  const goto_functionst::goto_functiont &goto_function) const
91  {
92  for(const auto &filter : filters)
93  if(!(*filter)(identifier, goto_function))
94  return false;
95 
96  return true;
97  }
98 
101  void report_anomalies() const
102  {
103  for(const auto &filter : filters)
104  filter->report_anomalies();
105  }
106 
107 private:
108  std::vector<std::unique_ptr<function_filter_baset>> filters;
109 };
110 
113 {
114 public:
117  void add(std::unique_ptr<goal_filter_baset> filter)
118  {
119  filters.push_back(std::move(filter));
120  }
121 
124  bool operator()(const source_locationt &source_location) const
125  {
126  for(const auto &filter : filters)
127  if(!(*filter)(source_location))
128  return false;
129 
130  return true;
131  }
132 
135  void report_anomalies() const
136  {
137  for(const auto &filter : filters)
138  filter->report_anomalies();
139  }
140 
141 private:
142  std::vector<std::unique_ptr<goal_filter_baset>> filters;
143 };
144 
147 {
148 public:
151  {
152  }
153 
154  bool operator()(
155  const symbolt &identifier,
156  const goto_functionst::goto_functiont &goto_function) const override;
157 };
158 
160 {
161 public:
162  explicit file_filtert(
164  const irep_idt &file_id)
166  {
167  }
168 
169  bool operator()(
170  const symbolt &identifier,
171  const goto_functionst::goto_functiont &goto_function) const override;
172 
173 private:
175 };
176 
178 {
179 public:
182  const irep_idt &function_id)
184  {
185  }
186 
187  bool operator()(
188  const symbolt &identifier,
189  const goto_functionst::goto_functiont &goto_function) const override;
190 
191 private:
193 };
194 
197 {
198 public:
201  const std::string &cover_include_pattern)
203  regex_matcher(cover_include_pattern)
204  {
205  }
206 
207  bool operator()(
208  const symbolt &identifier,
209  const goto_functionst::goto_functiont &goto_function) const override;
210 
211 private:
212  std::regex regex_matcher;
213 };
214 
217 {
218 public:
221  {
222  }
223 
224  bool operator()(
225  const symbolt &identifier,
226  const goto_functionst::goto_functiont &goto_function) const override;
227 };
228 
231 {
232 public:
235  {
236  }
237 
238  bool operator()(const source_locationt &) const override;
239 };
240 
241 #endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
function_filter_baset::operator()
virtual bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const =0
Returns true if the function passes the filter criteria.
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goal_filterst::operator()
bool operator()(const source_locationt &source_location) const
Applies the filters to the given source location.
Definition: cover_filter.h:124
single_function_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out all functions except for one particular function given in the constructor.
Definition: cover_filter.cpp:68
function_filterst::report_anomalies
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:101
goal_filterst::filters
std::vector< std::unique_ptr< goal_filter_baset > > filters
Definition: cover_filter.h:142
include_pattern_filtert::regex_matcher
std::regex regex_matcher
Definition: cover_filter.h:212
function_filterst::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const
Applies the filters to the given function.
Definition: cover_filter.h:88
single_function_filtert::function_id
irep_idt function_id
Definition: cover_filter.h:192
invariant.h
goal_filterst::add
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:117
goto_model.h
Symbol Table + CFG.
trivial_functions_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
Definition: cover_filter.cpp:99
single_function_filtert::single_function_filtert
single_function_filtert(message_handlert &message_handler, const irep_idt &function_id)
Definition: cover_filter.h:180
function_filter_baset::~function_filter_baset
virtual ~function_filter_baset()
Definition: cover_filter.h:33
goal_filter_baset::report_anomalies
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:68
goal_filterst::report_anomalies
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:135
internal_goals_filtert
Filters out goals with source locations considered internal.
Definition: cover_filter.h:231
internal_functions_filtert::internal_functions_filtert
internal_functions_filtert(message_handlert &message_handler)
Definition: cover_filter.h:149
single_function_filtert
Definition: cover_filter.h:178
goal_filter_baset::operator()
virtual bool operator()(const source_locationt &) const =0
Returns true if the goal passes the filter criteria.
file_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out all functions except those defined in the file that is given in the constructor.
Definition: cover_filter.cpp:54
function_filter_baset
Base class for filtering functions.
Definition: cover_filter.h:26
goal_filter_baset
Base class for filtering goals.
Definition: cover_filter.h:52
symbol.h
Symbol table entry.
message_handlert
Definition: message.h:28
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:113
include_pattern_filtert::include_pattern_filtert
include_pattern_filtert(message_handlert &message_handler, const std::string &cover_include_pattern)
Definition: cover_filter.h:199
internal_goals_filtert::internal_goals_filtert
internal_goals_filtert(message_handlert &message_handler)
Definition: cover_filter.h:233
internal_functions_filtert
Filters out CPROVER internal functions.
Definition: cover_filter.h:147
include_pattern_filtert
Filters functions that match the provided pattern.
Definition: cover_filter.h:197
file_filtert
Definition: cover_filter.h:160
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
trivial_functions_filtert::trivial_functions_filtert
trivial_functions_filtert(message_handlert &message_handler)
Definition: cover_filter.h:219
trivial_functions_filtert
Filters out trivial functions.
Definition: cover_filter.h:217
goal_filter_baset::goal_filter_baset
goal_filter_baset(message_handlert &message_handler)
Definition: cover_filter.h:54
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
include_pattern_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name matches the regex.
Definition: cover_filter.cpp:80
file_filtert::file_id
irep_idt file_id
Definition: cover_filter.h:174
symbolt
Symbol table entry.
Definition: symbol.h:28
function_filterst::filters
std::vector< std::unique_ptr< function_filter_baset > > filters
Definition: cover_filter.h:108
goal_filter_baset::~goal_filter_baset
virtual ~goal_filter_baset()
Definition: cover_filter.h:59
internal_goals_filtert::operator()
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
Definition: cover_filter.cpp:128
function_filter_baset::function_filter_baset
function_filter_baset(message_handlert &message_handler)
Definition: cover_filter.h:28
file_filtert::file_filtert
file_filtert(message_handlert &message_handler, const irep_idt &file_id)
Definition: cover_filter.h:162
message.h
function_filterst
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:76
internal_functions_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out functions that are not considered provided by the user.
Definition: cover_filter.cpp:22
function_filterst::add
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:80
function_filter_baset::report_anomalies
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:44