From ecd1f1d4747671729351a9644010d016bc7d2999 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 11 Mar 2026 16:49:25 +0100 Subject: [PATCH 1/2] look in top-level project.key for includes to allow for dl escapes in Java files --- .../key_project/proofmanagement/check/KeYFacade.java | 11 ++++++++++- .../io/DirectoryProofBundleHandler.java | 9 +++++++++ .../proofmanagement/io/ProofBundleHandler.java | 8 ++++++++ .../proofmanagement/io/ZipProofBundleHandler.java | 5 +++++ 4 files changed, 32 insertions(+), 1 deletion(-) diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java index 6ccf66aed57..350f5b23aa8 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java @@ -433,7 +433,16 @@ public static void ensureSourceLoaded(CheckerData data) throws ProofManagementEx Profile profile = AbstractProfile.getDefaultProfile(); - SLEnvInput slenv = new SLEnvInput(src, cp, bcp, profile, null); + /* We need to respect included .key files from project.key (for dl_ escapes). The + * easiest way to do this is to add the top-level project.key as include and let + * SLEnvInput take care about the includes from there. */ + List includePaths = List.of(); + Path projectFile = pbh.getTopLevelProjectFile(); + if (projectFile != null) { + includePaths = List.of(projectFile); + } + + SLEnvInput slenv = new SLEnvInput(src, cp, bcp, profile, includePaths); data.setSlenv(slenv); data.setSrcLoadingState(CheckerData.LoadingState.SUCCESS); data.print(LogLevel.DEBUG, "Java sources successfully loaded!"); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/DirectoryProofBundleHandler.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/DirectoryProofBundleHandler.java index 2f6f29c09e0..364b92d3dd4 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/DirectoryProofBundleHandler.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/DirectoryProofBundleHandler.java @@ -106,6 +106,15 @@ public Path getBootclasspath() throws IOException { return null; } + @Override + public Path getTopLevelProjectFile() { + Path projectFile = rootPath.resolve(Paths.get("project.key")); + if (Files.isRegularFile(projectFile)) { + return projectFile; + } + return null; + } + @Override public PathNode getFileTree() throws IOException { PathNode root = new PathNode(null, rootPath); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java index 29fbab0450c..d91831ea374 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java @@ -117,6 +117,14 @@ public abstract class ProofBundleHandler implements Closeable { */ public abstract Path getBootclasspath() throws IOException; + /** + * Returns the path to the top-level `project.key` file in the bundle, if existing, otherwise + * null. + * + * @return the path to the top-level project file or null + */ + public abstract Path getTopLevelProjectFile(); + /** * Returns a tree of the complete file hierarchy inside the bundle. * diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ZipProofBundleHandler.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ZipProofBundleHandler.java index b3f008b16ab..6a1b336d99d 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ZipProofBundleHandler.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ZipProofBundleHandler.java @@ -111,6 +111,11 @@ public Path getBootclasspath() throws IOException { return dbh.getBootclasspath(); } + @Override + public Path getTopLevelProjectFile() { + return dbh.getTopLevelProjectFile(); + } + @Override public PathNode getFileTree() throws IOException { // Path rootPath = fs.getPath("/"); From 687101e7311d8eff82386ac2b6f090081bab9f79 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 11 Mar 2026 16:50:20 +0100 Subject: [PATCH 2/2] spotless --- .../org/key_project/proofmanagement/check/KeYFacade.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java index 350f5b23aa8..86e70da2ccc 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java @@ -433,9 +433,11 @@ public static void ensureSourceLoaded(CheckerData data) throws ProofManagementEx Profile profile = AbstractProfile.getDefaultProfile(); - /* We need to respect included .key files from project.key (for dl_ escapes). The + /* + * We need to respect included .key files from project.key (for dl_ escapes). The * easiest way to do this is to add the top-level project.key as include and let - * SLEnvInput take care about the includes from there. */ + * SLEnvInput take care about the includes from there. + */ List includePaths = List.of(); Path projectFile = pbh.getTopLevelProjectFile(); if (projectFile != null) {