cprover
Loading...
Searching...
No Matches
cover_filter.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: 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
19
22{
23public:
25 {
26 }
27
29 virtual bool operator()(
30 const symbolt &identifier,
31 const goto_functionst::goto_functiont &goto_function) const = 0;
32
35 virtual void report_anomalies() const
36 {
37 // do nothing by default
38 }
39};
40
43{
44public:
46 {
47 }
48
50 virtual bool operator()(const source_locationt &) const = 0;
51
54 virtual void report_anomalies() const
55 {
56 // do nothing by default
57 }
58};
59
62{
63public:
66 void add(std::unique_ptr<function_filter_baset> filter)
67 {
68 filters.push_back(std::move(filter));
69 }
70
75 const symbolt &identifier,
76 const goto_functionst::goto_functiont &goto_function) const
77 {
78 for(const auto &filter : filters)
79 if(!(*filter)(identifier, goto_function))
80 return false;
81
82 return true;
83 }
84
87 void report_anomalies() const
88 {
89 for(const auto &filter : filters)
90 filter->report_anomalies();
91 }
92
93private:
94 std::vector<std::unique_ptr<function_filter_baset>> filters;
95};
96
99{
100public:
103 void add(std::unique_ptr<goal_filter_baset> filter)
104 {
105 filters.push_back(std::move(filter));
106 }
107
110 bool operator()(const source_locationt &source_location) const
111 {
112 for(const auto &filter : filters)
113 if(!(*filter)(source_location))
114 return false;
115
116 return true;
117 }
118
121 void report_anomalies() const
122 {
123 for(const auto &filter : filters)
124 filter->report_anomalies();
125 }
126
127private:
128 std::vector<std::unique_ptr<goal_filter_baset>> filters;
129};
130
133{
134public:
135 bool operator()(
136 const symbolt &identifier,
137 const goto_functionst::goto_functiont &goto_function) const override;
138};
139
141{
142public:
144 {
145 }
146
147 bool operator()(
148 const symbolt &identifier,
149 const goto_functionst::goto_functiont &goto_function) const override;
150
151private:
153};
154
156{
157public:
162
163 bool operator()(
164 const symbolt &identifier,
165 const goto_functionst::goto_functiont &goto_function) const override;
166
167private:
169};
170
173{
174public:
179
180 bool operator()(
181 const symbolt &identifier,
182 const goto_functionst::goto_functiont &goto_function) const override;
183
184private:
185 std::regex regex_matcher;
186};
187
190{
191public:
192 bool operator()(
193 const symbolt &identifier,
194 const goto_functionst::goto_functiont &goto_function) const override;
195};
196
199{
200public:
201 bool operator()(const source_locationt &) const override;
202};
203
204#endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
file_filtert(const irep_idt &file_id)
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.
irep_idt file_id
Base class for filtering functions.
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
virtual ~function_filter_baset()
virtual bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const =0
Returns true if the function passes the filter criteria.
A collection of function filters to be applied in conjunction.
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const
Applies the filters to the given function.
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
std::vector< std::unique_ptr< function_filter_baset > > filters
Base class for filtering goals.
virtual bool operator()(const source_locationt &) const =0
Returns true if the goal passes the filter criteria.
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
virtual ~goal_filter_baset()
A collection of goal filters to be applied in conjunction.
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
std::vector< std::unique_ptr< goal_filter_baset > > filters
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
bool operator()(const source_locationt &source_location) const
Applies the filters to the given source location.
::goto_functiont goto_functiont
Filters functions that match the provided pattern.
include_pattern_filtert(const std::string &cover_include_pattern)
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name matches the regex.
Filters out CPROVER internal functions.
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.
Filters out goals with source locations considered internal.
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
single_function_filtert(const irep_idt &function_id)
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.
Symbol table entry.
Definition symbol.h:28
Filters out trivial functions.
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
Goto Programs with Functions.