Skip to content

Commit

Permalink
Add regression test for NullPointerException
Browse files Browse the repository at this point in the history
The new test is similar to NullPointerException2. It checks that a
NullPointerException is correctly caught if the catch block specifies
one of its superclasses.
  • Loading branch information
antlechner committed Dec 5, 2017
1 parent 41d77f4 commit 379e415
Show file tree
Hide file tree
Showing 8 changed files with 32 additions and 0 deletions.
Binary file added regression/cbmc-java/NullPointerException4/A.class
Binary file not shown.
Binary file not shown.
15 changes: 15 additions & 0 deletions regression/cbmc-java/NullPointerException4/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
class A {
int i;
}

public class Test {
public static void main(String args[]) {
A a=null;
try {
a.i=0;
}
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 NullPointerException 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/NullPointerException4/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
Test.class
--java-throw-runtime-exceptions
^EXIT=10$
^SIGNAL=0$
^.*assertion at file Test.java line 12 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring

0 comments on commit 379e415

Please sign in to comment.