Skip to content

Commit 51dcb3f

Browse files
tautschnigtautschnig
committed
Constant propagation for individual fields through byte extract
Field sensitivity in goto symex updates the full object as well as individual fields for divisible objects. The updates of individual fields, however, previously used index or member expressions on that full object. Consequently, constant propagation was only possible when the full-object assignment had a constant as the right-hand side. In some cases, however, only parts of the whole object might be constant. We are now able to constant propagate the fields covering those (constant) parts. Fixes: diffblue#6846
1 parent ee860d4 commit 51dcb3f

File tree

19 files changed

+247
-170
lines changed

19 files changed

+247
-170
lines changed

‎jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,20 @@
11
CORE
22
Test
33
--function Test.main --show-vcc --max-field-sensitivity-array-size 10
4-
symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
5-
symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
6-
symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
7-
symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
8-
symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
9-
symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
10-
symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
11-
symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
12-
symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
13-
symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
4+
symex_dynamic::dynamic_2_array#2\[\[0\]\] =
5+
symex_dynamic::dynamic_2_array#2\[\[1\]\] =
6+
symex_dynamic::dynamic_2_array#2\[\[2\]\] =
7+
symex_dynamic::dynamic_2_array#2\[\[3\]\] =
8+
symex_dynamic::dynamic_2_array#2\[\[4\]\] =
9+
symex_dynamic::dynamic_2_array#2\[\[5\]\] =
10+
symex_dynamic::dynamic_2_array#2\[\[6\]\] =
11+
symex_dynamic::dynamic_2_array#2\[\[7\]\] =
12+
symex_dynamic::dynamic_2_array#2\[\[8\]\] =
13+
symex_dynamic::dynamic_2_array#2\[\[9\]\] =
1414
symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
1515
^EXIT=0$
1616
^SIGNAL=0$
1717
--
1818
--
1919
This checks that field sensitvity is still applied to an array of size 10
20-
when the max is set to 10.
20+
when the max is set to 10.

‎jbmc/regression/jbmc/array-cell-sensitivity1/test.desc

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
CORE
22
Test
33
--function Test.main --show-vcc
4-
symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
5-
symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
6-
symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
7-
symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
8-
symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
9-
symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
10-
symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
11-
symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
12-
symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
13-
symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
4+
symex_dynamic::dynamic_2_array#2\[\[0\]\] =
5+
symex_dynamic::dynamic_2_array#2\[\[1\]\] =
6+
symex_dynamic::dynamic_2_array#2\[\[2\]\] =
7+
symex_dynamic::dynamic_2_array#2\[\[3\]\] =
8+
symex_dynamic::dynamic_2_array#2\[\[4\]\] =
9+
symex_dynamic::dynamic_2_array#2\[\[5\]\] =
10+
symex_dynamic::dynamic_2_array#2\[\[6\]\] =
11+
symex_dynamic::dynamic_2_array#2\[\[7\]\] =
12+
symex_dynamic::dynamic_2_array#2\[\[8\]\] =
13+
symex_dynamic::dynamic_2_array#2\[\[9\]\] =
1414
symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
1515
^EXIT=0$
1616
^SIGNAL=0$

‎regression/cbmc/array-cell-sensitivity1/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
5-
main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
6-
main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
7-
main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
8-
main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
9-
main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
10-
main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
11-
main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
12-
main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
4+
main::1::array!0@1#2\[\[1\]\] =
5+
main::1::array!0@1#2\[\[2\]\] =
6+
main::1::array!0@1#2\[\[3\]\] =
7+
main::1::array!0@1#2\[\[4\]\] =
8+
main::1::array!0@1#2\[\[5\]\] =
9+
main::1::array!0@1#2\[\[6\]\] =
10+
main::1::array!0@1#2\[\[7\]\] =
11+
main::1::array!0@1#2\[\[8\]\] =
12+
main::1::array!0@1#2\[\[9\]\] =
1313
main::1::array!0@1#3\[\[1\]\] =
1414
^EXIT=0$
1515
^SIGNAL=0$

‎regression/cbmc/array-cell-sensitivity10/test.desc

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,27 @@
11
CORE
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
5-
main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
6-
main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
7-
main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
8-
main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
9-
main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
10-
main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
11-
main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
12-
main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
13-
main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
4+
main::1::array!0@1#2\[\[0\]\]..x =
5+
main::1::array!0@1#2\[\[1\]\]..x =
6+
main::1::array!0@1#2\[\[2\]\]..x =
7+
main::1::array!0@1#2\[\[3\]\]..x =
8+
main::1::array!0@1#2\[\[4\]\]..x =
9+
main::1::array!0@1#2\[\[5\]\]..x =
10+
main::1::array!0@1#2\[\[6\]\]..x =
11+
main::1::array!0@1#2\[\[7\]\]..x =
12+
main::1::array!0@1#2\[\[8\]\]..x =
13+
main::1::array!0@1#2\[\[9\]\]..x =
1414
main::1::array!0@1#3\[\[1\]\]..x =
15-
main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
16-
main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
17-
main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
18-
main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
19-
main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
20-
main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
21-
main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
22-
main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
23-
main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
24-
main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
15+
main::1::array!0@1#2\[\[0\]\]..y =
16+
main::1::array!0@1#2\[\[1\]\]..y =
17+
main::1::array!0@1#2\[\[2\]\]..y =
18+
main::1::array!0@1#2\[\[3\]\]..y =
19+
main::1::array!0@1#2\[\[4\]\]..y =
20+
main::1::array!0@1#2\[\[5\]\]..y =
21+
main::1::array!0@1#2\[\[6\]\]..y =
22+
main::1::array!0@1#2\[\[7\]\]..y =
23+
main::1::array!0@1#2\[\[8\]\]..y =
24+
main::1::array!0@1#2\[\[9\]\]..y =
2525
^EXIT=0$
2626
^SIGNAL=0$
2727
--

‎regression/cbmc/array-cell-sensitivity3/test.desc

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
CORE
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2\[\[0]\] = main::1::array!0@1#1\[0\]
5-
main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
6-
main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
7-
main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
8-
main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
9-
main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
10-
main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
11-
main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
12-
main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
13-
main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
4+
main::1::array!0@1#2\[\[0\]\] =
5+
main::1::array!0@1#2\[\[1\]\] =
6+
main::1::array!0@1#2\[\[2\]\] =
7+
main::1::array!0@1#2\[\[3\]\] =
8+
main::1::array!0@1#2\[\[4\]\] =
9+
main::1::array!0@1#2\[\[5\]\] =
10+
main::1::array!0@1#2\[\[6\]\] =
11+
main::1::array!0@1#2\[\[7\]\] =
12+
main::1::array!0@1#2\[\[8\]\] =
13+
main::1::array!0@1#2\[\[9\]\] =
1414
main::1::array!0@1#3\[\[1\]\] =
1515
^EXIT=0$
1616
^SIGNAL=0$

‎regression/cbmc/array-cell-sensitivity4/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
5-
main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
6-
main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
7-
main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
8-
main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
9-
main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
10-
main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
11-
main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
12-
main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
4+
main::1::array!0@1#2\[\[1\]\] =
5+
main::1::array!0@1#2\[\[2\]\] =
6+
main::1::array!0@1#2\[\[3\]\] =
7+
main::1::array!0@1#2\[\[4\]\] =
8+
main::1::array!0@1#2\[\[5\]\] =
9+
main::1::array!0@1#2\[\[6\]\] =
10+
main::1::array!0@1#2\[\[7\]\] =
11+
main::1::array!0@1#2\[\[8\]\] =
12+
main::1::array!0@1#2\[\[9\]\] =
1313
main::1::array!0@1#3\[\[1\]\] =
1414
^EXIT=0$
1515
^SIGNAL=0$

‎regression/cbmc/array-cell-sensitivity5/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE
22
test.c
33
--show-vcc
4-
symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\]
5-
symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\]
6-
symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\]
7-
symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\]
8-
symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\]
9-
symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\]
10-
symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\]
11-
symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\]
12-
symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\]
4+
symex_dynamic::dynamic_object1#2\[\[1\]\] =
5+
symex_dynamic::dynamic_object1#2\[\[2\]\] =
6+
symex_dynamic::dynamic_object1#2\[\[3\]\] =
7+
symex_dynamic::dynamic_object1#2\[\[4\]\] =
8+
symex_dynamic::dynamic_object1#2\[\[5\]\] =
9+
symex_dynamic::dynamic_object1#2\[\[6\]\] =
10+
symex_dynamic::dynamic_object1#2\[\[7\]\] =
11+
symex_dynamic::dynamic_object1#2\[\[8\]\] =
12+
symex_dynamic::dynamic_object1#2\[\[9\]\] =
1313
symex_dynamic::dynamic_object1#3\[\[1\]\] =
1414
^EXIT=0$
1515
^SIGNAL=0$

‎regression/cbmc/array-cell-sensitivity6/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE
22
test.c
33
--show-vcc
4-
symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\]
5-
symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\]
6-
symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\]
7-
symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\]
8-
symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\]
9-
symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\]
10-
symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\]
11-
symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\]
12-
symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\]
4+
symex_dynamic::dynamic_object1#2\[\[1\]\] =
5+
symex_dynamic::dynamic_object1#2\[\[2\]\] =
6+
symex_dynamic::dynamic_object1#2\[\[3\]\] =
7+
symex_dynamic::dynamic_object1#2\[\[4\]\] =
8+
symex_dynamic::dynamic_object1#2\[\[5\]\] =
9+
symex_dynamic::dynamic_object1#2\[\[6\]\] =
10+
symex_dynamic::dynamic_object1#2\[\[7\]\] =
11+
symex_dynamic::dynamic_object1#2\[\[8\]\] =
12+
symex_dynamic::dynamic_object1#2\[\[9\]\] =
1313
symex_dynamic::dynamic_object1#3\[\[1\]\] =
1414
^EXIT=0$
1515
^SIGNAL=0$

‎regression/cbmc/array-cell-sensitivity7/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
5-
main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
6-
main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
7-
main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
8-
main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
9-
main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
10-
main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
11-
main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
12-
main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
4+
main::1::array!0@1#2\[\[1\]\] =
5+
main::1::array!0@1#2\[\[2\]\] =
6+
main::1::array!0@1#2\[\[3\]\] =
7+
main::1::array!0@1#2\[\[4\]\] =
8+
main::1::array!0@1#2\[\[5\]\] =
9+
main::1::array!0@1#2\[\[6\]\] =
10+
main::1::array!0@1#2\[\[7\]\] =
11+
main::1::array!0@1#2\[\[8\]\] =
12+
main::1::array!0@1#2\[\[9\]\] =
1313
main::1::array!0@1#3\[\[0\]\] =
1414
^EXIT=0$
1515
^SIGNAL=0$

‎regression/cbmc/array-cell-sensitivity8/test.desc

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,26 @@
11
CORE
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
5-
main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
6-
main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
7-
main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
8-
main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
9-
main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
10-
main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
11-
main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
12-
main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
4+
main::1::array!0@1#2\[\[1\]\] =
5+
main::1::array!0@1#2\[\[2\]\] =
6+
main::1::array!0@1#2\[\[3\]\] =
7+
main::1::array!0@1#2\[\[4\]\] =
8+
main::1::array!0@1#2\[\[5\]\] =
9+
main::1::array!0@1#2\[\[6\]\] =
10+
main::1::array!0@1#2\[\[7\]\] =
11+
main::1::array!0@1#2\[\[8\]\] =
12+
main::1::array!0@1#2\[\[9\]\] =
1313
main::1::array!0@1#2 =.*byte_extract_little_endian
14-
main::1::array!0@1#3\[\[0\]\] = main::1::array!0@1#2\[0\]
15-
main::1::array!0@1#3\[\[1\]\] = main::1::array!0@1#2\[1\]
16-
main::1::array!0@1#3\[\[2\]\] = main::1::array!0@1#2\[2\]
17-
main::1::array!0@1#3\[\[3\]\] = main::1::array!0@1#2\[3\]
18-
main::1::array!0@1#3\[\[4\]\] = main::1::array!0@1#2\[4\]
19-
main::1::array!0@1#3\[\[5\]\] = main::1::array!0@1#2\[5\]
20-
main::1::array!0@1#3\[\[6\]\] = main::1::array!0@1#2\[6\]
21-
main::1::array!0@1#3\[\[7\]\] = main::1::array!0@1#2\[7\]
22-
main::1::array!0@1#3\[\[8\]\] = main::1::array!0@1#2\[8\]
23-
main::1::array!0@1#3\[\[9\]\] = main::1::array!0@1#2\[9\]
14+
main::1::array!0@1#3\[\[0\]\] =
15+
main::1::array!0@1#3\[\[1\]\] =
16+
main::1::array!0@1#3\[\[2\]\] =
17+
main::1::array!0@1#3\[\[3\]\] =
18+
main::1::array!0@1#3\[\[4\]\] =
19+
main::1::array!0@1#3\[\[5\]\] =
20+
main::1::array!0@1#3\[\[6\]\] =
21+
main::1::array!0@1#3\[\[7\]\] =
22+
main::1::array!0@1#3\[\[8\]\] =
23+
main::1::array!0@1#3\[\[9\]\] =
2424
^EXIT=0$
2525
^SIGNAL=0$
2626
--

‎regression/cbmc/array-cell-sensitivity9/test.desc

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,27 @@
11
CORE
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
5-
main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
6-
main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
7-
main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
8-
main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
9-
main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
10-
main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
11-
main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
12-
main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
13-
main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
4+
main::1::array!0@1#2\[\[0\]\]..x =
5+
main::1::array!0@1#2\[\[1\]\]..x =
6+
main::1::array!0@1#2\[\[2\]\]..x =
7+
main::1::array!0@1#2\[\[3\]\]..x =
8+
main::1::array!0@1#2\[\[4\]\]..x =
9+
main::1::array!0@1#2\[\[5\]\]..x =
10+
main::1::array!0@1#2\[\[6\]\]..x =
11+
main::1::array!0@1#2\[\[7\]\]..x =
12+
main::1::array!0@1#2\[\[8\]\]..x =
13+
main::1::array!0@1#2\[\[9\]\]..x =
1414
main::1::array!0@1#3\[\[1\]\]..x =
15-
main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
16-
main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
17-
main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
18-
main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
19-
main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
20-
main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
21-
main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
22-
main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
23-
main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
24-
main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
15+
main::1::array!0@1#2\[\[0\]\]..y =
16+
main::1::array!0@1#2\[\[1\]\]..y =
17+
main::1::array!0@1#2\[\[2\]\]..y =
18+
main::1::array!0@1#2\[\[3\]\]..y =
19+
main::1::array!0@1#2\[\[4\]\]..y =
20+
main::1::array!0@1#2\[\[5\]\]..y =
21+
main::1::array!0@1#2\[\[6\]\]..y =
22+
main::1::array!0@1#2\[\[7\]\]..y =
23+
main::1::array!0@1#2\[\[8\]\]..y =
24+
main::1::array!0@1#2\[\[9\]\]..y =
2525
^EXIT=0$
2626
^SIGNAL=0$
2727
--

‎regression/cbmc/field-sensitivity14/main.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <string.h>
2+
3+
struct S
4+
{
5+
int x;
6+
int y;
7+
};
8+
9+
int main()
10+
{
11+
struct S s1, s2, s3;
12+
13+
s1.y = 42;
14+
memcpy(&s2, &s1, sizeof(struct S));
15+
__CPROVER_assert(s2.y == 42, "should propagate");
16+
17+
s3.x = 42;
18+
memcpy(&s2, &s3, sizeof(struct S));
19+
__CPROVER_assert(s2.x == 42, "should propagate");
20+
}

‎regression/cbmc/field-sensitivity14/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
4+
^Generated \d+ VCC\(s\), 0 remaining after simplification$
5+
^VERIFICATION SUCCESSFUL$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
--
10+
All properties in this example can be solved by combining field-sensitive
11+
constant propagation and simplification.

0 commit comments

Comments
 (0)