Merge pull request #4329 from smowton/smowton/fix/tolerate-nil-names

Java: tolerate fields and classes with the name "nil"

Author: smowton

jbmc/regression/jbmc/nil-names/nil.class

@@ -0,0 +1,9 @@
+public class nil {
+
+  int nil;
+
+  public int getNil() {
+    return nil;
+  }
+
+}

jbmc/regression/jbmc/nil-names/nil.java

@@ -0,0 +1,8 @@
+CORE
+nil.class
+--function nil.getNil
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+std::bad_cast

jbmc/regression/jbmc/nil-names/test.desc

@@ -352,7 +352,7 @@ class fieldref_exprt : public exprt
 template <>
 inline bool can_cast_expr<fieldref_exprt>(const exprt &base)
 {
-  return base.get(ID_class) != ID_nil && base.get(ID_component_name) != ID_nil;
+  return !base.get(ID_class).empty() && !base.get(ID_component_name).empty();
 }
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H