diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index f00a0bfb17c..36ad3bff30d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -279,6 +279,7 @@ void java_bytecode_convert_classt::convert( class_type.set_is_inner_class(c.is_inner_class); class_type.set_is_static_class(c.is_static_class); class_type.set_is_anonymous_class(c.is_anonymous_class); + class_type.set_outer_class(c.outer_class); if(c.is_enum) { if(max_array_length != 0 && c.enum_elements > max_array_length) diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 431dd4804f5..29b3bb056a5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -221,6 +221,7 @@ class java_bytecode_parse_treet bool is_static_class = false; bool is_anonymous_class = false; bool attribute_bootstrapmethods_read = false; + irep_idt outer_class; // when no outer class is set, there is no outer class size_t enum_elements=0; enum class method_handle_typet diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 8bcb491939e..0ac957a849b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1643,6 +1643,11 @@ void java_bytecode_parsert::rinner_classes_attribute( } else { + std::string outer_class_info_name = + class_infot(pool_entry(outer_class_info_index)) + .get_name(pool_entry_lambda); + parsed_class.outer_class = + constant(outer_class_info_index).type().get(ID_C_base_name); parsed_class.is_private = is_private; parsed_class.is_protected = is_protected; parsed_class.is_public = is_public; diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 8e9f092eee6..a82f30a260e 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -121,6 +121,16 @@ class java_class_typet:public class_typet return set(ID_is_inner_class, is_inner_class); } + const irep_idt get_outer_class() const + { + return get(ID_outer_class); + } + + void set_outer_class(irep_idt outer_class) + { + return set(ID_outer_class, outer_class); + } + const bool get_is_static_class() const { return get_bool(ID_is_static); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e2d7d160112..bcc6a8f6906 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -675,6 +675,7 @@ IREP_ID_ONE(interface) IREP_ID_TWO(C_must_not_throw, #must_not_throw) IREP_ID_ONE(is_inner_class) IREP_ID_ONE(is_anonymous) +IREP_ID_ONE(outer_class) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.h in their source tree and