Skip to content

Commit 52e46c3

Browse files
Add a test with array in generic type
The JBMC behavior could be changed by array cell propagation in this case, so a test is needed to ensure we do not introduce a bug.
1 parent ea615af commit 52e46c3

File tree

4 files changed

+27
-0
lines changed

4 files changed

+27
-0
lines changed
363 Bytes
Binary file not shown.
Binary file not shown.
723 Bytes
Binary file not shown.
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
class Generic<T> {
2+
public T field;
3+
public Generic(T fieldParam) {
4+
field = fieldParam;
5+
}
6+
}
7+
8+
class IntWrapper {
9+
public int i0;
10+
public IntWrapper(int intParam) {
11+
i0 = intParam;
12+
}
13+
}
14+
15+
public class Test {
16+
public static int test(Generic<IntWrapper[]> arrayInput, boolean triggerAssertion) {
17+
if (arrayInput != null
18+
&& arrayInput.field != null
19+
&& arrayInput.field.length > 0
20+
&& arrayInput.field[0] != null) {
21+
assert(!triggerAssertion);
22+
return arrayInput.field[0].i0;
23+
} else {
24+
return -1;
25+
}
26+
}
27+
}

0 commit comments

Comments
 (0)