Skip to content

Commit 0d5d83b

Browse files
jezhigginsjezhiggins
committed
Move template member functions out of variable_sensitivity_object_factoryt
1 parent ca8f6b1 commit 0d5d83b

File tree

2 files changed

+92
-108
lines changed

2 files changed

+92
-108
lines changed

‎src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp‎

Lines changed: 91 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,83 @@ ABSTRACT_OBJECT_TYPET vsd_configt::option_to_abstract_type(
6767
return selected->second;
6868
}
6969

70+
template <class abstract_object_classt, class context_classt>
71+
abstract_object_pointert initialize_context_abstract_object(
72+
const typet type,
73+
bool top,
74+
bool bottom,
75+
const exprt &e,
76+
const abstract_environmentt &environment,
77+
const namespacet &ns)
78+
{
79+
if(top || bottom)
80+
{
81+
return abstract_object_pointert(new context_classt(
82+
abstract_object_pointert(new abstract_object_classt(type, top, bottom)),
83+
type,
84+
top,
85+
bottom));
86+
}
87+
else
88+
{
89+
PRECONDITION(type == ns.follow(e.type()));
90+
return abstract_object_pointert(new context_classt(
91+
abstract_object_pointert(new abstract_object_classt(e, environment, ns)),
92+
e,
93+
environment,
94+
ns));
95+
}
96+
}
97+
98+
/// Function: variable_sensitivity_object_factoryt::initialize_abstract_object
99+
/// Initialize the abstract object class and return it.
100+
///
101+
/// \param type: the type of the variable
102+
/// \param top: whether the abstract object should be top in the
103+
/// two-value domain
104+
/// \param bottom: whether the abstract object should be bottom in the
105+
/// two-value domain
106+
/// \param e: if top and bottom are false this expression is used as the
107+
/// starting pointer for the abstract object
108+
/// \param environment: the current abstract environment
109+
/// \param ns: namespace, used when following the input type
110+
///
111+
/// \return An abstract object of the appropriate type.
112+
///
113+
template <class abstract_object_classt>
114+
abstract_object_pointert initialize_abstract_object(
115+
const typet type,
116+
bool top,
117+
bool bottom,
118+
const exprt &e,
119+
const abstract_environmentt &environment,
120+
const namespacet &ns,
121+
const vsd_configt &configuration)
122+
{
123+
if(configuration.context_tracking.data_dependency_context)
124+
return initialize_context_abstract_object<
125+
abstract_object_classt,
126+
data_dependency_contextt>(type, top, bottom, e, environment, ns);
127+
if(configuration.context_tracking.last_write_context)
128+
return initialize_context_abstract_object<
129+
abstract_object_classt,
130+
write_location_contextt>(type, top, bottom, e, environment, ns);
131+
else
132+
{
133+
if(top || bottom)
134+
{
135+
return abstract_object_pointert(
136+
new abstract_object_classt(type, top, bottom));
137+
}
138+
else
139+
{
140+
PRECONDITION(type == ns.follow(e.type()));
141+
return abstract_object_pointert(
142+
new abstract_object_classt(e, environment, ns));
143+
}
144+
}
145+
}
146+
70147
ABSTRACT_OBJECT_TYPET
71148
variable_sensitivity_object_factoryt::get_abstract_object_type(const typet type)
72149
{
@@ -128,48 +205,48 @@ variable_sensitivity_object_factoryt::get_abstract_object(
128205
{
129206
case CONSTANT:
130207
return initialize_abstract_object<constant_abstract_valuet>(
131-
followed_type, top, bottom, e, environment, ns);
208+
followed_type, top, bottom, e, environment, ns, configuration);
132209
case INTERVAL:
133210
return initialize_abstract_object<interval_abstract_valuet>(
134-
followed_type, top, bottom, e, environment, ns);
211+
followed_type, top, bottom, e, environment, ns, configuration);
135212
case ARRAY_SENSITIVE:
136213
return configuration.value_abstract_type == INTERVAL
137214
? initialize_abstract_object<interval_array_abstract_objectt>(
138-
followed_type, top, bottom, e, environment, ns)
215+
followed_type, top, bottom, e, environment, ns, configuration)
139216
: initialize_abstract_object<constant_array_abstract_objectt>(
140-
followed_type, top, bottom, e, environment, ns);
217+
followed_type, top, bottom, e, environment, ns, configuration);
141218
case ARRAY_INSENSITIVE:
142219
return initialize_abstract_object<array_abstract_objectt>(
143-
followed_type, top, bottom, e, environment, ns);
220+
followed_type, top, bottom, e, environment, ns, configuration);
144221
case POINTER_SENSITIVE:
145222
return initialize_abstract_object<constant_pointer_abstract_objectt>(
146-
followed_type, top, bottom, e, environment, ns);
223+
followed_type, top, bottom, e, environment, ns, configuration);
147224
case POINTER_INSENSITIVE:
148225
return initialize_abstract_object<pointer_abstract_objectt>(
149-
followed_type, top, bottom, e, environment, ns);
226+
followed_type, top, bottom, e, environment, ns, configuration);
150227
case STRUCT_SENSITIVE:
151228
return initialize_abstract_object<full_struct_abstract_objectt>(
152-
followed_type, top, bottom, e, environment, ns);
229+
followed_type, top, bottom, e, environment, ns, configuration);
153230
case STRUCT_INSENSITIVE:
154231
return initialize_abstract_object<struct_abstract_objectt>(
155-
followed_type, top, bottom, e, environment, ns);
232+
followed_type, top, bottom, e, environment, ns, configuration);
156233
case UNION_INSENSITIVE:
157234
return initialize_abstract_object<union_abstract_objectt>(
158-
followed_type, top, bottom, e, environment, ns);
235+
followed_type, top, bottom, e, environment, ns, configuration);
159236
case TWO_VALUE:
160237
return initialize_abstract_object<abstract_objectt>(
161-
followed_type, top, bottom, e, environment, ns);
238+
followed_type, top, bottom, e, environment, ns, configuration);
162239
case VALUE_SET:
163240
if(configuration.advanced_sensitivities.new_value_set)
164241
{
165242
return initialize_abstract_object<value_set_abstract_valuet>(
166-
followed_type, top, bottom, e, environment, ns);
243+
followed_type, top, bottom, e, environment, ns, configuration);
167244
}
168245
return initialize_abstract_object<value_set_abstract_objectt>(
169-
followed_type, top, bottom, e, environment, ns);
246+
followed_type, top, bottom, e, environment, ns, configuration);
170247
default:
171248
UNREACHABLE;
172249
return initialize_abstract_object<abstract_objectt>(
173-
followed_type, top, bottom, e, environment, ns);
250+
followed_type, top, bottom, e, environment, ns, configuration);
174251
}
175252
}

‎src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h‎

Lines changed: 1 addition & 94 deletions
Original file line numberDiff line numberDiff line change
@@ -226,102 +226,9 @@ class variable_sensitivity_object_factoryt
226226
///
227227
/// \return An enum indicating the abstract object type to use.
228228
ABSTRACT_OBJECT_TYPET get_abstract_object_type(const typet type);
229-
template <class abstract_object_class>
230-
abstract_object_pointert initialize_abstract_object(
231-
const typet type,
232-
bool top,
233-
bool bottom,
234-
const exprt &e,
235-
const abstract_environmentt &enviroment,
236-
const namespacet &ns);
237-
template <class abstract_object_class, class context_classt>
238-
abstract_object_pointert initialize_context_abstract_object(
239-
const typet type,
240-
bool top,
241-
bool bottom,
242-
const exprt &e,
243-
const abstract_environmentt &enviroment,
244-
const namespacet &ns);
229+
245230
vsd_configt configuration;
246231
bool initialized;
247232
};
248233

249-
/// Function: variable_sensitivity_object_factoryt::initialize_abstract_object
250-
/// Initialize the abstract object class and return it.
251-
///
252-
/// \param type: the type of the variable
253-
/// \param top: whether the abstract object should be top in the
254-
/// two-value domain
255-
/// \param bottom: whether the abstract object should be bottom in the
256-
/// two-value domain
257-
/// \param e: if top and bottom are false this expression is used as the
258-
/// starting pointer for the abstract object
259-
/// \param environment: the current abstract environment
260-
/// \param ns: namespace, used when following the input type
261-
///
262-
/// \return An abstract object of the appropriate type.
263-
///
264-
template <class abstract_object_classt>
265-
abstract_object_pointert
266-
variable_sensitivity_object_factoryt::initialize_abstract_object(
267-
const typet type,
268-
bool top,
269-
bool bottom,
270-
const exprt &e,
271-
const abstract_environmentt &environment,
272-
const namespacet &ns)
273-
{
274-
if(configuration.context_tracking.data_dependency_context)
275-
return initialize_context_abstract_object<
276-
abstract_object_classt,
277-
data_dependency_contextt>(type, top, bottom, e, environment, ns);
278-
if(configuration.context_tracking.last_write_context)
279-
return initialize_context_abstract_object<
280-
abstract_object_classt,
281-
write_location_contextt>(type, top, bottom, e, environment, ns);
282-
else
283-
{
284-
if(top || bottom)
285-
{
286-
return abstract_object_pointert(
287-
new abstract_object_classt(type, top, bottom));
288-
}
289-
else
290-
{
291-
PRECONDITION(type == ns.follow(e.type()));
292-
return abstract_object_pointert(
293-
new abstract_object_classt(e, environment, ns));
294-
}
295-
}
296-
}
297-
298-
template <class abstract_object_classt, class context_classt>
299-
abstract_object_pointert
300-
variable_sensitivity_object_factoryt::initialize_context_abstract_object(
301-
const typet type,
302-
bool top,
303-
bool bottom,
304-
const exprt &e,
305-
const abstract_environmentt &environment,
306-
const namespacet &ns)
307-
{
308-
if(top || bottom)
309-
{
310-
return abstract_object_pointert(new context_classt(
311-
abstract_object_pointert(new abstract_object_classt(type, top, bottom)),
312-
type,
313-
top,
314-
bottom));
315-
}
316-
else
317-
{
318-
PRECONDITION(type == ns.follow(e.type()));
319-
return abstract_object_pointert(new context_classt(
320-
abstract_object_pointert(new abstract_object_classt(e, environment, ns)),
321-
e,
322-
environment,
323-
ns));
324-
}
325-
}
326-
327234
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_OBJECT_FACTORY_H // NOLINT(*)

0 commit comments

Comments
 (0)