Complete instanceof for Java.

The current implementation did not consider correctly the case of `null` in
`ID_java_instanceof`. An instanceof with `null` always fails. For `a instanceof
B` this now adds `a != null` to the condition.

Author: Matthias Güdemann

src/goto-programs/remove_instanceof.cpp

@@ -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;
 }