Skip to content

Commit

Permalink
Add test for NegativeArraySizeException
Browse files Browse the repository at this point in the history
The new test is similar to NegativeArraySizeException1 (was called
NegativeArraySizeException before the previous commit). It checks that a
NegativeArraySizeException is correctly caught if the catch block
specifies one of its superclasses.
  • Loading branch information
antlechner committed Dec 5, 2017
1 parent 9cc3192 commit 94a6ad4
Show file tree
Hide file tree
Showing 7 changed files with 27 additions and 0 deletions.
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
public class NegativeArraySizeExceptionTest {
public static void main(String args[]) {
try {
int a[]=new int[-1];
}
catch (Exception exc) {
assert false;
}
}
}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
package java.lang;

public class NegativeArraySizeException extends RuntimeException {
}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
package java.lang;

public class RuntimeException extends Exception {
}
9 changes: 9 additions & 0 deletions regression/cbmc-java/NegativeArraySizeException2/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
NegativeArraySizeExceptionTest.class
--java-throw-runtime-exceptions
^EXIT=10$
^SIGNAL=0$
^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring

0 comments on commit 94a6ad4

Please sign in to comment.