@@ -27,73 +27,81 @@ bool has_symbol(const exprt &src, const find_symbols_sett &symbols)
27
27
return false ;
28
28
}
29
29
30
- void find_symbols (
31
- const exprt &src,
32
- std::set<symbol_exprt> &dest)
33
- {
34
- src.visit_pre ([&dest](const exprt &e) {
35
- if (e.id () == ID_symbol)
36
- dest.insert (to_symbol_expr (e));
37
- });
38
- }
39
-
40
- std::set<symbol_exprt> find_symbols (const exprt &src)
41
- {
42
- return make_range (src.depth_begin (), src.depth_end ())
43
- .filter ([](const exprt &e) { return e.id () == ID_symbol; })
44
- .map ([](const exprt &e) { return to_symbol_expr (e); });
45
- }
30
+ static bool find_symbols (
31
+ kindt,
32
+ const typet &,
33
+ std::function<bool (const symbol_exprt &)>);
46
34
47
- std::unordered_set<irep_idt> find_symbol_identifiers (const exprt &src)
48
- {
49
- std::unordered_set<irep_idt> result;
50
- src.visit_pre ([&](const exprt &e) {
51
- if (e.id () == ID_symbol)
52
- result.insert (to_symbol_expr (e).get_identifier ());
53
- });
54
- return result;
55
- }
56
-
57
- void find_symbols (kindt kind, const typet &src, find_symbols_sett &dest);
58
-
59
- void find_symbols (kindt kind, const exprt &src, find_symbols_sett &dest)
35
+ static bool find_symbols (
36
+ kindt kind,
37
+ const exprt &src,
38
+ std::function<bool (const symbol_exprt &)> op)
60
39
{
61
40
forall_operands (it, src)
62
- find_symbols (kind, *it, dest);
41
+ {
42
+ if (!find_symbols (kind, *it, op))
43
+ return false ;
44
+ }
63
45
64
- find_symbols (kind, src.type (), dest);
46
+ if (!find_symbols (kind, src.type (), op))
47
+ return false ;
65
48
66
49
if (kind == kindt::F_ALL || kind == kindt::F_EXPR)
67
50
{
68
- if (src.id () == ID_symbol)
69
- dest. insert ( to_symbol_expr (src). get_identifier ()) ;
51
+ if (src.id () == ID_symbol && ! op ( to_symbol_expr (src)) )
52
+ return false ;
70
53
}
71
54
72
55
const irept &c_sizeof_type=src.find (ID_C_c_sizeof_type);
73
56
74
- if (c_sizeof_type.is_not_nil ())
75
- find_symbols (kind, static_cast <const typet &>(c_sizeof_type), dest);
57
+ if (
58
+ c_sizeof_type.is_not_nil () &&
59
+ !find_symbols (kind, static_cast <const typet &>(c_sizeof_type), op))
60
+ {
61
+ return false ;
62
+ }
76
63
77
64
const irept &va_arg_type=src.find (ID_C_va_arg_type);
78
65
79
- if (va_arg_type.is_not_nil ())
80
- find_symbols (kind, static_cast <const typet &>(va_arg_type), dest);
66
+ if (
67
+ va_arg_type.is_not_nil () &&
68
+ !find_symbols (kind, static_cast <const typet &>(va_arg_type), op))
69
+ {
70
+ return false ;
71
+ }
72
+
73
+ return true ;
81
74
}
82
75
83
- void find_symbols (kindt kind, const typet &src, find_symbols_sett &dest)
76
+ static bool find_symbols (
77
+ kindt kind,
78
+ const typet &src,
79
+ std::function<bool (const symbol_exprt &)> op)
84
80
{
85
81
if (kind!=kindt::F_TYPE_NON_PTR ||
86
82
src.id ()!=ID_pointer)
87
83
{
88
- if (src.has_subtype ())
89
- find_symbols (kind, to_type_with_subtype (src).subtype (), dest);
84
+ if (
85
+ src.has_subtype () &&
86
+ !find_symbols (kind, to_type_with_subtype (src).subtype (), op))
87
+ {
88
+ return false ;
89
+ }
90
90
91
91
for (const typet &subtype : to_type_with_subtypes (src).subtypes ())
92
- find_symbols (kind, subtype, dest);
92
+ {
93
+ if (!find_symbols (kind, subtype, op))
94
+ return false ;
95
+ }
93
96
94
- const irep_idt &typedef_name=src.get (ID_C_typedef);
95
- if (!typedef_name.empty ())
96
- dest.insert (typedef_name);
97
+ if (
98
+ kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR ||
99
+ kind == kindt::F_ALL)
100
+ {
101
+ const irep_idt &typedef_name = src.get (ID_C_typedef);
102
+ if (!typedef_name.empty () && !op (symbol_exprt{typedef_name, typet{}}))
103
+ return false ;
104
+ }
97
105
}
98
106
99
107
if (src.id ()==ID_struct ||
@@ -102,84 +110,132 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
102
110
const struct_union_typet &struct_union_type=to_struct_union_type (src);
103
111
104
112
for (const auto &c : struct_union_type.components ())
105
- find_symbols (kind, c, dest);
113
+ {
114
+ if (!find_symbols (kind, c, op))
115
+ return false ;
116
+ }
106
117
}
107
118
else if (src.id ()==ID_code)
108
119
{
109
120
const code_typet &code_type=to_code_type (src);
110
- find_symbols (kind, code_type.return_type (), dest);
121
+ if (!find_symbols (kind, code_type.return_type (), op))
122
+ return false ;
111
123
112
124
for (const auto &p : code_type.parameters ())
113
125
{
114
- find_symbols (kind, p, dest);
126
+ if (!find_symbols (kind, p, op))
127
+ return false ;
115
128
}
116
129
}
117
130
else if (src.id ()==ID_array)
118
131
{
119
132
// do the size -- the subtype is already done
120
- find_symbols (kind, to_array_type (src).size (), dest);
121
- }
122
- else if (src.id ()==ID_c_enum_tag)
123
- {
124
- dest.insert (to_c_enum_tag_type (src).get_identifier ());
133
+ if (!find_symbols (kind, to_array_type (src).size (), op))
134
+ return false ;
125
135
}
126
- else if (src.id ()==ID_struct_tag)
136
+ else if (
137
+ kind == kindt::F_TYPE || kind == kindt::F_TYPE_NON_PTR ||
138
+ kind == kindt::F_ALL)
127
139
{
128
- dest.insert (to_struct_tag_type (src).get_identifier ());
129
- }
130
- else if (src.id ()==ID_union_tag)
131
- {
132
- dest.insert (to_union_tag_type (src).get_identifier ());
140
+ if (src.id () == ID_c_enum_tag)
141
+ {
142
+ if (!op (symbol_exprt{to_c_enum_tag_type (src).get_identifier (), typet{}}))
143
+ return false ;
144
+ }
145
+ else if (src.id () == ID_struct_tag)
146
+ {
147
+ if (!op (symbol_exprt{to_struct_tag_type (src).get_identifier (), typet{}}))
148
+ return false ;
149
+ }
150
+ else if (src.id () == ID_union_tag)
151
+ {
152
+ if (!op (symbol_exprt{to_union_tag_type (src).get_identifier (), typet{}}))
153
+ return false ;
154
+ }
133
155
}
156
+
157
+ return true ;
158
+ }
159
+
160
+ void find_symbols (const exprt &src, std::set<symbol_exprt> &dest)
161
+ {
162
+ find_symbols (kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
163
+ dest.insert (e);
164
+ return true ;
165
+ });
134
166
}
135
167
136
168
bool has_symbol (const exprt &src, const irep_idt &identifier, kindt kind)
137
169
{
138
- find_symbols_sett tmp_dest;
139
- find_symbols (kind, src, tmp_dest) ;
140
- return tmp_dest. find (identifier) != tmp_dest. end ( );
170
+ return ! find_symbols (kind, src, [&identifier]( const symbol_exprt &e) {
171
+ return e. get_identifier () != identifier ;
172
+ } );
141
173
}
142
174
143
175
void find_type_symbols (const exprt &src, find_symbols_sett &dest)
144
176
{
145
- find_symbols (kindt::F_TYPE, src, dest);
177
+ find_symbols (kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
178
+ dest.insert (e.get_identifier ());
179
+ return true ;
180
+ });
146
181
}
147
182
148
183
void find_type_symbols (const typet &src, find_symbols_sett &dest)
149
184
{
150
- find_symbols (kindt::F_TYPE, src, dest);
185
+ find_symbols (kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
186
+ dest.insert (e.get_identifier ());
187
+ return true ;
188
+ });
151
189
}
152
190
153
191
void find_non_pointer_type_symbols (
154
192
const exprt &src,
155
193
find_symbols_sett &dest)
156
194
{
157
- find_symbols (kindt::F_TYPE_NON_PTR, src, dest);
195
+ find_symbols (kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
196
+ dest.insert (e.get_identifier ());
197
+ return true ;
198
+ });
158
199
}
159
200
160
201
void find_non_pointer_type_symbols (
161
202
const typet &src,
162
203
find_symbols_sett &dest)
163
204
{
164
- find_symbols (kindt::F_TYPE_NON_PTR, src, dest);
205
+ find_symbols (kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
206
+ dest.insert (e.get_identifier ());
207
+ return true ;
208
+ });
165
209
}
166
210
167
211
void find_type_and_expr_symbols (const exprt &src, find_symbols_sett &dest)
168
212
{
169
- find_symbols (kindt::F_ALL, src, dest);
213
+ find_symbols (kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
214
+ dest.insert (e.get_identifier ());
215
+ return true ;
216
+ });
170
217
}
171
218
172
219
void find_type_and_expr_symbols (const typet &src, find_symbols_sett &dest)
173
220
{
174
- find_symbols (kindt::F_ALL, src, dest);
221
+ find_symbols (kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
222
+ dest.insert (e.get_identifier ());
223
+ return true ;
224
+ });
175
225
}
176
226
177
227
void find_symbols_or_nexts (const exprt &src, find_symbols_sett &dest)
178
228
{
179
- find_symbols (kindt::F_EXPR, src, dest);
229
+ find_symbols (kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
230
+ dest.insert (e.get_identifier ());
231
+ return true ;
232
+ });
180
233
}
181
234
182
235
void find_symbols (const exprt &src, find_symbols_sett &dest)
183
236
{
184
- find_symbols (kindt::F_EXPR, src, dest);
237
+ find_symbols (kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
238
+ dest.insert (e.get_identifier ());
239
+ return true ;
240
+ });
185
241
}
0 commit comments