Skip to content

Commit 4259db2

Browse files
Add a test with array of negative size
This tests that defining an array with negative size does not make JBMC crash.
1 parent d6da909 commit 4259db2

File tree

3 files changed

+20
-0
lines changed

3 files changed

+20
-0
lines changed
Binary file not shown.
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Test {
2+
public static void check(Integer t) {
3+
if (t != null)
4+
try {
5+
Integer[] arr = new Integer[-7];
6+
assert false;
7+
} catch (NegativeArraySizeException e) {
8+
assert false;
9+
}
10+
}
11+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
Test.class
3+
--function Test.check
4+
line 5 Array size should be >= 0: FAILURE
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
Test that defining an array with negative size does not crash JBMC

0 commit comments

Comments
 (0)