Merge pull request #1197 from smowton/smowton/feature/virtual_call_null_check

Add more NullPointerException throw sites

Author: smowton

regression/cbmc-java/NondetArray2/NondetArray2.class

@@ -8,6 +8,8 @@ void main()
 
     int num = 0;
     for (Integer i : ints) {
+      if(i == null)
+        continue;
       num *= i.intValue();
     }
     assert num == 0;

regression/cbmc-java/NondetArray2/NondetArray2.java

@@ -9,6 +9,8 @@ void main()
 
     int num = 0;
     for (Integer i : ints) {
+      if(i == null)
+        continue;
       num *= i.intValue();
     }
     assert num == 0;

regression/cbmc-java/NondetArray3/NondetArray3.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/NondetArray3/NondetArray3.java

@@ -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.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 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.