From 089d26b7e589457f64ee7482d0ba8340b35bf0a7 Mon Sep 17 00:00:00 2001
From: Hritik Raj <hritik23154049@akgec.ac.in>
Date: Thu, 19 Feb 2026 02:24:40 +0530
Subject: [PATCH] Fix: Add Java 11 Nestmate support and edge-case tests

---
 .../modules/java.base/java/lang/Class.java    | 14 +++++
 .../nasa/jpf/test/java/lang/NestmateTest.java | 61 +++++++++++++++++++
 2 files changed, 75 insertions(+)
 create mode 100644 src/tests/gov/nasa/jpf/test/java/lang/NestmateTest.java

diff --git a/src/classes/modules/java.base/java/lang/Class.java b/src/classes/modules/java.base/java/lang/Class.java
index 524f3b0e1..4f8959ea0 100644
--- a/src/classes/modules/java.base/java/lang/Class.java
+++ b/src/classes/modules/java.base/java/lang/Class.java
@@ -408,4 +408,18 @@ public boolean isSynthetic (){
   public Module getModule() {
     return module;
   }
+  public Class<?> getNestHost() {
+    Class<?> host = this;
+    while (host.getEnclosingClass() != null) {
+      host = host.getEnclosingClass();
+    }
+    return host;
+  }
+
+  public boolean isNestmateOf(Class<?> c) {
+    if (c == null) {
+      return false;
+    }
+    return this.getNestHost() == c.getNestHost();
+  }
 }
diff --git a/src/tests/gov/nasa/jpf/test/java/lang/NestmateTest.java b/src/tests/gov/nasa/jpf/test/java/lang/NestmateTest.java
new file mode 100644
index 000000000..9112f242e
--- /dev/null
+++ b/src/tests/gov/nasa/jpf/test/java/lang/NestmateTest.java
@@ -0,0 +1,61 @@
+/*
+ * Copyright (C) 2018, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package gov.nasa.jpf.test.java.lang;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+import static org.junit.Assert.*; // <-- This was the missing magic line!
+
+public class NestmateTest extends TestJPF {
+
+    public class Inner {}
+
+    @Test
+    public void testNestHost() {
+        if (verifyNoPropertyViolation()) {
+            Class<?> host = NestmateTest.class.getNestHost();
+            assertEquals(NestmateTest.class, host);
+            Class<?> innerHost = Inner.class.getNestHost();
+            assertEquals(NestmateTest.class, innerHost);
+        }
+    }
+
+    @Test
+    public void testIsNestmateOf() {
+        if (verifyNoPropertyViolation()) {
+            assertTrue(NestmateTest.class.isNestmateOf(Inner.class));
+            assertTrue(Inner.class.isNestmateOf(NestmateTest.class));
+        }
+    }
+
+    @Test
+    public void testPrimitiveArrayVoidNestHost() {
+        if (verifyNoPropertyViolation()) {
+            // Primitive
+            assertEquals(int.class, int.class.getNestHost());
+            assertEquals(double.class, double.class.getNestHost());
+
+            // Array
+            assertEquals(int[].class, int[].class.getNestHost());
+            assertEquals(String[].class, String[].class.getNestHost());
+
+            // Void
+            assertEquals(void.class, void.class.getNestHost());
+        }
+    }
+}
\ No newline at end of file