@@ -145,17 +145,8 @@ typedef
145145#define TEST_FUNCTION_NAME TEST_PREFIX " test:()V"
146146#define TEST_LOCAL_PREFIX TEST_FUNCTION_NAME " ::"
147147
148- template <class VST >
149- static value_setst::valuest
150- get_values (const VST &value_set, const namespacet &ns, const exprt &expr)
151- {
152- value_setst::valuest vals;
153- value_set.get_value_set (expr, vals, ns);
154- return vals;
155- }
156-
157- static std::size_t exprs_with_id (
158- const value_setst::valuest &exprs, const irep_idt &id)
148+ static std::size_t
149+ exprs_with_id (const std::vector<exprt> &exprs, const irep_idt &id)
159150{
160151 return std::count_if (
161152 exprs.begin (),
@@ -222,15 +213,15 @@ SCENARIO("test_value_set_analysis",
222213 TEST_LOCAL_PREFIX " 23::ignored" , jlo_ref_type);
223214 THEN (" The normal analysis should write to it" )
224215 {
225- auto normal_exprs=
226- get_values ( normal_function_end_vs, ns, written_symbol );
216+ auto normal_exprs =
217+ normal_function_end_vs. get_value_set (written_symbol , ns);
227218 REQUIRE (exprs_with_id (normal_exprs, ID_dynamic_object)==1 );
228219 REQUIRE (exprs_with_id (normal_exprs, ID_unknown)==0 );
229220 }
230221 THEN (" The custom analysis should ignore the write to it" )
231222 {
232- auto test_exprs=
233- get_values ( test_function_end_vs, ns, written_symbol );
223+ auto test_exprs =
224+ test_function_end_vs. get_value_set (written_symbol , ns);
234225 REQUIRE (exprs_with_id (test_exprs, ID_dynamic_object)==0 );
235226 REQUIRE (exprs_with_id (test_exprs, ID_unknown)==1 );
236227 }
@@ -242,15 +233,15 @@ SCENARIO("test_value_set_analysis",
242233 TEST_LOCAL_PREFIX " 31::no_write" , jlo_ref_type);
243234 THEN (" The normal analysis should write to it" )
244235 {
245- auto normal_exprs=
246- get_values ( normal_function_end_vs, ns, written_symbol );
236+ auto normal_exprs =
237+ normal_function_end_vs. get_value_set (written_symbol , ns);
247238 REQUIRE (exprs_with_id (normal_exprs, ID_dynamic_object)==1 );
248239 REQUIRE (exprs_with_id (normal_exprs, ID_unknown)==0 );
249240 }
250241 THEN (" The custom analysis should ignore the write to it" )
251242 {
252- auto test_exprs=
253- get_values ( test_function_end_vs, ns, written_symbol );
243+ auto test_exprs =
244+ test_function_end_vs. get_value_set (written_symbol , ns);
254245 REQUIRE (exprs_with_id (test_exprs, ID_dynamic_object)==0 );
255246 REQUIRE (exprs_with_id (test_exprs, ID_unknown)==1 );
256247 }
@@ -262,15 +253,15 @@ SCENARIO("test_value_set_analysis",
262253 TEST_LOCAL_PREFIX " 55::read" , jlo_ref_type);
263254 THEN (" The normal analysis should find a dynamic object" )
264255 {
265- auto normal_exprs=
266- get_values ( normal_function_end_vs, ns, written_symbol );
256+ auto normal_exprs =
257+ normal_function_end_vs. get_value_set (written_symbol , ns);
267258 REQUIRE (exprs_with_id (normal_exprs, ID_dynamic_object)==1 );
268259 REQUIRE (exprs_with_id (normal_exprs, ID_unknown)==0 );
269260 }
270261 THEN (" The custom analysis should have no information about it" )
271262 {
272- auto test_exprs=
273- get_values ( test_function_end_vs, ns, written_symbol );
263+ auto test_exprs =
264+ test_function_end_vs. get_value_set (written_symbol , ns);
274265 REQUIRE (test_exprs.size ()==0 );
275266 }
276267 }
@@ -281,16 +272,16 @@ SCENARIO("test_value_set_analysis",
281272 TEST_PREFIX " maybe_unknown_read" , jlo_ref_type);
282273 THEN (" The normal analysis should find a dynamic object" )
283274 {
284- auto normal_exprs=
285- get_values ( normal_function_end_vs, ns, written_symbol );
275+ auto normal_exprs =
276+ normal_function_end_vs. get_value_set (written_symbol , ns);
286277 REQUIRE (exprs_with_id (normal_exprs, ID_dynamic_object)==1 );
287278 REQUIRE (exprs_with_id (normal_exprs, ID_unknown)==0 );
288279 }
289280 THEN (" The custom analysis should find a dynamic object "
290281 " *and* an unknown entry" )
291282 {
292- auto test_exprs=
293- get_values ( test_function_end_vs, ns, written_symbol );
283+ auto test_exprs =
284+ test_function_end_vs. get_value_set (written_symbol , ns);
294285 REQUIRE (test_exprs.size ()==2 );
295286 REQUIRE (exprs_with_id (test_exprs, ID_unknown)==1 );
296287 REQUIRE (exprs_with_id (test_exprs, ID_dynamic_object)==1 );
@@ -301,16 +292,16 @@ SCENARIO("test_value_set_analysis",
301292 {
302293 symbol_exprt read_before_cause_write (
303294 TEST_PREFIX " first_effect_read" , jlo_ref_type);
304- auto normal_exprs_before=
305- get_values ( normal_function_end_vs, ns, read_before_cause_write );
306- auto test_exprs_before=
307- get_values ( test_function_end_vs, ns, read_before_cause_write );
295+ auto normal_exprs_before =
296+ normal_function_end_vs. get_value_set (read_before_cause_write , ns);
297+ auto test_exprs_before =
298+ test_function_end_vs. get_value_set (read_before_cause_write , ns);
308299 symbol_exprt read_after_cause_write (
309300 TEST_PREFIX " second_effect_read" , jlo_ref_type);
310- auto normal_exprs_after=
311- get_values ( normal_function_end_vs, ns, read_after_cause_write );
312- auto test_exprs_after=
313- get_values ( test_function_end_vs, ns, read_after_cause_write );
301+ auto normal_exprs_after =
302+ normal_function_end_vs. get_value_set (read_after_cause_write , ns);
303+ auto test_exprs_after =
304+ test_function_end_vs. get_value_set (read_after_cause_write , ns);
314305
315306 THEN (" Before writing to 'cause' both analyses should think 'effect' "
316307 " points to some object" )
0 commit comments