13
13
// was accessed using e.g. member-x--of-dereference (written
14
14
// "->x" in C++, ".x" in Java) at function f location
15
15
// (instruction offset) z.
16
- class access_path_entry_exprt : public exprt
16
+ class access_path_entry_exprt : public exprt
17
17
{
18
- public:
19
- access_path_entry_exprt ():exprt(ID_access_path_entry) {}
18
+ public:
19
+ access_path_entry_exprt () : exprt(ID_access_path_entry)
20
+ {
21
+ }
22
+
20
23
access_path_entry_exprt (
21
24
const irep_idt &label,
22
25
const irep_idt &function,
23
26
const irep_idt &loc,
24
27
const typet &declared_on_type)
25
- :exprt(ID_access_path_entry)
28
+ : exprt(ID_access_path_entry)
26
29
{
27
30
set_label (label);
28
31
set (ID_access_path_function, function);
29
32
set (ID_access_path_loc, loc);
30
33
add (ID_declared_on_type, declared_on_type);
31
34
}
32
35
33
- irep_idt label () const { return get (ID_access_path_label); }
34
- void set_label (const irep_idt &i) { set (ID_access_path_label, i); }
35
- irep_idt function () const { return get (ID_access_path_function); }
36
- irep_idt loc () const { return get (ID_access_path_loc); }
36
+ irep_idt label () const
37
+ {
38
+ return get (ID_access_path_label);
39
+ }
40
+
41
+ void set_label (const irep_idt &i)
42
+ {
43
+ set (ID_access_path_label, i);
44
+ }
45
+
46
+ irep_idt function () const
47
+ {
48
+ return get (ID_access_path_function);
49
+ }
50
+
51
+ irep_idt loc () const
52
+ {
53
+ return get (ID_access_path_loc);
54
+ }
55
+
37
56
const typet &declared_on_type () const
38
57
{
39
58
return static_cast <const typet &>(find (ID_declared_on_type));
40
59
}
60
+
41
61
void drop_loc ()
42
62
{
43
63
set (ID_access_path_function, " " );
@@ -77,16 +97,16 @@ enum class external_value_set_typet
77
97
// Represents an external unknown points-to set that can't be
78
98
// directly referenced with a symbol, such as "arg1->x"
79
99
80
- class external_value_set_exprt : public exprt
100
+ class external_value_set_exprt : public exprt
81
101
{
82
- public:
83
- external_value_set_exprt (): exprt(ID_external_value_set)
102
+ public:
103
+ external_value_set_exprt () : exprt(ID_external_value_set)
84
104
{
85
105
// The default-initalised version of EVS doesn't represent anything sane;
86
106
// the caller should set label() before using an instance constructed
87
107
// this way.
88
108
operands ().resize (2 );
89
- op0 ()= constant_exprt ();
109
+ op0 () = constant_exprt ();
90
110
// / No need to initialise op1(). op1().operands() will hold the vector of
91
111
// / access path entries.
92
112
}
@@ -95,11 +115,11 @@ class external_value_set_exprt:public exprt
95
115
const typet &type,
96
116
const constant_exprt &_label,
97
117
const external_value_set_typet mode,
98
- bool is_initializer):
99
- exprt (ID_external_value_set, type)
118
+ bool is_initializer)
119
+ : exprt(ID_external_value_set, type)
100
120
{
101
121
operands ().resize (2 );
102
- op0 ()= _label;
122
+ op0 () = _label;
103
123
// / No need to initialise op1(). op1().operands() will hold the vector of
104
124
// / access path entries.
105
125
set (ID_lvsa_evs_type, std::to_string (static_cast <int >(mode)));
@@ -140,24 +160,31 @@ class external_value_set_exprt:public exprt
140
160
141
161
bool can_extend_to_imprecise () const
142
162
{
143
- return
144
- get_external_value_set_type ()== external_value_set_typet::ROOT_OBJECT ||
145
- get_external_value_set_type ()== external_value_set_typet::PER_FIELD;
163
+ const external_value_set_typet evs_type = get_external_value_set_type ();
164
+ return evs_type == external_value_set_typet::ROOT_OBJECT ||
165
+ evs_type == external_value_set_typet::PER_FIELD;
146
166
}
147
167
148
168
bool can_extend_to_precise () const
149
169
{
150
170
#ifdef DO_NOT_USE_PRECISE_EXTERNAL_VALUE_SETS
151
171
return false ;
152
172
#else
153
- return
154
- get_external_value_set_type ()== external_value_set_typet::ROOT_OBJECT ||
155
- get_external_value_set_type ()== external_value_set_typet::PRECISE;
173
+ const external_value_set_typet evs_type = get_external_value_set_type ();
174
+ return evs_type == external_value_set_typet::ROOT_OBJECT ||
175
+ evs_type == external_value_set_typet::PRECISE;
156
176
#endif
157
177
}
158
178
159
- constant_exprt &label () { return to_constant_expr (op0 ()); }
160
- const constant_exprt &label () const { return to_constant_expr (op0 ()); }
179
+ constant_exprt &label ()
180
+ {
181
+ return to_constant_expr (op0 ());
182
+ }
183
+
184
+ const constant_exprt &label () const
185
+ {
186
+ return to_constant_expr (op0 ());
187
+ }
161
188
162
189
typedef std::vector<access_path_entry_exprt> access_path_entriest;
163
190
@@ -173,27 +200,30 @@ class external_value_set_exprt:public exprt
173
200
174
201
std::string type_to_basename (const typet &type) const
175
202
{
176
- if (type.id ()!= ID_struct)
203
+ if (type.id () != ID_struct)
177
204
return " " ;
178
- std::string tag= id2string (to_struct_type (type).get_tag ());
205
+ std::string tag = id2string (to_struct_type (type).get_tag ());
179
206
for (auto &c : tag)
180
- if (c==' .' )
181
- c=' _' ;
182
- return ' _' +tag;
207
+ {
208
+ if (c == ' .' )
209
+ c = ' _' ;
210
+ }
211
+ return ' _' + tag;
183
212
}
184
213
185
214
std::string get_access_path_basename (const typet &declared_on_type) const
186
215
{
187
216
switch (get_external_value_set_type ())
188
217
{
189
218
case external_value_set_typet::PER_FIELD:
190
- return PER_FIELD_EVS_PREFIX+ type_to_basename (declared_on_type);
219
+ return PER_FIELD_EVS_PREFIX + type_to_basename (declared_on_type);
191
220
case external_value_set_typet::PRECISE:
192
221
return id2string (label ().get_value ());
193
222
default :
194
223
UNREACHABLE;
195
224
}
196
225
}
226
+
197
227
std::string get_access_path_suffix () const
198
228
{
199
229
switch (get_external_value_set_type ())
@@ -227,9 +257,10 @@ class external_value_set_exprt:public exprt
227
257
// / `external_value_set_typet::PRECISE`. In this case we should delete the
228
258
// / external value set.
229
259
bool extend_access_path (
230
- const access_path_entry_exprt &newentry, external_value_set_typet evs_type)
260
+ const access_path_entry_exprt &newentry,
261
+ external_value_set_typet evs_type)
231
262
{
232
- PRECONDITION (evs_type!= external_value_set_typet::ROOT_OBJECT);
263
+ PRECONDITION (evs_type != external_value_set_typet::ROOT_OBJECT);
233
264
set_external_value_set_type (evs_type);
234
265
set_non_initializer ();
235
266
@@ -238,28 +269,28 @@ class external_value_set_exprt:public exprt
238
269
case external_value_set_typet::PER_FIELD:
239
270
{
240
271
// Any attempt to extend a path yields <all-externals>->fieldname
241
- label ()= constant_exprt (PER_FIELD_EVS_PREFIX, string_typet ());
242
- access_path_entry_exprt toadd= newentry;
272
+ label () = constant_exprt (PER_FIELD_EVS_PREFIX, string_typet ());
273
+ access_path_entry_exprt toadd = newentry;
243
274
// In this case entries created at different
244
275
// locations are not distinguished:
245
276
toadd.drop_loc ();
246
277
if (access_path_entries ().empty ())
247
278
access_path_entries ().push_back (toadd);
248
279
else
249
- access_path_entries ().back ()= toadd;
280
+ access_path_entries ().back () = toadd;
250
281
break ;
251
282
}
252
283
case external_value_set_typet::PRECISE:
253
284
{
254
285
// / Check if there is a loop, i.e. there is already an access path
255
286
// / entry with the same label and loc as the one we are adding
256
287
for (const auto &entry : access_path_entries ())
257
- if (entry== newentry)
288
+ if (entry == newentry)
258
289
return true ;
259
290
260
291
if (access_path_entries ().empty ())
261
- label ()= constant_exprt (
262
- PRECISE_EVS_PREFIX+ id2string (label ().get_value ()), string_typet ());
292
+ label () = constant_exprt (
293
+ PRECISE_EVS_PREFIX + id2string (label ().get_value ()), string_typet ());
263
294
264
295
access_path_entries ().push_back (newentry);
265
296
break ;
@@ -289,7 +320,7 @@ class external_value_set_exprt:public exprt
289
320
return *this ;
290
321
else
291
322
{
292
- external_value_set_exprt copy= *this ;
323
+ external_value_set_exprt copy = *this ;
293
324
copy.set_non_initializer ();
294
325
return copy;
295
326
}
@@ -323,10 +354,10 @@ inline const external_value_set_exprt &to_external_value_set(const exprt &e)
323
354
return static_cast <const external_value_set_exprt &>(e);
324
355
}
325
356
326
- template <>
327
- inline bool can_cast_expr<external_value_set_exprt >(const exprt &base)
357
+ template <>
358
+ inline bool can_cast_expr<external_value_set_exprt>(const exprt &base)
328
359
{
329
- return base.id ()== ID_external_value_set;
360
+ return base.id () == ID_external_value_set;
330
361
}
331
362
332
363
#endif
0 commit comments