more tests for NullPointer

Author: Daniel Kroening

regression/cbmc-java/NullPointer3/NullPointer3.class

@@ -0,0 +1,8 @@
+public class NullPointer3 {
+
+  public static void main(String[] args)
+  {
+    throw null; // NULL pointer dereference
+  }
+
+}

regression/cbmc-java/NullPointer3/NullPointer3.java

@@ -0,0 +1,9 @@
+KNOWNBUG
+NullPointer3.class
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^  file NullPointer3.java line 5$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NullPointer3/test.desc

@@ -0,0 +1,9 @@
+public class NullPointer4 {
+
+  public static void main(String[] args)
+  {
+    int array[]=null;
+    int s=array.length; // NULL pointer dereference
+  }
+
+}

regression/cbmc-java/NullPointer4/NullPointer4.class

@@ -0,0 +1,9 @@
+CORE
+NullPointer4.class
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^  file NullPointer4.java line 6$
+^VERIFICATION FAILED$
+--
+^warning: ignoring