Skip to content

Commit 48146e0

Browse files
jezhigginsjezhiggins
committed
Regression tests capturing value-set compacting
Simple variable, array element, and field in a structure. They all compact.
1 parent 4248f1b commit 48146e0

File tree

7 files changed

+163
-39
lines changed

7 files changed

+163
-39
lines changed

regression/goto-analyzer/value-set-convert-to-interval/main.c renamed to regression/goto-analyzer/value-set-compact-01/main.c

File renamed without changes.

regression/goto-analyzer/value-set-convert-to-interval/test.desc renamed to regression/goto-analyzer/value-set-compact-01/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
FUTURE
1+
CORE
22
main.c
33
--variable-sensitivity --vsd-values set-of-constants --show
44
^EXIT=0$
55
^SIGNAL=0$
66
main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\]
77
main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\]
8-
main::1::c .* \[14, 1E\] @ \[30\]
8+
main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[30\]
99
--

‎regression/goto-analyzer/value-set-compact-02/main.c‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
#include <stdbool.h>
2+
3+
extern int x;
4+
5+
int main(void)
6+
{
7+
int a[1] = {0};
8+
switch(x)
9+
{
10+
case 1:
11+
a[0] = 1;
12+
break;
13+
case 2:
14+
a[0] = 2;
15+
break;
16+
case 3:
17+
a[0] = 3;
18+
break;
19+
case 4:
20+
a[0] = 4;
21+
break;
22+
case 5:
23+
a[0] = 5;
24+
break;
25+
case 6:
26+
a[0] = 6;
27+
break;
28+
case 7:
29+
a[0] = 7;
30+
break;
31+
case 8:
32+
a[0] = 8;
33+
break;
34+
case 9:
35+
a[0] = 9;
36+
break;
37+
case 10:
38+
a[0] = 10;
39+
break;
40+
case 11:
41+
a[0] = 11;
42+
break;
43+
case 12:
44+
a[0] = 12;
45+
break;
46+
}
47+
48+
return 0;
49+
}

‎regression/goto-analyzer/value-set-compact-02/test.desc‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]
7+
--

‎regression/goto-analyzer/value-set-compact-03/main.c‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
#include <stdbool.h>
2+
3+
extern int x;
4+
5+
struct S
6+
{
7+
int a;
8+
};
9+
10+
int main(void)
11+
{
12+
struct S a;
13+
a.a = 0;
14+
switch(x)
15+
{
16+
case 1:
17+
a.a = 1;
18+
break;
19+
case 2:
20+
a.a = 2;
21+
break;
22+
case 3:
23+
a.a = 3;
24+
break;
25+
case 4:
26+
a.a = 4;
27+
break;
28+
case 5:
29+
a.a = 5;
30+
break;
31+
case 6:
32+
a.a = 6;
33+
break;
34+
case 7:
35+
a.a = 7;
36+
break;
37+
case 8:
38+
a.a = 8;
39+
break;
40+
case 9:
41+
a.a = 9;
42+
break;
43+
case 10:
44+
a.a = 10;
45+
break;
46+
case 11:
47+
a.a = 11;
48+
break;
49+
case 12:
50+
a.a = 12;
51+
break;
52+
}
53+
54+
return 0;
55+
}

‎regression/goto-analyzer/value-set-compact-03/test.desc‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]\} .*
7+
--

‎unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp‎

Lines changed: 43 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,13 @@ SCENARIO(
4040
auto val11 = from_integer(11, type);
4141
auto val12 = from_integer(12, type);
4242
auto val13 = from_integer(13, type);
43+
auto val1minus = from_integer(-1, type);
44+
auto val2minus = from_integer(-2, type);
45+
auto val3minus = from_integer(-3, type);
46+
auto val4minus = from_integer(-4, type);
47+
auto val5minus = from_integer(-5, type);
48+
auto val8minus = from_integer(-8, type);
49+
auto val10minus = from_integer(-10, type);
4350

4451
auto config = vsd_configt::constant_domain();
4552
config.context_tracking.data_dependency_context = false;
@@ -312,69 +319,68 @@ SCENARIO(
312319
EXPECT_MODIFIED(merged, {interval_3minus_3, interval_2_4});
313320
}
314321
}
315-
/*
316-
WHEN("merging [-3, -1] with [-4, -2]")
322+
WHEN("merging {-3, -1} with {-4, -2}")
317323
{
318-
auto op1 = make_value_set(val3minus, val1minus, environment, ns);
319-
auto op2 = make_value_set(val4minus, val2minus, environment, ns);
324+
auto op1 = make_value_set({val3minus, val1minus}, environment, ns);
325+
auto op2 = make_value_set({val4minus, val2minus}, environment, ns);
320326

321327
auto merged = widening_merge(op1, op2);
322328

323-
THEN("widen lower bound - [-8, -1]")
329+
THEN("widen lower bound - {[-8, -4], -3, -2, -1}")
324330
{
325-
EXPECT_MODIFIED(merged, val8minus, val1minus);
326-
}
327-
}
328-
WHEN("merging [-4, -2] with [-3, -1]")
329-
{
330-
auto op1 = make_value_set(val4minus, val2minus, environment, ns);
331-
auto op2 = make_value_set(val3minus, val1minus, environment, ns);
332-
333-
auto merged = widening_merge(op1, op2);
334-
335-
THEN("widen upper bound - [-4, 3]")
336-
{
337-
EXPECT_MODIFIED(merged, val4minus, val3);
331+
EXPECT_MODIFIED(
332+
merged,
333+
{constant_interval_exprt(val8minus, val4minus),
334+
val3minus,
335+
val2minus,
336+
val1minus});
338337
}
339338
}
340-
WHEN("merging [-2, -1] with [-5, -4]")
339+
WHEN("merging {[-3, -1]} with {[-4, -2]}")
341340
{
342-
auto op1 = make_value_set(val2minus, val1minus, environment, ns);
343-
auto op2 = make_value_set(val5minus, val4minus, environment, ns);
341+
auto interval31minus = constant_interval_exprt(val3minus, val1minus);
342+
auto interval42minus = constant_interval_exprt(val4minus, val2minus);
343+
auto op1 = make_value_set(interval31minus, environment, ns);
344+
auto op2 = make_value_set(interval42minus, environment, ns);
344345

345346
auto merged = widening_merge(op1, op2);
346347

347-
THEN("widen lower bound - [-10, -1]")
348+
THEN("widen lower bound - {[-8, -2], [-3, -1]}")
348349
{
349-
EXPECT_MODIFIED(merged, val10minus, val1minus);
350+
EXPECT_MODIFIED(
351+
merged,
352+
{constant_interval_exprt(val8minus, val2minus), interval31minus});
350353
}
351354
}
352-
WHEN("merging [-5, -4] with [-2, -1]")
355+
WHEN("merging {-3, -1} with {[-4, -2]}")
353356
{
354-
auto op1 = make_value_set(val5minus, val4minus, environment, ns);
355-
auto op2 = make_value_set(val2minus, val1minus, environment, ns);
357+
auto interval42minus = constant_interval_exprt(val4minus, val2minus);
358+
auto op1 = make_value_set({val3minus, val1minus}, environment, ns);
359+
auto op2 = make_value_set(interval42minus, environment, ns);
356360

357361
auto merged = widening_merge(op1, op2);
358362

359-
THEN("widen upper bound - [-5, 4]")
363+
THEN("widen lower bound - {[-8, -2], -1}")
360364
{
361-
EXPECT_MODIFIED(merged, val5minus, val4);
365+
EXPECT_MODIFIED(
366+
merged, {constant_interval_exprt(val8minus, val2minus), val1minus});
362367
}
363368
}
364-
WHEN("merging [-3, -2] with [-5, -1]")
369+
WHEN("merging {[-3, -1]} with {-4, -2}")
365370
{
366-
auto op1 = make_value_set(val3minus, val2minus, environment, ns);
367-
auto op2 = make_value_set(val5minus, val1minus, environment, ns);
371+
auto interval31minus = constant_interval_exprt(val3minus, val1minus);
372+
auto op1 = make_value_set(interval31minus, environment, ns);
373+
auto op2 = make_value_set({val4minus, val2minus}, environment, ns);
368374

369375
auto merged = widening_merge(op1, op2);
370-
371-
THEN("result is widen both bounds - [-10, 4]")
376+
THEN("widen lower bound - {[-8, -4], [-3, -1], -2}")
372377
{
373-
EXPECT_MODIFIED(merged, val10minus, val4);
378+
EXPECT_MODIFIED(
379+
merged,
380+
{constant_interval_exprt(val8minus, val4minus),
381+
interval31minus,
382+
val2minus});
374383
}
375384
}
376-
377-
value_sets with intervals too
378-
*/
379385
}
380386
}

0 commit comments

Comments
 (0)