From 2368d5d6f3bdef24d2a57ad5c2e001cab2891745 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 2 Nov 2026 09:54:42 +0000 Subject: [PATCH] Make the models compile with JDK 25 Building the models with JDK 25 (the default JDK on Ubuntu 26.04, and thus on GitHub's ubuntu-latest runners) fails with three errors: - Object.java: "flexible constructors is not supported in -source 8". java.lang.Object has no superclass, so javac 25 treats every statement in its constructor as part of a constructor prologue (JEP 513). Initialise cproverMonitorCount in its declaration instead. - Class.java: ClassLoader.checkClassLoaderPermission no longer exists. As the call was already passing null for the caller class, it did not check anything; comment it out like the original call. - URLEncoder.java: package sun.security.action does not exist. Read the file.encoding property with System.getProperty: doPrivileged has no effect without a security manager. With these changes the models build with JDK 11, 17 and 25. With JDK 17, the bytecode of Class differs only in the removed call and constant-pool indices, and that of Object only in the constructor no longer storing 0 to cproverMonitorCount, which is the default value of the field. Co-authored-by: Kiro --- src/main/java/java/lang/Class.java | 4 +++- src/main/java/java/lang/Object.java | 3 +-- src/main/java/java/net/URLEncoder.java | 12 +++++------- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/main/java/java/lang/Class.java b/src/main/java/java/lang/Class.java index 36d0482..ac5c501 100644 --- a/src/main/java/java/lang/Class.java +++ b/src/main/java/java/lang/Class.java @@ -271,7 +271,9 @@ public ClassLoader getClassLoader() { // DIFFBLUE MODEL LIBRARY // removed for compatibility with Java 9 and newer // ClassLoader.checkClassLoaderPermission(cl, Reflection.getCallerClass()); - ClassLoader.checkClassLoaderPermission(cl, null); + // removed for compatibility with Java 25, where this method no + // longer exists + // ClassLoader.checkClassLoaderPermission(cl, null); } return cl; } diff --git a/src/main/java/java/lang/Object.java b/src/main/java/java/lang/Object.java index dfe9363..1c783e0 100644 --- a/src/main/java/java/lang/Object.java +++ b/src/main/java/java/lang/Object.java @@ -34,10 +34,9 @@ public class Object { // lock needed for synchronization in JBMC // used by monitorenter, monitorexit, wait, and notify // Not present in the original Object class - public int cproverMonitorCount; + public int cproverMonitorCount = 0; public Object() { - cproverMonitorCount = 0; } /** diff --git a/src/main/java/java/net/URLEncoder.java b/src/main/java/java/net/URLEncoder.java index 86377b7..87f41e4 100644 --- a/src/main/java/java/net/URLEncoder.java +++ b/src/main/java/java/net/URLEncoder.java @@ -35,10 +35,6 @@ import java.nio.charset.IllegalCharsetNameException; import java.nio.charset.UnsupportedCharsetException ; import java.util.BitSet; -import java.security.AccessController; -import java.security.PrivilegedAction; -import sun.security.action.GetBooleanAction; -import sun.security.action.GetPropertyAction; /** * Utility class for HTML form encoding. This class contains static methods @@ -140,9 +136,11 @@ public class URLEncoder { dontNeedEncoding.set('.'); dontNeedEncoding.set('*'); - dfltEncName = AccessController.doPrivileged( - new GetPropertyAction("file.encoding") - ); + // DIFFBLUE MODEL LIBRARY + // sun.security.action.GetPropertyAction is not available in Java 25, + // and AccessController.doPrivileged has no effect without a + // security manager + dfltEncName = System.getProperty("file.encoding"); } /**