Merge pull request diffblue#1856 from thk123/refactor/fieldref_expr

Introduce fieldref_exprt to represent a field reference

Author: Thomas Kiley

src/java_bytecode/java_bytecode_parse_tree.h

@@ -222,4 +222,21 @@ class java_bytecode_parse_treet
   }
 };
 
+/// Represents the argument of an instruction that uses a CONSTANT_Fieldref
+/// This is used for example as an argument to a getstatic and putstatic
+/// instruction
+class fieldref_exprt : public exprt
+{
+public:
+  fieldref_exprt(
+    const typet &type,
+    const irep_idt &component_name,
+    const irep_idt &class_name)
+    : exprt(ID_empty_string, type)
+  {
+    set(ID_class, class_name);
+    set(ID_component_name, component_name);
+  }
+};
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H

src/java_bytecode/java_bytecode_parser.cpp

@@ -537,9 +537,8 @@ void java_bytecode_parsert::rconstant_pool()
         symbol_typet class_symbol=
           java_classname(id2string(class_name_entry.s));
 
-        exprt fieldref("fieldref", type);
-        fieldref.set(ID_class, class_symbol.get_identifier());
-        fieldref.set(ID_component_name, name_entry.s);
+        fieldref_exprt fieldref(
+          type, name_entry.s, class_symbol.get_identifier());
 
         it->expr=fieldref;
       }