Skip to content

Commit 8e145fa

Browse files
author
Daniel Kroening
authored
Merge pull request #3649 from allredj/loop-less-array-init
Loop-less initialization of primitive arrays
2 parents 7b0887f + 2d24bbd commit 8e145fa

15 files changed

+376
-57
lines changed

‎jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.class

1.46 KB
Binary file not shown.

‎jbmc/regression/jbmc/NondetArrayPrimitive/NondetArrayPrimitive.java

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
class NondetArrayPrimitive
2+
{
3+
void intArray(int[] array)
4+
{
5+
if (array != null && array.length > 1500 && array[1500] == 42) {
6+
assert false;
7+
}
8+
}
9+
10+
void floatArray(float[] array)
11+
{
12+
if (array != null && array.length > 1500 && array[1500] == 42.0) {
13+
assert false;
14+
}
15+
}
16+
17+
void charArray(char[] array)
18+
{
19+
if (array != null && array.length > 1500 && array[1500] == 'f') {
20+
assert false;
21+
}
22+
}
23+
24+
void doubleArray(double[] array)
25+
{
26+
if (array != null && array.length > 1500 && array[1500] == 42.0) {
27+
assert false;
28+
}
29+
}
30+
31+
void longArray(long[] array)
32+
{
33+
if (array != null && array.length > 1500 && array[1500] == 42) {
34+
assert false;
35+
}
36+
}
37+
38+
void shortArray(short[] array)
39+
{
40+
if (array != null && array.length > 1500 && array[1500] == 42) {
41+
assert false;
42+
}
43+
}
44+
45+
void byteArray(byte[] array)
46+
{
47+
if (array != null && array.length > 1500 && array[1500] == 42) {
48+
assert false;
49+
}
50+
}
51+
52+
void boolArray(boolean[] array)
53+
{
54+
if (array != null && array.length > 1500 && array[1500] == true) {
55+
assert false;
56+
}
57+
}
58+
59+
void intArrayMulti(int[][] array)
60+
{
61+
if (array != null &&
62+
array.length > 2 &&
63+
array[2].length > 50 &&
64+
array[2][50] == 42) {
65+
assert false;
66+
}
67+
}
68+
69+
}

‎jbmc/regression/jbmc/NondetArrayPrimitive/boolArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.boolArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 55 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/NondetArrayPrimitive/byteArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.byteArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 48 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/NondetArrayPrimitive/charArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.charArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 20 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/NondetArrayPrimitive/doubleArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.doubleArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 27 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/NondetArrayPrimitive/floatArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.floatArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 13 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/NondetArrayPrimitive/intArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.intArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 6 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/NondetArrayPrimitive/intArrayMulti.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.intArrayMulti --max-nondet-array-length 51 --unwind 4
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 65 assertion.*: FAILURE
8+
--
9+
^warning: ignoring
10+
--
11+
Check inner most array of multi-dimensional array is reachable independently of
12+
--unwind value.

‎jbmc/regression/jbmc/NondetArrayPrimitive/longArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.longArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 34 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/NondetArrayPrimitive/shortArray.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
NondetArrayPrimitive.class
3+
--function NondetArrayPrimitive.shortArray --max-nondet-array-length 2000 --unwind 1
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
line 41 assertion.*: FAILURE
8+
--
9+
Unwinding loop __CPROVER__start.0 iteration 2
10+
^warning: ignoring
11+
--
12+
Check no unwind needed to reach non-primitive array cell

‎jbmc/regression/jbmc/json_trace3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Test.class
44
activate-multi-line-match
55
EXIT=10
66
SIGNAL=0
7-
"lhs": "dynamic_2_array\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
7+
"lhs": "dynamic_object3\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
88
--
99
"name": "unknown"
1010
^warning: ignoring

0 commit comments

Comments
 (0)