Skip to content

Migration to java.nio.Path #3618

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wadoon merged 3 commits into from
Jun 6, 2025
Merged

Migration to java.nio.Path #3618

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4e5cd04
migration to java.nio.Path
wadoon Jun 2, 2025
84f7f8b
update makeFilenameRelative functionality
wadoon Jun 6, 2025
86c0458
Apply suggestions from code review
wadoon Jun 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 9 additions & 7 deletions key.core.example/src/main/java/org/key_project/Main.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@
* SPDX-License-Identifier: GPL-2.0-only */
package org.key_project;

import java.io.File;

import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.*;

import de.uka.ilkd.key.control.KeYEnvironment;
Expand Down Expand Up @@ -39,7 +41,7 @@ public class Main {
*/
public static void main(String[] args) {
LOGGER.info("Starting KeY example application.");
File location = args.length == 1 ? new File(args[0]) : new File("example");
Path location = Paths.get(args.length == 1 ? args[0] : "example");
// Path to the source code folder/file or to a *.proof file
try {
// Ensure that Taclets are parsed
Expand All @@ -53,15 +55,15 @@ public static void main(String[] args) {
/**
* sets up the environment with the Java project described by its location
*
* @param location the File with the path to the source directory of the Java project
* @param location the Path with the path to the source directory of the Java project
* to be verified
* @return the {@KeYEnvironment} that provides the context for all following verification tasks
* @throws ProblemLoaderException if the setup fails
*/
private static KeYEnvironment<?> setupEnvironment(File location) throws ProblemLoaderException {
List<File> classPaths = null; // Optionally: Additional specifications for API classes
File bootClassPath = null; // Optionally: Different default specifications for Java API
List<File> includes = null; // Optionally: Additional includes to consider
private static KeYEnvironment<?> setupEnvironment(Path location) throws ProblemLoaderException {
List<Path> classPaths = null; // Optionally: Additional specifications for API classes
Path bootClassPath = null; // Optionally: Different default specifications for Java API
List<Path> includes = null; // Optionally: Additional includes to consider

if (!ProofSettings.isChoiceSettingInitialised()) {
KeYEnvironment<?> env =
Expand Down
31 changes: 17 additions & 14 deletions ...c/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof_references.testcase;

import java.io.File;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.Map;
Expand Down Expand Up @@ -35,6 +36,8 @@
import org.key_project.util.helper.FindResources;
import org.key_project.util.java.CollectionUtil;

import org.jspecify.annotations.Nullable;

import static org.junit.jupiter.api.Assertions.*;

/**
Expand All @@ -43,7 +46,7 @@
* @author Martin Hentschel
*/
public abstract class AbstractProofReferenceTestCase {
public static final File TESTCASE_DIRECTORY = FindResources.getTestCasesDirectory();
public static final @Nullable Path TESTCASE_DIRECTORY = FindResources.getTestCasesDirectory();

static {
assertNotNull(TESTCASE_DIRECTORY, "Could not find test case directory");
Expand All @@ -61,7 +64,7 @@ public abstract class AbstractProofReferenceTestCase {
* @param expectedReferences The expected proof references.
* @throws Exception Occurred Exception.
*/
protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
protected void doReferenceFunctionTest(@Nullable Path baseDir, String javaPathInBaseDir,
String containerTypeName, String targetName, boolean useContracts,
IProofReferencesAnalyst analyst, ExpectedProofReferences... expectedReferences)
throws Exception {
Expand All @@ -83,7 +86,7 @@ protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
* @param expectedReferences The expected proof references.
* @throws Exception Occurred Exception.
*/
protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
protected void doReferenceFunctionTest(@Nullable Path baseDir, String javaPathInBaseDir,
String containerTypeName, String targetName, boolean useContracts,
IProofReferencesAnalyst analyst, Predicate<IProofReference<?>> currentReferenceFilter,
ExpectedProofReferences... expectedReferences) throws Exception {
Expand All @@ -105,7 +108,7 @@ protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
* @param expectedReferences The expected proof references.
* @throws Exception Occurred Exception.
*/
protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
protected void doReferenceMethodTest(@Nullable Path baseDir, String javaPathInBaseDir,
String containerTypeName, String methodFullName, boolean useContracts,
IProofReferencesAnalyst analyst, ExpectedProofReferences... expectedReferences)
throws Exception {
Expand All @@ -126,7 +129,7 @@ protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
* @param expectedReferences The expected proof references.
* @throws Exception Occurred Exception.
*/
protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
protected void doReferenceMethodTest(@Nullable Path baseDir, String javaPathInBaseDir,
String containerTypeName, String methodFullName, boolean useContracts,
IProofReferencesAnalyst analyst, Predicate<IProofReference<?>> currentReferenceFilter,
ExpectedProofReferences... expectedReferences) throws Exception {
Expand All @@ -138,8 +141,8 @@ protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,

/**
* Creates the {@link IProofTester} used by
* {@link #doProofFunctionTest(File, String, String, String, boolean, IProofTester)} and
* {@link #doProofMethodTest(File, String, String, String, boolean, IProofTester)}.
* {@link #doProofFunctionTest(Path, String, String, String, boolean, IProofTester)} and
* {@link #doProofMethodTest(Path, String, String, String, boolean, IProofTester)}.
*
* @param analyst The {@link IProofReferencesAnalyst} to use.
* @param currentReferenceFilter An optional {@link Predicate} to limit the references to test.
Expand Down Expand Up @@ -296,7 +299,7 @@ public String target() {
* @param tester The {@link IProofTester} which executes the test steps.
* @throws Exception Occurred Exception.
*/
protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir,
protected void doProofFunctionTest(@Nullable Path baseDir, String javaPathInBaseDir,
String containerTypeName, final String targetName, boolean useContracts,
IProofTester tester) throws Exception {
assertNotNull(tester);
Expand All @@ -309,8 +312,8 @@ protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir,
// representations
ProofIndependentSettings.setUsePrettyPrinting(false);
// Make sure that required files exists
File javaFile = new File(baseDir, javaPathInBaseDir);
assertTrue(javaFile.exists());
Path javaFile = baseDir.resolve(javaPathInBaseDir);
assertTrue(Files.exists(javaFile));
// Make sure that the correct taclet options are defined.
originalTacletOptions = HelperClassForTests.setDefaultTacletOptionsForTarget(javaFile,
containerTypeName, targetName);
Expand Down Expand Up @@ -369,7 +372,7 @@ protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir,
* @param tester The {@link IProofTester} which executes the test steps.
* @throws Exception Occurred Exception.
*/
protected void doProofMethodTest(File baseDir, String javaPathInBaseDir,
protected void doProofMethodTest(@Nullable Path baseDir, String javaPathInBaseDir,
String containerTypeName, String methodFullName, boolean useContracts,
IProofTester tester) throws Exception {
assertNotNull(tester);
Expand All @@ -382,8 +385,8 @@ protected void doProofMethodTest(File baseDir, String javaPathInBaseDir,
// representations
ProofIndependentSettings.setUsePrettyPrinting(false);
// Make sure that required files exists
File javaFile = new File(baseDir, javaPathInBaseDir);
assertTrue(javaFile.exists());
Path javaFile = baseDir.resolve(javaPathInBaseDir);
assertTrue(Files.exists(javaFile));
// Make sure that the correct taclet options are defined.
originalTacletOptions =
HelperClassForTests.setDefaultTacletOptions(baseDir, javaPathInBaseDir);
Expand Down
17 changes: 8 additions & 9 deletions ...f_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestKeYTypeUtil.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof_references.testcase;

import java.io.File;

import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.Services;
Expand All @@ -26,8 +25,8 @@ public class TestKeYTypeUtil extends AbstractProofReferenceTestCase {
@Test
public void testIsInnerType() throws Exception {
KeYEnvironment<?> environment = KeYEnvironment.load(
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
null);
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
null, null, null);
try {
Services services = environment.getServices();
assertNotNull(services);
Expand Down Expand Up @@ -67,8 +66,8 @@ public void testIsInnerType() throws Exception {
@Test
public void testGetParentName() throws Exception {
KeYEnvironment<?> environment = KeYEnvironment.load(
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
null);
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
null, null, null);
try {
Services services = environment.getServices();
assertNotNull(services);
Expand Down Expand Up @@ -110,8 +109,8 @@ public void testGetParentName() throws Exception {
@Test
public void testIsType() throws Exception {
KeYEnvironment<?> environment = KeYEnvironment.load(
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
null);
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
null, null, null);
try {
Services services = environment.getServices();
assertNotNull(services);
Expand Down Expand Up @@ -145,8 +144,8 @@ public void testIsType() throws Exception {
@Test
public void testGetType() throws Exception {
KeYEnvironment<?> environment = KeYEnvironment.load(
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
null);
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
null, null, null);
try {
Services services = environment.getServices();
assertNotNull(services);
Expand Down
18 changes: 8 additions & 10 deletions ...ences/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestProofReferenceUtil.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof_references.testcase;

import java.io.File;
import java.nio.file.Path;
import java.util.LinkedHashSet;

import de.uka.ilkd.key.proof.Node;
Expand All @@ -17,6 +17,7 @@
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import org.jspecify.annotations.Nullable;
import org.junit.jupiter.api.Test;

/**
Expand All @@ -26,8 +27,7 @@
*/
public class TestProofReferenceUtil extends AbstractProofReferenceTestCase {
/**
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
*/
@Test
public void testReferenceComputation_ExpandAndContract() throws Exception {
Expand All @@ -43,8 +43,7 @@ public void testReferenceComputation_ExpandAndContract() throws Exception {
}

/**
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
*/
@Test
public void testReferenceComputation_NoAnalysts() throws Exception {
Expand All @@ -53,8 +52,7 @@ public void testReferenceComputation_NoAnalysts() throws Exception {
}

/**
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
*/
@Test
public void testReferenceComputation_ContractOnly() throws Exception {
Expand All @@ -64,8 +62,7 @@ public void testReferenceComputation_ContractOnly() throws Exception {
}

/**
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
*/
@Test
public void testReferenceComputation_ExpandOnly() throws Exception {
Expand Down Expand Up @@ -106,7 +103,8 @@ public void testReferenceComputation_DefaultAnalysts() throws Exception {
* @param expectedReferences The expected proof references.
* @throws Exception Occurred Exception.
*/
protected void doAPITest(File baseDir, String javaPathInBaseDir, String containerTypeName,
protected void doAPITest(@Nullable Path baseDir, String javaPathInBaseDir,
String containerTypeName,
String methodFullName, boolean useContracts,
final ImmutableList<IProofReferencesAnalyst> analysts,
final ExpectedProofReferences... expectedReferences) throws Exception {
Expand Down
Loading
Loading