diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index 8470d0cb864..bf5b36c5a2b 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/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 diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 93dba637f5a..54d70bbfac5 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/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; }