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/symbol.h>
20 
22 
25 {
26 public:
28  {
29  }
30 
32  virtual bool operator()(
33  const symbolt &identifier,
34  const goto_functionst::goto_functiont &goto_function) const = 0;
35 
38  virtual void report_anomalies() const
39  {
40  // do nothing by default
41  }
42 };
43 
46 {
47 public:
49  {
50  }
51 
53  virtual bool operator()(const source_locationt &) const = 0;
54 
57  virtual void report_anomalies() const
58  {
59  // do nothing by default
60  }
61 };
62 
65 {
66 public:
69  void add(std::unique_ptr<function_filter_baset> filter)
70  {
71  filters.push_back(std::move(filter));
72  }
73 
77  bool operator()(
78  const symbolt &identifier,
79  const goto_functionst::goto_functiont &goto_function) const
80  {
81  for(const auto &filter : filters)
82  if(!(*filter)(identifier, goto_function))
83  return false;
84 
85  return true;
86  }
87 
90  void report_anomalies() const
91  {
92  for(const auto &filter : filters)
93  filter->report_anomalies();
94  }
95 
96 private:
97  std::vector<std::unique_ptr<function_filter_baset>> filters;
98 };
99 
102 {
103 public:
106  void add(std::unique_ptr<goal_filter_baset> filter)
107  {
108  filters.push_back(std::move(filter));
109  }
110 
113  bool operator()(const source_locationt &source_location) const
114  {
115  for(const auto &filter : filters)
116  if(!(*filter)(source_location))
117  return false;
118 
119  return true;
120  }
121 
124  void report_anomalies() const
125  {
126  for(const auto &filter : filters)
127  filter->report_anomalies();
128  }
129 
130 private:
131  std::vector<std::unique_ptr<goal_filter_baset>> filters;
132 };
133 
136 {
137 public:
138  bool operator()(
139  const symbolt &identifier,
140  const goto_functionst::goto_functiont &goto_function) const override;
141 };
142 
144 {
145 public:
147  {
148  }
149 
150  bool operator()(
151  const symbolt &identifier,
152  const goto_functionst::goto_functiont &goto_function) const override;
153 
154 private:
156 };
157 
159 {
160 public:
163  {
164  }
165 
166  bool operator()(
167  const symbolt &identifier,
168  const goto_functionst::goto_functiont &goto_function) const override;
169 
170 private:
172 };
173 
176 {
177 public:
178  explicit include_pattern_filtert(const std::string &cover_include_pattern)
179  : regex_matcher(cover_include_pattern)
180  {
181  }
182 
183  bool operator()(
184  const symbolt &identifier,
185  const goto_functionst::goto_functiont &goto_function) const override;
186 
187 private:
188  std::regex regex_matcher;
189 };
190 
193 {
194 public:
195  bool operator()(
196  const symbolt &identifier,
197  const goto_functionst::goto_functiont &goto_function) const override;
198 };
199 
202 {
203 public:
204  bool operator()(const source_locationt &) const override;
205 };
206 
207 #endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
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:113
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:90
goal_filterst::filters
std::vector< std::unique_ptr< goal_filter_baset > > filters
Definition: cover_filter.h:131
include_pattern_filtert::regex_matcher
std::regex regex_matcher
Definition: cover_filter.h:188
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:77
single_function_filtert::function_id
irep_idt function_id
Definition: cover_filter.h:171
invariant.h
goal_filterst::add
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:106
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(const irep_idt &function_id)
Definition: cover_filter.h:161
function_filter_baset::~function_filter_baset
virtual ~function_filter_baset()
Definition: cover_filter.h:27
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:57
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:124
internal_goals_filtert
Filters out goals with source locations considered internal.
Definition: cover_filter.h:202
single_function_filtert
Definition: cover_filter.h:159
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:25
goal_filter_baset
Base class for filtering goals.
Definition: cover_filter.h:46
symbol.h
Symbol table entry.
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:102
internal_functions_filtert
Filters out CPROVER internal functions.
Definition: cover_filter.h:136
include_pattern_filtert
Filters functions that match the provided pattern.
Definition: cover_filter.h:176
file_filtert
Definition: cover_filter.h:144
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
trivial_functions_filtert
Filters out trivial functions.
Definition: cover_filter.h:193
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:155
symbolt
Symbol table entry.
Definition: symbol.h:28
function_filterst::filters
std::vector< std::unique_ptr< function_filter_baset > > filters
Definition: cover_filter.h:97
goal_filter_baset::~goal_filter_baset
virtual ~goal_filter_baset()
Definition: cover_filter.h:48
internal_goals_filtert::operator()
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
Definition: cover_filter.cpp:128
file_filtert::file_filtert
file_filtert(const irep_idt &file_id)
Definition: cover_filter.h:146
function_filterst
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:65
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:69
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:38
include_pattern_filtert::include_pattern_filtert
include_pattern_filtert(const std::string &cover_include_pattern)
Definition: cover_filter.h:178