Merge pull request #106 from cristina-david/java_pointer_check

Java pointer checks

Author: Daniel Kroening

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

regression/cbmc-java/missing_class1/missing_class1.java

@@ -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/missing_class1/test.desc

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

regression/cbmc-java/pointer_check1/A.class

@@ -944,23 +944,32 @@ void goto_checkt::pointer_validity_check(
       expr,
       guard);
 
-  if(flags.is_unknown() || flags.is_dynamic_heap())
-    add_guarded_claim(
-      not_exprt(deallocated(pointer, ns)),
-      "dereference failure: deallocated dynamic object",
-      "pointer dereference",
-      expr.find_source_location(),
-      expr,
-      guard);
+  symbol_tablet symbol_table = ns.get_symbol_table();
 
-  if(flags.is_unknown() || flags.is_dynamic_local())
-    add_guarded_claim(
-      not_exprt(dead_object(pointer, ns)),
-      "dereference failure: dead object",
-      "pointer dereference",
-      expr.find_source_location(),
-      expr,
-      guard);
+  symbol_tablet::symbolst::iterator s_it =
+    symbol_table.symbols.find(CPROVER_PREFIX "initialize");
+
+  // For Java don't check dereference of a deallocated or dead object
+  if (s_it == symbol_table.symbols.end() || (s_it->second).mode != ID_java)
+  {
+    if(flags.is_unknown() || flags.is_dynamic_heap())
+      add_guarded_claim(
+        not_exprt(deallocated(pointer, ns)),
+        "dereference failure: deallocated dynamic object",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
+
+    if(flags.is_unknown() || flags.is_dynamic_local())
+      add_guarded_claim(
+        not_exprt(dead_object(pointer, ns)),
+        "dereference failure: dead object",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
+  }
 
   if(enable_bounds_check)
   {