Skip to content

Commit b09b664

Browse files
tautschnigtautschnig
authored
Merge pull request #6856 from tautschnig/feature/field-propagation
Constant propagation for individual fields through byte extract
2 parents 7bfbfce + 6193534 commit b09b664

File tree

30 files changed

+306
-194
lines changed

30 files changed

+306
-194
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-incr-oneloop/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,10 @@ default: tests.log
22

33
# Note the `perl -e` serves the purpose of providing timeout
44
test:
5-
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
5+
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
66

77
tests.log: ../test.pl
8-
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
8+
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
99

1010
clean:
1111
@$(RM) *.log

‎regression/cbmc/Array_UF22/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG broken-smt-backend
22
main.c
3-
--arrays-uf-always --no-propagation
3+
--arrays-uf-always --no-propagation --no-simplify
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

‎regression/cbmc/Pointer21/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--pointer-check
44
^EXIT=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
--

0 commit comments

Comments
 (0)