check null references on method invokation

Author: Daniel Kroening

regression/cbmc-java/NullPointer2/NullPointer2.class

@@ -0,0 +1,12 @@
+public class NullPointer2 {
+
+  static Object my_field;
+
+  public static void main(String[] args)
+  {
+    int z;
+    
+    z=my_field.hashCode(); // NULL pointer dereference 
+  }
+
+}

regression/cbmc-java/NullPointer2/NullPointer2.java

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