From 796f7e15251be6ba356e54c92d3764e118033d92 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Tue, 5 Mar 2019 14:32:40 +0000
Subject: [PATCH] Java: tolerate fields and classes with the name "nil"

fieldref_exprt confused ID_nil with ID_empty_string and therefore rejected "class nil { int nil; }" for example.
---
 jbmc/regression/jbmc/nil-names/nil.class          | Bin 0 -> 332 bytes
 jbmc/regression/jbmc/nil-names/nil.java           |   9 +++++++++
 jbmc/regression/jbmc/nil-names/test.desc          |   8 ++++++++
 jbmc/src/java_bytecode/java_bytecode_parse_tree.h |   2 +-
 4 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 jbmc/regression/jbmc/nil-names/nil.class
 create mode 100644 jbmc/regression/jbmc/nil-names/nil.java
 create mode 100644 jbmc/regression/jbmc/nil-names/test.desc

diff --git a/jbmc/regression/jbmc/nil-names/nil.class b/jbmc/regression/jbmc/nil-names/nil.class
new file mode 100644
index 0000000000000000000000000000000000000000..4c76ef5936e3743ca5da11896f292146b6a595dc
GIT binary patch
literal 332
zcmZur%}&B#5S)enK&?_xAHW-Opcii%E+!--4IVVyzm_lXk<uom_*7m@NJu#N06vsq
zTDeF(?CkFB%w)fR4qpHsaO=TBuZ<?IUDz&e1kKE(0+|S$CzF|SM5=#36IjprTnjpp
z$@Fx)j&<>-;*?A;$`h5&RAH+9L|Wz2Yy@`1xJPC!bUCepnZ;=DHQyGA9-GSFqGY&I
z@5+aZmJb__AgG8iRoNnZiB~!)amOz$el09Yhz-tk5Zl~B_WCy1Lq6-XM|5gZaKYLC
a6|i4&6I`J~{A=E!@o{E${xt`+s(S?SZ7+ZT

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/nil-names/nil.java b/jbmc/regression/jbmc/nil-names/nil.java
new file mode 100644
index 00000000000..2a17b7227b4
--- /dev/null
+++ b/jbmc/regression/jbmc/nil-names/nil.java
@@ -0,0 +1,9 @@
+public class nil {
+
+  int nil;
+
+  public int getNil() {
+    return nil;
+  }
+
+}
diff --git a/jbmc/regression/jbmc/nil-names/test.desc b/jbmc/regression/jbmc/nil-names/test.desc
new file mode 100644
index 00000000000..0d4dcf5bd46
--- /dev/null
+++ b/jbmc/regression/jbmc/nil-names/test.desc
@@ -0,0 +1,8 @@
+CORE
+nil.class
+--function nil.getNil
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+std::bad_cast
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
index 99e03329b87..72d0c07aab4 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
+++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -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