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
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
include_pattern_filtert::operator()
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name match the regex.
Definition: cover_filter.cpp:50
goal_filterst::operator()
bool operator()(const source_locationt &source_location) const
Applies the filters to the given source location.
Definition: cover_filter.h:123
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:100
goal_filterst::filters
std::vector< std::unique_ptr< goal_filter_baset > > filters
Definition: cover_filter.h:141
include_pattern_filtert::regex_matcher
std::regex regex_matcher
Definition: cover_filter.h:175
function_filterst::operator()
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
goal_filterst::add
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:116
goto_model.h
invariant.h
function_filter_baset::~function_filter_baset
virtual ~function_filter_baset()
Definition: cover_filter.h:32
trivial_functions_filtert::operator()
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
Definition: cover_filter.cpp:67
internal_functions_filtert::operator()
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.
Definition: cover_filter.cpp:20
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:67
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:134
internal_goals_filtert
Filters out goals with source locations considered internal.
Definition: cover_filter.h:193
internal_functions_filtert::internal_functions_filtert
internal_functions_filtert(message_handlert &message_handler)
Definition: cover_filter.h:148
goal_filter_baset::operator()
virtual bool operator()(const source_locationt &) const =0
Returns true if the goal passes the filter criteria.
function_filter_baset
Base class for filtering functions.
Definition: cover_filter.h:24
goal_filter_baset
Base class for filtering goals.
Definition: cover_filter.h:50
message_handlert
Definition: message.h:24
goal_filterst
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:111
include_pattern_filtert::include_pattern_filtert
include_pattern_filtert(message_handlert &message_handler, const std::string &cover_include_pattern)
Definition: cover_filter.h:162
internal_goals_filtert::internal_goals_filtert
internal_goals_filtert(message_handlert &message_handler)
Definition: cover_filter.h:196
internal_functions_filtert
Filters out CPROVER internal functions.
Definition: cover_filter.h:145
include_pattern_filtert
Filters functions that match the provided pattern.
Definition: cover_filter.h:159
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:182
trivial_functions_filtert
Filters out trivial functions.
Definition: cover_filter.h:179
goal_filter_baset::goal_filter_baset
goal_filter_baset(message_handlert &message_handler)
Definition: cover_filter.h:53
messaget::message_handler
message_handlert * message_handler
Definition: message.h:426
function_filterst::filters
std::vector< std::unique_ptr< function_filter_baset > > filters
Definition: cover_filter.h:107
goal_filter_baset::~goal_filter_baset
virtual ~goal_filter_baset()
Definition: cover_filter.h:58
internal_goals_filtert::operator()
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
Definition: cover_filter.cpp:96
function_filter_baset::operator()
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.
function_filter_baset::function_filter_baset
function_filter_baset(message_handlert &message_handler)
Definition: cover_filter.h:27
message.h
function_filterst
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:74
function_filterst::add
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
Definition: cover_filter.h:79
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:43