Skip to content

Commit 677f39d

Browse files
committed
Add zero-length array test
This should compile warning-free, since it is legal Java. Previously an array_of expression with nil length yielded a warning, as would a WITH based upon one.
1 parent 40fb6a0 commit 677f39d

File tree

3 files changed

+22
-0
lines changed

3 files changed

+22
-0
lines changed
315 Bytes
Binary file not shown.

regression/cbmc-java/array2/test.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.class
3+
--function test.f --cover location
4+
\d+ of \d+ covered
5+
--
6+
^warning: ignoring

regression/cbmc-java/array2/test.java

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
public class test {
2+
3+
public void f(int unknown) {
4+
5+
int[] arr;
6+
if(unknown > 0)
7+
arr = new int[1];
8+
else
9+
arr = new int[0];
10+
11+
if(unknown > 0)
12+
arr[0]=1;
13+
14+
}
15+
16+
}

0 commit comments

Comments
 (0)