+ test failing to find a null pointer dereferencing when one of the classes is missing (pointer related assertions missing from the goto program)

Author: cristina-david

regression/cbmc-java/missing_class1/A.class

@@ -0,0 +1,16 @@
+class B {
+  int j;
+}
+ 
+class A {
+  int i;
+  B b;
+}
+
+public class missing_class1 {
+  public static void main(String[] args) {
+    A a = new A();
+    B b = a.b;
+    int j = b.j; // NULL pointer dereference
+  }
+}

regression/cbmc-java/missing_class1/missing_class1.class

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