+ passing test checking NULL object dereferencing in Java

Author: cristina-david

regression/cbmc-java/pointer_check1/A.class

@@ -0,0 +1,16 @@
+class A {
+  int val;
+}
+
+class B {
+  int getVal(A a) {
+    return a.val;
+  }
+}
+
+class pointer_check1 {
+  public static void main(String[] args) {
+    B b = new B();
+    int myval = b.getVal(null);
+  }
+}

regression/cbmc-java/pointer_check1/B.class

@@ -0,0 +1,8 @@
+CORE
+pointer_check1.class
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring