CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
20class symbolt;
21
24{
25public:
27 {
28 }
29
31 virtual bool operator()(
32 const symbolt &identifier,
33 const goto_functionst::goto_functiont &goto_function) const = 0;
34
37 virtual void report_anomalies() const
38 {
39 // do nothing by default
40 }
41};
42
45{
46public:
48 {
49 }
50
52 virtual bool operator()(const source_locationt &) const = 0;
53
56 virtual void report_anomalies() const
57 {
58 // do nothing by default
59 }
60};
61
64{
65public:
68 void add(std::unique_ptr<function_filter_baset> filter)
69 {
70 filters.push_back(std::move(filter));
71 }
72
77 const symbolt &identifier,
78 const goto_functionst::goto_functiont &goto_function) const
79 {
80 for(const auto &filter : filters)
81 if(!(*filter)(identifier, goto_function))
82 return false;
83
84 return true;
85 }
86
89 void report_anomalies() const
90 {
91 for(const auto &filter : filters)
92 filter->report_anomalies();
93 }
94
95private:
96 std::vector<std::unique_ptr<function_filter_baset>> filters;
97};
98
101{
102public:
105 void add(std::unique_ptr<goal_filter_baset> filter)
106 {
107 filters.push_back(std::move(filter));
108 }
109
112 bool operator()(const source_locationt &source_location) const
113 {
114 for(const auto &filter : filters)
115 if(!(*filter)(source_location))
116 return false;
117
118 return true;
119 }
120
123 void report_anomalies() const
124 {
125 for(const auto &filter : filters)
126 filter->report_anomalies();
127 }
128
129private:
130 std::vector<std::unique_ptr<goal_filter_baset>> filters;
131};
132
135{
136public:
137 bool operator()(
138 const symbolt &identifier,
139 const goto_functionst::goto_functiont &goto_function) const override;
140};
141
143{
144public:
146 {
147 }
148
149 bool operator()(
150 const symbolt &identifier,
151 const goto_functionst::goto_functiont &goto_function) const override;
152
153private:
155};
156
158{
159public:
164
165 bool operator()(
166 const symbolt &identifier,
167 const goto_functionst::goto_functiont &goto_function) const override;
168
169private:
171};
172
175{
176public:
181
182 bool operator()(
183 const symbolt &identifier,
184 const goto_functionst::goto_functiont &goto_function) const override;
185
186private:
187 std::regex regex_matcher;
188};
189
192{
193public:
194 bool operator()(
195 const symbolt &identifier,
196 const goto_functionst::goto_functiont &goto_function) const override;
197};
198
201{
202public:
203 bool operator()(const source_locationt &) const override;
204};
205
206#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:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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.