Add tests for NullPointerException on virtual call or array access

Author: smowton

regression/cbmc-java/exceptions23/test.class

@@ -0,0 +1,12 @@
+CORE
+test.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+--
+^warning: ignoring
+--
+This test checks that accessing an array member, cf. a getfield or setfield bytecode,
+can produce a NullPointerException.

regression/cbmc-java/exceptions23/test.desc

@@ -0,0 +1,12 @@
+
+public class test {
+ public static void main () {
+   try {
+     int[] array = null;
+     int x = array[0];
+   }
+   catch(NullPointerException e) {
+     assert false;
+   }
+ }
+}

regression/cbmc-java/exceptions23/test.java

@@ -0,0 +1,12 @@
+CORE
+test.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 10: FAILURE
+--
+^warning: ignoring
+--
+This test ensures that attempting a virtual call against a null pointer can produce a NullPointerException,
+even when there are no field accesses inside the method or inspection of its class identifier to trigger one.

regression/cbmc-java/exceptions24/A.class

@@ -0,0 +1,18 @@
+
+public class test {
+ public static void main () {
+   try {
+     A a = null;
+     a.f();
+   }
+   catch(NullPointerException e) {
+     assert false;
+   }
+ }
+}
+
+class A {
+
+  public void f() {}
+
+}