Merge pull request #1716 from mgudemann/fix/null_check_for_java_instanceof

[TG-1793] Complete instanceof for Java.

Author: Matthias Güdemann

regression/cbmc-java/instanceof8/InstanceOf8.class

@@ -0,0 +1,14 @@
+public class InstanceOf8 {
+  public static boolean test(Integer i) {
+    if (i instanceof Integer) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+  public static void main(String[] args)
+  {
+    assert(!test(null));
+    assert(test(new Integer(1)));
+  }
+}

regression/cbmc-java/instanceof8/InstanceOf8.java

@@ -0,0 +1,7 @@
+CORE
+InstanceOf8.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc-java/instanceof8/test.desc

@@ -113,15 +113,20 @@ std::size_t remove_instanceoft::lower_instanceof(
   newinst->source_location=this_inst->source_location;
   newinst->function=this_inst->function;
 
-  // Replace the instanceof construct with a big-or.
+  // Replace the instanceof construct with a conjunction of non-null and the
+  // disjunction of all possible object types. According to the Java
+  // specification, null instanceof T is false for all possible values of T.
+  // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
+  notequal_exprt non_null_expr(
+    check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type())));
   exprt::operandst or_ops;
   for(const auto &clsname : children)
   {
     constant_exprt clsexpr(clsname, string_typet());
     equal_exprt test(newsym.symbol_expr(), clsexpr);
     or_ops.push_back(test);
   }
-  expr=disjunction(or_ops);
+  expr = and_exprt(non_null_expr, disjunction(or_ops));
 
   return 1;
 }