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..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,7 +433,18 @@ 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("/");