Skip to content

Commit 4e5cd04

Browse files
wadoonwadoon
committed
migration to java.nio.Path
1 parent a094d2a commit 4e5cd04

File tree

154 files changed

+1479
-1341
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

154 files changed

+1479
-1341
lines changed

‎key.core.example/src/main/java/org/key_project/Main.java‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package org.key_project;
55

6-
import java.io.File;
6+
7+
import java.nio.file.Path;
8+
import java.nio.file.Paths;
79
import java.util.*;
810

911
import de.uka.ilkd.key.control.KeYEnvironment;
@@ -39,7 +41,7 @@ public class Main {
3941
*/
4042
public static void main(String[] args) {
4143
LOGGER.info("Starting KeY example application.");
42-
File location = args.length == 1 ? new File(args[0]) : new File("example");
44+
Path location = Paths.get(args.length == 1 ? args[0] : "example");
4345
// Path to the source code folder/file or to a *.proof file
4446
try {
4547
// Ensure that Taclets are parsed
@@ -53,15 +55,15 @@ public static void main(String[] args) {
5355
/**
5456
* sets up the environment with the Java project described by its location
5557
*
56-
* @param location the File with the path to the source directory of the Java project
58+
* @param location the Path with the path to the source directory of the Java project
5759
* to be verified
5860
* @return the {@KeYEnvironment} that provides the context for all following verification tasks
5961
* @throws ProblemLoaderException if the setup fails
6062
*/
61-
private static KeYEnvironment<?> setupEnvironment(File location) throws ProblemLoaderException {
62-
List<File> classPaths = null; // Optionally: Additional specifications for API classes
63-
File bootClassPath = null; // Optionally: Different default specifications for Java API
64-
List<File> includes = null; // Optionally: Additional includes to consider
63+
private static KeYEnvironment<?> setupEnvironment(Path location) throws ProblemLoaderException {
64+
List<Path> classPaths = null; // Optionally: Additional specifications for API classes
65+
Path bootClassPath = null; // Optionally: Different default specifications for Java API
66+
List<Path> includes = null; // Optionally: Additional includes to consider
6567

6668
if (!ProofSettings.isChoiceSettingInitialised()) {
6769
KeYEnvironment<?> env =

‎key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java‎

Lines changed: 17 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.proof_references.testcase;
55

6-
import java.io.File;
6+
import java.nio.file.Files;
7+
import java.nio.file.Path;
78
import java.util.Iterator;
89
import java.util.LinkedHashSet;
910
import java.util.Map;
@@ -35,6 +36,8 @@
3536
import org.key_project.util.helper.FindResources;
3637
import org.key_project.util.java.CollectionUtil;
3738

39+
import org.jspecify.annotations.Nullable;
40+
3841
import static org.junit.jupiter.api.Assertions.*;
3942

4043
/**
@@ -43,7 +46,7 @@
4346
* @author Martin Hentschel
4447
*/
4548
public abstract class AbstractProofReferenceTestCase {
46-
public static final File TESTCASE_DIRECTORY = FindResources.getTestCasesDirectory();
49+
public static final @Nullable Path TESTCASE_DIRECTORY = FindResources.getTestCasesDirectory();
4750

4851
static {
4952
assertNotNull(TESTCASE_DIRECTORY, "Could not find test case directory");
@@ -61,7 +64,7 @@ public abstract class AbstractProofReferenceTestCase {
6164
* @param expectedReferences The expected proof references.
6265
* @throws Exception Occurred Exception.
6366
*/
64-
protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
67+
protected void doReferenceFunctionTest(@Nullable Path baseDir, String javaPathInBaseDir,
6568
String containerTypeName, String targetName, boolean useContracts,
6669
IProofReferencesAnalyst analyst, ExpectedProofReferences... expectedReferences)
6770
throws Exception {
@@ -83,7 +86,7 @@ protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
8386
* @param expectedReferences The expected proof references.
8487
* @throws Exception Occurred Exception.
8588
*/
86-
protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
89+
protected void doReferenceFunctionTest(@Nullable Path baseDir, String javaPathInBaseDir,
8790
String containerTypeName, String targetName, boolean useContracts,
8891
IProofReferencesAnalyst analyst, Predicate<IProofReference<?>> currentReferenceFilter,
8992
ExpectedProofReferences... expectedReferences) throws Exception {
@@ -105,7 +108,7 @@ protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
105108
* @param expectedReferences The expected proof references.
106109
* @throws Exception Occurred Exception.
107110
*/
108-
protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
111+
protected void doReferenceMethodTest(@Nullable Path baseDir, String javaPathInBaseDir,
109112
String containerTypeName, String methodFullName, boolean useContracts,
110113
IProofReferencesAnalyst analyst, ExpectedProofReferences... expectedReferences)
111114
throws Exception {
@@ -126,7 +129,7 @@ protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
126129
* @param expectedReferences The expected proof references.
127130
* @throws Exception Occurred Exception.
128131
*/
129-
protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
132+
protected void doReferenceMethodTest(@Nullable Path baseDir, String javaPathInBaseDir,
130133
String containerTypeName, String methodFullName, boolean useContracts,
131134
IProofReferencesAnalyst analyst, Predicate<IProofReference<?>> currentReferenceFilter,
132135
ExpectedProofReferences... expectedReferences) throws Exception {
@@ -138,8 +141,8 @@ protected void doReferenceMethodTest(File baseDir, String javaPathInBaseDir,
138141

139142
/**
140143
* Creates the {@link IProofTester} used by
141-
* {@link #doProofFunctionTest(File, String, String, String, boolean, IProofTester)} and
142-
* {@link #doProofMethodTest(File, String, String, String, boolean, IProofTester)}.
144+
* {@link #doProofFunctionTest(Path, String, String, String, boolean, IProofTester)} and
145+
* {@link #doProofMethodTest(Path, String, String, String, boolean, IProofTester)}.
143146
*
144147
* @param analyst The {@link IProofReferencesAnalyst} to use.
145148
* @param currentReferenceFilter An optional {@link Predicate} to limit the references to test.
@@ -296,7 +299,7 @@ public String target() {
296299
* @param tester The {@link IProofTester} which executes the test steps.
297300
* @throws Exception Occurred Exception.
298301
*/
299-
protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir,
302+
protected void doProofFunctionTest(@Nullable Path baseDir, String javaPathInBaseDir,
300303
String containerTypeName, final String targetName, boolean useContracts,
301304
IProofTester tester) throws Exception {
302305
assertNotNull(tester);
@@ -309,8 +312,8 @@ protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir,
309312
// representations
310313
ProofIndependentSettings.setUsePrettyPrinting(false);
311314
// Make sure that required files exists
312-
File javaFile = new File(baseDir, javaPathInBaseDir);
313-
assertTrue(javaFile.exists());
315+
Path javaFile = baseDir.resolve(javaPathInBaseDir);
316+
assertTrue(Files.exists(javaFile));
314317
// Make sure that the correct taclet options are defined.
315318
originalTacletOptions = HelperClassForTests.setDefaultTacletOptionsForTarget(javaFile,
316319
containerTypeName, targetName);
@@ -369,7 +372,7 @@ protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir,
369372
* @param tester The {@link IProofTester} which executes the test steps.
370373
* @throws Exception Occurred Exception.
371374
*/
372-
protected void doProofMethodTest(File baseDir, String javaPathInBaseDir,
375+
protected void doProofMethodTest(@Nullable Path baseDir, String javaPathInBaseDir,
373376
String containerTypeName, String methodFullName, boolean useContracts,
374377
IProofTester tester) throws Exception {
375378
assertNotNull(tester);
@@ -382,8 +385,8 @@ protected void doProofMethodTest(File baseDir, String javaPathInBaseDir,
382385
// representations
383386
ProofIndependentSettings.setUsePrettyPrinting(false);
384387
// Make sure that required files exists
385-
File javaFile = new File(baseDir, javaPathInBaseDir);
386-
assertTrue(javaFile.exists());
388+
Path javaFile = baseDir.resolve(javaPathInBaseDir);
389+
assertTrue(Files.exists(javaFile));
387390
// Make sure that the correct taclet options are defined.
388391
originalTacletOptions =
389392
HelperClassForTests.setDefaultTacletOptions(baseDir, javaPathInBaseDir);

‎key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestKeYTypeUtil.java‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.proof_references.testcase;
55

6-
import java.io.File;
76

87
import de.uka.ilkd.key.control.KeYEnvironment;
98
import de.uka.ilkd.key.java.Services;
@@ -26,8 +25,8 @@ public class TestKeYTypeUtil extends AbstractProofReferenceTestCase {
2625
@Test
2726
public void testIsInnerType() throws Exception {
2827
KeYEnvironment<?> environment = KeYEnvironment.load(
29-
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
30-
null);
28+
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
29+
null, null, null);
3130
try {
3231
Services services = environment.getServices();
3332
assertNotNull(services);
@@ -67,8 +66,8 @@ public void testIsInnerType() throws Exception {
6766
@Test
6867
public void testGetParentName() throws Exception {
6968
KeYEnvironment<?> environment = KeYEnvironment.load(
70-
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
71-
null);
69+
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
70+
null, null, null);
7271
try {
7372
Services services = environment.getServices();
7473
assertNotNull(services);
@@ -110,8 +109,8 @@ public void testGetParentName() throws Exception {
110109
@Test
111110
public void testIsType() throws Exception {
112111
KeYEnvironment<?> environment = KeYEnvironment.load(
113-
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
114-
null);
112+
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
113+
null, null, null);
115114
try {
116115
Services services = environment.getServices();
117116
assertNotNull(services);
@@ -145,8 +144,8 @@ public void testIsType() throws Exception {
145144
@Test
146145
public void testGetType() throws Exception {
147146
KeYEnvironment<?> environment = KeYEnvironment.load(
148-
new File(TESTCASE_DIRECTORY, "/proofReferences/InnerAndAnonymousTypeTest"), null, null,
149-
null);
147+
TESTCASE_DIRECTORY.resolve("proofReferences/InnerAndAnonymousTypeTest"),
148+
null, null, null);
150149
try {
151150
Services services = environment.getServices();
152151
assertNotNull(services);

‎key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestProofReferenceUtil.java‎

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.proof_references.testcase;
55

6-
import java.io.File;
6+
import java.nio.file.Path;
77
import java.util.LinkedHashSet;
88

99
import de.uka.ilkd.key.proof.Node;
@@ -17,6 +17,7 @@
1717
import org.key_project.util.collection.ImmutableList;
1818
import org.key_project.util.collection.ImmutableSLList;
1919

20+
import org.jspecify.annotations.Nullable;
2021
import org.junit.jupiter.api.Test;
2122

2223
/**
@@ -26,8 +27,7 @@
2627
*/
2728
public class TestProofReferenceUtil extends AbstractProofReferenceTestCase {
2829
/**
29-
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
30-
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
30+
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
3131
*/
3232
@Test
3333
public void testReferenceComputation_ExpandAndContract() throws Exception {
@@ -43,8 +43,7 @@ public void testReferenceComputation_ExpandAndContract() throws Exception {
4343
}
4444

4545
/**
46-
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
47-
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
46+
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
4847
*/
4948
@Test
5049
public void testReferenceComputation_NoAnalysts() throws Exception {
@@ -53,8 +52,7 @@ public void testReferenceComputation_NoAnalysts() throws Exception {
5352
}
5453

5554
/**
56-
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
57-
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
55+
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
5856
*/
5957
@Test
6058
public void testReferenceComputation_ContractOnly() throws Exception {
@@ -64,8 +62,7 @@ public void testReferenceComputation_ContractOnly() throws Exception {
6462
}
6563

6664
/**
67-
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)} and
68-
* {@link ProofReferenceUtil#computeProofReferences(Node, ImmutableList)}.
65+
* Tests {@link ProofReferenceUtil#computeProofReferences(Proof, ImmutableList)}
6966
*/
7067
@Test
7168
public void testReferenceComputation_ExpandOnly() throws Exception {
@@ -106,7 +103,8 @@ public void testReferenceComputation_DefaultAnalysts() throws Exception {
106103
* @param expectedReferences The expected proof references.
107104
* @throws Exception Occurred Exception.
108105
*/
109-
protected void doAPITest(File baseDir, String javaPathInBaseDir, String containerTypeName,
106+
protected void doAPITest(@Nullable Path baseDir, String javaPathInBaseDir,
107+
String containerTypeName,
110108
String methodFullName, boolean useContracts,
111109
final ImmutableList<IProofReferencesAnalyst> analysts,
112110
final ExpectedProofReferences... expectedReferences) throws Exception {

0 commit comments

Comments
 (0)