Skip to content

Commit 7e28299

Browse files
committed
Add parsing of the names of inner java classes
This is required for correctly printing the names of inner classes.
1 parent 8065b10 commit 7e28299

File tree

5 files changed

+17
-1
lines changed

5 files changed

+17
-1
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -303,6 +303,7 @@ void java_bytecode_convert_classt::convert(
303303
}
304304

305305
class_type.set_tag(c.name);
306+
class_type.set_inner_name(c.inner_name);
306307
class_type.set(ID_abstract, c.is_abstract);
307308
class_type.set(ID_is_annotation, c.is_annotation);
308309
class_type.set(ID_interface, c.is_interface);

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,7 @@ struct java_bytecode_parse_treet
213213
classt &operator=(classt &&) = default;
214214
#endif
215215

216-
irep_idt name, super_class;
216+
irep_idt name, super_class, inner_name;
217217
bool is_abstract=false;
218218
bool is_enum=false;
219219
bool is_public=false, is_protected=false, is_private=false;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1696,6 +1696,8 @@ void java_bytecode_parsert::rinner_classes_attribute(
16961696
// This is a marker that a class is anonymous.
16971697
if(inner_name_index == 0)
16981698
parsed_class.is_anonymous_class = true;
1699+
else
1700+
parsed_class.inner_name = pool_entry_lambda(inner_name_index).s;
16991701
// Note that if outer_class_info_index == 0, the inner class is an anonymous
17001702
// or local class, and is treated as private.
17011703
if(outer_class_info_index == 0)

jbmc/src/java_bytecode/java_types.h

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -241,6 +241,18 @@ class java_class_typet:public class_typet
241241
{
242242
set(ID_name, name);
243243
}
244+
245+
/// Get the name of a java inner class.
246+
const irep_idt &get_inner_name() const
247+
{
248+
return get(ID_inner_name);
249+
}
250+
251+
/// Set the name of a java inner class.
252+
void set_inner_name(const irep_idt &name)
253+
{
254+
set(ID_inner_name, name);
255+
}
244256
};
245257

246258
inline const java_class_typet &to_java_class_type(const typet &type)

src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,7 @@ IREP_ID_ONE(incomplete_c_enum)
131131
IREP_ID_TWO(C_incomplete, #incomplete)
132132
IREP_ID_ONE(identifier)
133133
IREP_ID_ONE(name)
134+
IREP_ID_ONE(inner_name)
134135
IREP_ID_ONE(cpp_name)
135136
IREP_ID_ONE(component_cpp_name)
136137
IREP_ID_TWO(C_id_class, #id_class)

0 commit comments

Comments
 (0)