Unit tests deeply nested inner class parsing.

Author: jeannielynnmoulton

jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class

@@ -85,6 +85,72 @@ private PrivateDoublyNestedInnerClass(int i) {
     }
 }
 
+class InnerPrivateClassesDeeplyNested {
+    private class SinglyNestedPrivateClass {
+        int i;
+        SinglyNestedPrivateClass(int i) {
+            this.i = i;
+        }
+        public class PublicDoublyNestedInnerClass {
+            public int i;
+            public PublicDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        class DefaultDoublyNestedInnerClass {
+            int i;
+            DefaultDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        protected class ProtectedDoublyNestedInnerClass {
+            protected int i;
+            protected ProtectedDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        private class PrivateDoublyNestedInnerClass {
+            private int i;
+            private PrivateDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+    }
+}
+
+class OuterClassMostRestrictiveDeeplyNested {
+    public class SinglyNestedPublicClass {
+        int i;
+        SinglyNestedPublicClass(int i) {
+            this.i = i;
+        }
+        public class PublicDoublyNestedInnerClass {
+            public int i;
+            public PublicDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        class DefaultDoublyNestedInnerClass {
+            int i;
+            DefaultDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        protected class ProtectedDoublyNestedInnerClass {
+            protected int i;
+            protected ProtectedDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        private class PrivateDoublyNestedInnerClass {
+            private int i;
+            private PrivateDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+    }
+}
+
 class ContainsAnonymousClass {
     interface InnerInterface {
         int i = 0;

jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class

@@ -22,7 +22,7 @@ SCENARIO(
       load_java_class("InnerClasses", "./java_bytecode/java_bytecode_parser");
     WHEN("Parsing the InnerClasses attribute for a public inner class")
     {
-      THEN("The class should be marked as public")
+      THEN("The inner class should be marked as public")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass");
@@ -35,7 +35,7 @@ SCENARIO(
     }
     WHEN("Parsing the InnerClasses attribute for a package private inner class")
     {
-      THEN("The class should be marked as default")
+      THEN("The inner class should be marked as default")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass");
@@ -48,7 +48,7 @@ SCENARIO(
     }
     WHEN("Parsing the InnerClasses attribute for a protected inner class")
     {
-      THEN("The class should be marked as protected")
+      THEN("The inner class should be marked as protected")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass");
@@ -61,7 +61,7 @@ SCENARIO(
     }
     WHEN("Parsing the InnerClasses attribute for a private inner class")
     {
-      THEN("The class should be marked as private")
+      THEN("The inner class should be marked as private")
       {
         const symbolt &class_symbol =
           new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass");
@@ -73,7 +73,9 @@ SCENARIO(
       }
     }
   }
-  GIVEN("Some package-private class files in the class path with inner classes")
+  GIVEN(
+    "Some package-private (default) class files in the class path with inner "
+    "classes")
   {
     const symbol_tablet &new_symbol_table = load_java_class(
       "InnerClassesDefault", "./java_bytecode/java_bytecode_parser");
@@ -90,9 +92,11 @@ SCENARIO(
         REQUIRE(java_class.get_access() == ID_public);
       }
     }
-    WHEN("Parsing the InnerClasses attribute for a package private inner class")
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private (default) "
+      "inner class")
     {
-      THEN("The class should be marked as default")
+      THEN("The inner class should be marked as package-private (default)")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
           "java::InnerClassesDefault$DefaultInnerClass");
@@ -118,7 +122,7 @@ SCENARIO(
     }
     WHEN("Parsing the InnerClasses attribute for a private inner class")
     {
-      THEN("The class should be marked as private")
+      THEN("The inner class should be marked as private")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
           "java::InnerClassesDefault$PrivateInnerClass");
@@ -154,10 +158,10 @@ SCENARIO(
       }
     }
     WHEN(
-      "Parsing the InnerClasses attribute for a package private doubly-nested "
-      "inner class")
+      "Parsing the InnerClasses attribute for a package private (default) "
+      "doubly-nested inner class")
     {
-      THEN("The class should be marked as default")
+      THEN("The inner class should be marked as package-private (default)")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
           "java::InnerClassesDeeplyNested$SinglyNestedClass$"
@@ -170,10 +174,10 @@ SCENARIO(
       }
     }
     WHEN(
-      "Parsing the InnerClasses attribute for a protected doubly-nested inner "
-      "class")
+      "Parsing the InnerClasses attribute for a package private (default) "
+      "doubly-nested inner class ")
     {
-      THEN("The class should be marked as protected")
+      THEN("The inner class should be marked as protected")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
           "java::InnerClassesDeeplyNested$SinglyNestedClass$"
@@ -189,7 +193,7 @@ SCENARIO(
       "Parsing the InnerClasses attribute for a private doubly-nested inner "
       "class")
     {
-      THEN("The class should be marked as private")
+      THEN("The inner class should be marked as private ")
       {
         const symbolt &class_symbol = new_symbol_table.lookup_ref(
           "java::InnerClassesDeeplyNested$SinglyNestedClass$"
@@ -203,6 +207,162 @@ SCENARIO(
     }
   }
 
+  GIVEN(
+    "Some package-private class files in the class path with private deeply"
+    "nested inner classes")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "InnerPrivateClassesDeeplyNested",
+      "./java_bytecode/java_bytecode_parser");
+    WHEN(
+      "Parsing the InnerClasses attribute for a public doubly-nested inner "
+      "class")
+    {
+      THEN(
+        "The inner class should be marked as private because its containing "
+        "class has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
+          "PublicDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private doubly-nested "
+      "inner class")
+    {
+      THEN(
+        "The inner class should be marked as private because its containing "
+        "class has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
+          "DefaultDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a protected doubly-nested inner "
+      "class")
+    {
+      THEN(
+        "The inner class should be marked as private because its containing "
+        "class has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
+          "ProtectedDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a private doubly-nested inner "
+      "class")
+    {
+      THEN("The inner class should be marked as private ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$"
+          "PrivateDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+  }
+
+  GIVEN(
+    "Some class files where the outer class is more restrictive than the first "
+    "inner class")
+  {
+    const symbol_tablet &new_symbol_table = load_java_class(
+      "OuterClassMostRestrictiveDeeplyNested",
+      "./java_bytecode/java_bytecode_parser");
+    WHEN(
+      "Parsing the InnerClasses attribute for a public doubly-nested inner "
+      "class")
+    {
+      THEN(
+        "The inner class should be marked as default (package-private) because "
+        "one of its containing classes has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
+          "PublicDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_default);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a package private doubly-nested "
+      "inner class")
+    {
+      THEN(
+        "The inner class should be marked as default (package-private) because "
+        "one of its containing classes has stricter access ")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
+          "DefaultDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_default);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a protected doubly-nested inner "
+      "class")
+    {
+      THEN("The inner class should be marked as default (package-private)")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
+          "ProtectedDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_default);
+      }
+    }
+    WHEN(
+      "Parsing the InnerClasses attribute for a private doubly-nested inner "
+      "class")
+    {
+      THEN("The inner class should be marked as private")
+      {
+        const symbolt &class_symbol = new_symbol_table.lookup_ref(
+          "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$"
+          "PrivateDoublyNestedInnerClass");
+        const java_class_typet java_class =
+          to_java_class_type(class_symbol.type);
+        REQUIRE_FALSE(java_class.get_is_anonymous_class());
+        REQUIRE(java_class.get_is_inner_class());
+        REQUIRE(java_class.get_access() == ID_private);
+      }
+    }
+  }
+
   GIVEN(
     "Some package-private class files in the class path with anonymous classes")
   {