Skip to content

Commit 2ba794d

Browse files
author
thk123
committed
Introduce fieldref_exprt to represent a field reference
1 parent c62b957 commit 2ba794d

File tree

3 files changed

+20
-3
lines changed

3 files changed

+20
-3
lines changed

src/java_bytecode/java_bytecode_parse_tree.h

+17
Original file line numberDiff line numberDiff line change
@@ -222,4 +222,21 @@ class java_bytecode_parse_treet
222222
}
223223
};
224224

225+
/// Represents the argument of an instruction that uses a CONSTANT_Fieldref
226+
/// This is used for example as an argument to a getstatic and putstatic
227+
/// instruction
228+
class fieldref_exprt : public exprt
229+
{
230+
public:
231+
fieldref_exprt(
232+
const typet &type,
233+
const irep_idt &component_name,
234+
const irep_idt &class_name)
235+
: exprt(ID_fieldref, type)
236+
{
237+
set(ID_class, class_name);
238+
set(ID_component_name, component_name);
239+
}
240+
};
241+
225242
#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H

src/java_bytecode/java_bytecode_parser.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -537,9 +537,8 @@ void java_bytecode_parsert::rconstant_pool()
537537
symbol_typet class_symbol=
538538
java_classname(id2string(class_name_entry.s));
539539

540-
exprt fieldref("fieldref", type);
541-
fieldref.set(ID_class, class_symbol.get_identifier());
542-
fieldref.set(ID_component_name, name_entry.s);
540+
fieldref_exprt fieldref(
541+
type, name_entry.s, class_symbol.get_identifier());
543542

544543
it->expr=fieldref;
545544
}

src/util/irep_ids.def

+1
Original file line numberDiff line numberDiff line change
@@ -840,6 +840,7 @@ IREP_ID_TWO(type_variables, #type_variables)
840840
IREP_ID_ONE(havoc_object)
841841
IREP_ID_TWO(overflow_shl, overflow-shl)
842842
IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
843+
IREP_ID_ONE(fieldref)
843844

844845
#undef IREP_ID_ONE
845846
#undef IREP_ID_TWO

0 commit comments

Comments
 (0)