introduce java_class_typet::componentt

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -375,7 +375,7 @@ void java_bytecode_convert_classt::convert(
     {
       class_type.add_base(base);
     }
-    class_typet::componentt base_class_field;
+    java_class_typet::componentt base_class_field;
     base_class_field.type() = class_type.bases().at(0).type();
     base_class_field.set_name("@" + id2string(c.super_class));
     base_class_field.set_base_name("@" + id2string(c.super_class));
@@ -740,10 +740,10 @@ void java_bytecode_convert_classt::convert(
   }
   else
   {
-    class_typet &class_type=to_class_type(class_symbol.type);
+    auto &class_type = to_java_class_type(class_symbol.type);
 
     class_type.components().emplace_back();
-    class_typet::componentt &component=class_type.components().back();
+    auto &component = class_type.components().back();
 
     component.set_name(f.name);
     component.set_base_name(f.name);
@@ -798,18 +798,18 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     class_type.set_name(struct_tag_type_identifier);
 
     class_type.components().reserve(3);
-    class_typet::componentt base_class_component(
+    java_class_typet::componentt base_class_component(
       "@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
     base_class_component.set_pretty_name("@java.lang.Object");
     base_class_component.set_base_name("@java.lang.Object");
     class_type.components().push_back(base_class_component);
 
-    class_typet::componentt length_component("length", java_int_type());
+    java_class_typet::componentt length_component("length", java_int_type());
     length_component.set_pretty_name("length");
     length_component.set_base_name("length");
     class_type.components().push_back(length_component);
 
-    class_typet::componentt data_component(
+    java_class_typet::componentt data_component(
       "data", java_reference_type(java_type_from_char(l)));
     data_component.set_pretty_name("data");
     data_component.set_base_name("data");

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -332,7 +332,7 @@ static void infer_opaque_type_fields(
             symbolt &writable_class_symbol =
               symbol_table.get_writeable_ref(class_symbol_id);
             auto &components =
-              to_struct_type(writable_class_symbol.type).components();
+              to_java_class_type(writable_class_symbol.type).components();
             components.emplace_back(component_name, fieldref.type());
             components.back().set_base_name(component_name);
             components.back().set_pretty_name(component_name);

jbmc/src/java_bytecode/java_types.h

@@ -101,7 +101,60 @@ inline bool can_cast_type<annotated_typet>(const typet &)
 
 class java_class_typet:public class_typet
 {
- public:
+public:
+  class componentt : public class_typet::componentt
+  {
+  public:
+    componentt() = default;
+
+    componentt(const irep_idt &_name, typet _type)
+      : class_typet::componentt(_name, std::move(_type))
+    {
+    }
+
+    /// is a method or field 'final'?
+    bool get_is_final() const
+    {
+      return get_bool(ID_final);
+    }
+
+    /// is a method or field 'final'?
+    void set_is_final(const bool is_final)
+    {
+      set(ID_final, is_final);
+    }
+
+    /// is a method 'native'?
+    bool get_is_native() const
+    {
+      return get_bool(ID_is_native_method);
+    }
+
+    /// marks a method as 'native'
+    void set_is_native(const bool is_native)
+    {
+      set(ID_is_native_method, is_native);
+    }
+  };
+
+  using componentst = std::vector<componentt>;
+
+  const componentst &components() const
+  {
+    return (const componentst &)(find(ID_components).get_sub());
+  }
+
+  componentst &components()
+  {
+    return (componentst &)(add(ID_components).get_sub());
+  }
+
+  const componentt &get_component(const irep_idt &component_name) const
+  {
+    return static_cast<const componentt &>(
+      class_typet::get_component(component_name));
+  }
+
   const irep_idt &get_access() const
   {
     return get(ID_access);

jbmc/unit/java-testing-utils/require_type.cpp

@@ -30,11 +30,30 @@ pointer_typet require_type::require_pointer(
   return pointer;
 }
 
+/// Checks that a class has a component with a specific name
+/// \param java_class_type: The class that should have the component
+/// \param component_name: The name of the component
+/// \return The component with the specified name
+java_class_typet::componentt require_type::require_component(
+  const java_class_typet &java_class_type,
+  const irep_idt &component_name)
+{
+  const auto &component = std::find_if(
+    java_class_type.components().begin(),
+    java_class_type.components().end(),
+    [&component_name](const java_class_typet::componentt &component) {
+      return component.get_name() == component_name;
+    });
+
+  REQUIRE(component != java_class_type.components().end());
+  return *component;
+}
+
 /// Checks a struct like type has a component with a specific name
 /// \param struct_type: The structure that should have the component
 /// \param component_name: The name of the component
 /// \return The component with the specified name
-struct_union_typet::componentt require_type::require_component(
+struct_typet::componentt require_type::require_component(
   const struct_typet &struct_type,
   const irep_idt &component_name)
 {

jbmc/unit/java-testing-utils/require_type.h

@@ -32,6 +32,10 @@ const pointer_typet require_pointer_to_tag(
   const typet &type,
   const irep_idt &identifier = irep_idt());
 
+java_class_typet::componentt require_component(
+  const java_class_typet &java_class_type,
+  const irep_idt &component_name);
+
 struct_typet::componentt require_component(
   const struct_typet &struct_type,
   const irep_idt &component_name);

jbmc/unit/java_bytecode/java_bytecode_language/language.cpp

@@ -36,9 +36,9 @@ SCENARIO(
       {
         const symbolt &opaque_class_symbol =
           symbol_table.lookup_ref(opaque_class_prefix);
-        const struct_typet &opaque_class_struct =
-          to_struct_type(opaque_class_symbol.type);
-        const struct_union_typet::componentt &field =
+        const auto &opaque_class_struct =
+          to_java_class_type(opaque_class_symbol.type);
+        const auto &field =
           require_type::require_component(opaque_class_struct, "field2");
         REQUIRE(field.get_is_final());
       }

src/util/std_types.h

@@ -123,16 +123,6 @@ class struct_union_typet:public typet
     {
       return set(ID_C_is_padding, is_padding);
     }
-
-    bool get_is_final() const
-    {
-      return get_bool(ID_final);
-    }
-
-    void set_is_final(const bool is_final)
-    {
-      set(ID_final, is_final);
-    }
   };
 
   typedef std::vector<componentt> componentst;