Captures information for static inner classes.

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -269,6 +269,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

@@ -213,6 +213,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

@@ -1625,6 +1625,7 @@ void java_bytecode_parsert::rinner_classes_attribute(
     bool is_private = inner_class_access_flags & ACC_PRIVATE;
     bool is_public = inner_class_access_flags & ACC_PUBLIC;
     bool is_protected = inner_class_access_flags & ACC_PROTECTED;
+    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'
@@ -1643,12 +1644,14 @@ void java_bytecode_parsert::rinner_classes_attribute(
       parsed_class.is_private = true;
       parsed_class.is_protected = false;
       parsed_class.is_public = false;
+      parsed_class.is_static_class = is_static;
     }
     else
     {
       parsed_class.is_private = is_private;
       parsed_class.is_protected = is_protected;
       parsed_class.is_public = is_public;
+      parsed_class.is_static_class = is_static;
     }
   }
 }

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/parse_java_attributes.cpp

@@ -266,4 +266,64 @@ SCENARIO(
       }
     }
   }
+
+  GIVEN("Some class with a static inner class")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "StaticInnerClass", "./java_bytecode/java_bytecode_parser");
+    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")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "StaticInnerClass", "./java_bytecode/java_bytecode_parser");
+    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_FALSE(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_FALSE(java_class.get_is_inner_class());
+        REQUIRE_FALSE(java_class.get_is_static_class());
+      }
+    }
+  }
 }