Adds another test for inner class accessibility

This tests when the outer most class is the most restrictive for an inner class depth of 3.

Author: jeannielynnmoulton

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

@@ -118,6 +118,39 @@ private PrivateDoublyNestedInnerClass(int 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

@@ -295,6 +295,83 @@ SCENARIO(
     }
   }
 
+  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")
   {