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

smowton · smowton · commit 4cd4cf37b25f · 2019-03-05T14:32:40.000Z
fieldref_exprt confused ID_nil with ID_empty_string and therefore rejected "class nil { int nil; }" for example.
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -352,7 +352,8 @@ 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) != ID_empty_string &&
+    base.get(ID_component_name) != ID_empty_string;
 }
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H

Original file line number	Diff line number	Diff line change
`@@ -352,7 +352,8 @@ class fieldref_exprt : public exprt`
`352`	`352`	`template <>`
`353`	`353`	`inline bool can_cast_expr<fieldref_exprt>(const exprt &base)`
`354`	`354`	`{`
`355`		`- return base.get(ID_class) != ID_nil && base.get(ID_component_name) != ID_nil;`
	`355`	`+ return base.get(ID_class) != ID_empty_string &&`
	`356`	`+ base.get(ID_component_name) != ID_empty_string;`
`356`	`357`	`}`
`357`	`358`
`358`	`359`	`#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H`