Captures static inner class information

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -277,6 +277,7 @@ void java_bytecode_convert_classt::convert(
   class_type.set(ID_synthetic, c.is_synthetic);
   class_type.set_final(c.is_final);
   class_type.set_is_inner_class(c.is_inner_class);
+  class_type.set_is_static_class(c.is_static_class);
   if(c.is_enum)
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -218,6 +218,7 @@ class java_bytecode_parse_treet
     bool is_synthetic = false;
     bool is_annotation = false;
     bool is_inner_class = false;
+    bool is_static_class = false;
     bool attribute_bootstrapmethods_read = false;
     size_t enum_elements=0;
 

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1622,6 +1622,7 @@ void java_bytecode_parsert::rinner_classes_attribute(
     bool is_private = (inner_class_access_flags & ACC_PRIVATE) != 0;
     bool is_public = (inner_class_access_flags & ACC_PUBLIC) != 0;
     bool is_protected = (inner_class_access_flags & ACC_PROTECTED) != 0;
+    bool is_static = (inner_class_access_flags & ACC_STATIC) != 0;
 
     // If the original parsed class name matches the inner class name,
     // the parsed class is an inner class, so overwrite the parsed class'
@@ -1632,6 +1633,7 @@ void java_bytecode_parsert::rinner_classes_attribute(
       parsed_class.is_inner_class = is_inner_class;
     if(!is_inner_class)
       continue;
+    parsed_class.is_static_class = is_static;
     // Note that if outer_class_info_index == 0, the inner class is an anonymous
     // or local class, and is treated as private.
     if(outer_class_info_index == 0)

jbmc/src/java_bytecode/java_types.h

@@ -121,6 +121,17 @@ class java_class_typet:public class_typet
     return set(ID_is_inner_class, is_inner_class);
   }
 
+  const bool get_is_static_class() const
+  {
+    return get_bool(ID_is_static);
+  }
+
+  void set_is_static_class(const bool &is_static_class)
+  {
+    return set(ID_is_static, is_static_class);
+  }
+
+
   bool get_final()
   {
     return get_bool(ID_final);

jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java

@@ -0,0 +1,33 @@
+public class StaticInnerClass {
+    public static interface SomeInterface {
+        public int i = 0;
+    }
+    public static class PublicStaticInnerClass {
+        public int i;
+        public PublicStaticInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    public class PublicNonStaticInnerClass {
+        public int i;
+        public PublicNonStaticInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    public static SomeInterface staticAnonymousClass = new SomeInterface() {
+        public int i = 50;
+    };
+    public SomeInterface anonymousClass = new SomeInterface() {
+        public int i = 25;
+    };
+    public void testNonStatic() {
+        class LocalClassInNonStatic {
+            public int i = 1;
+        }
+    }
+    public static void testStatic() {
+        class LocalClassInStatic {
+            public int i = 2;
+        }
+    }
+}

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp

@@ -266,4 +266,92 @@ SCENARIO(
       }
     }
   }
+
+  const symbol_tablet &new_symbol_table =
+    load_java_class("StaticInnerClass", "./java_bytecode/java_bytecode_parser");
+  GIVEN("Some class with a static inner class")
+  {
+    WHEN("Parsing the InnerClasses attribute for a static inner class ")
+    {
+      THEN("The class should be marked as static")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::StaticInnerClass$PublicStaticInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_static_class());
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a non-static inner class ")
+    {
+      THEN("The class should not be marked as static")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::StaticInnerClass$PublicNonStaticInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE_FALSE(java_class.get_is_static_class());
+      }
+    }
+  }
+  GIVEN("Some class with a static anonymous class")
+  {
+    WHEN("Parsing the InnerClasses attribute for a static anonymous class ")
+    {
+      THEN("The class should be marked as static")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::StaticInnerClass$1");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_is_static_class());
+      }
+    }
+    WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ")
+    {
+      THEN("The class should not be marked as static")
+      {
+        const symbolt &class_symbol =
+          new_symbol_table.lookup_ref("java::StaticInnerClass$2");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE_FALSE(java_class.get_is_static_class());
+      }
+    }
+  }
+  GIVEN("Some method containing a local class")
+  {
+    WHEN(
+      "Parsing the InnerClasses attribute for a local class in a static "
+      "method ")
+    {
+      THEN("The local class should be marked as static")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::StaticInnerClass$1LocalClassInStatic");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE_FALSE(java_class.get_is_static_class());
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a local class in a non-static "
+      "method ")
+    {
+      THEN("The local class should not be marked as static")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::StaticInnerClass$1LocalClassInNonStatic");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE_FALSE(java_class.get_is_static_class());
+      }
+    }
+  }
 }