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/message.h>
19 #include <util/invariant.h>
20 
22 
25 {
26 public:
29  {
30  }
31 
33  {
34  }
35 
37  virtual bool operator()(
38  const irep_idt &identifier,
39  const goto_functionst::goto_functiont &goto_function) const = 0;
40 
43  virtual void report_anomalies() const
44  {
45  // do nothing by default
46  }
47 };
48 
51 {
52 public:
55  {
56  }
57 
59  {
60  }
61 
63  virtual bool operator()(const source_locationt &) const = 0;
64 
67  virtual void report_anomalies() const
68  {
69  // do nothing by default
70  }
71 };
72 
75 {
76 public:
79  void add(std::unique_ptr<function_filter_baset> filter)
80  {
81  filters.push_back(std::move(filter));
82  }
83 
87  bool operator()(
88  const irep_idt &identifier,
89  const goto_functionst::goto_functiont &goto_function) const
90  {
91  for(const auto &filter : filters)
92  if(!(*filter)(identifier, goto_function))
93  return false;
94 
95  return true;
96  }
97 
100  void report_anomalies() const
101  {
102  for(const auto &filter : filters)
103  filter->report_anomalies();
104  }
105 
106 private:
107  std::vector<std::unique_ptr<function_filter_baset>> filters;
108 };
109 
112 {
113 public:
116  void add(std::unique_ptr<goal_filter_baset> filter)
117  {
118  filters.push_back(std::move(filter));
119  }
120 
123  bool operator()(const source_locationt &source_location) const
124  {
125  for(const auto &filter : filters)
126  if(!(*filter)(source_location))
127  return false;
128 
129  return true;
130  }
131 
134  void report_anomalies() const
135  {
136  for(const auto &filter : filters)
137  filter->report_anomalies();
138  }
139 
140 private:
141  std::vector<std::unique_ptr<goal_filter_baset>> filters;
142 };
143 
146 {
147 public:
150  {
151  }
152 
153  bool operator()(
154  const irep_idt &identifier,
155  const goto_functionst::goto_functiont &goto_function) const override;
156 };
157 
160 {
161 public:
164  const std::string &cover_include_pattern)
166  regex_matcher(cover_include_pattern)
167  {
168  }
169 
170  bool operator()(
171  const irep_idt &identifier,
172  const goto_functionst::goto_functiont &goto_function) const override;
173 
174 private:
175  std::regex regex_matcher;
176 };
177 
180 {
181 public:
184  {
185  }
186 
187  bool operator()(
188  const irep_idt &identifier,
189  const goto_functionst::goto_functiont &goto_function) const override;
190 };
191 
194 {
195 public:
198  {
199  }
200 
201  bool operator()(const source_locationt &) const override;
202 };
203 
204 #endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
function_filter_baset(message_handlert &message_handler)
Definition: cover_filter.h:27
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:79
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:74
Filters out CPROVER internal functions.
Definition: cover_filter.h:145
include_pattern_filtert(message_handlert &message_handler, const std::string &cover_include_pattern)
Definition: cover_filter.h:162
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const
Applies the filters to the given function.
Definition: cover_filter.h:87
Filters functions that match the provided pattern.
Definition: cover_filter.h:159
trivial_functions_filtert(message_handlert &message_handler)
Definition: cover_filter.h:182
bool operator()(const source_locationt &source_location) const
Applies the filters to the given source location.
Definition: cover_filter.h:123
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:134
virtual ~function_filter_baset()
Definition: cover_filter.h:32
virtual ~goal_filter_baset()
Definition: cover_filter.h:58
Symbol Table + CFG.
Filters out goals with source locations considered internal.
Definition: cover_filter.h:193
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:116
::goto_functiont goto_functiont
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name match the regex.
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
Base class for filtering functions.
Definition: cover_filter.h:24
goal_filter_baset(message_handlert &message_handler)
Definition: cover_filter.h:53
Base class for filtering goals.
Definition: cover_filter.h:50
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
Filters out trivial functions.
Definition: cover_filter.h:179
internal_goals_filtert(message_handlert &message_handler)
Definition: cover_filter.h:196
std::vector< std::unique_ptr< function_filter_baset > > filters
Definition: cover_filter.h:107
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:43
internal_functions_filtert(message_handlert &message_handler)
Definition: cover_filter.h:148
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out functions that are not considered provided by the user.
virtual bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const =0
Returns true if the function passes the filter criteria.
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:100
virtual bool operator()(const source_locationt &) const =0
Returns true if the goal passes the filter criteria.
message_handlert * message_handler
Definition: message.h:426
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:111
std::vector< std::unique_ptr< goal_filter_baset > > filters
Definition: cover_filter.h:141
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Definition: cover_filter.h:67