Skip to content

Commit d331fd1

Browse files
wadoonwadoon
committed
fix rebase
1 parent 503b69d commit d331fd1

File tree

6 files changed

+34
-43
lines changed

6 files changed

+34
-43
lines changed

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
package de.uka.ilkd.key.testgen;
55

66
import java.io.File;
7+
import java.nio.file.Path;
78
import java.util.ArrayList;
89
import java.util.LinkedList;
910
import java.util.List;
@@ -35,7 +36,7 @@ public static void main(String[] args) {
3536
}
3637

3738
@CommandLine.Parameters(description = "KeY or Java file.", arity = "1..*")
38-
private List<File> files = new LinkedList<>();
39+
private List<Path> files = new LinkedList<>();
3940

4041
@CommandLine.Option(names = "-T", description = "Number of parallel jobs", defaultValue = "4")
4142
private int numberOfThreads = 4;
@@ -107,7 +108,7 @@ public Integer call() throws Exception {
107108
}
108109

109110

110-
for (File file : files) {
111+
for (Path file : files) {
111112
List<Proof> proofs = new LinkedList<>();
112113
var env = KeYEnvironment.load(file);
113114
Proof proof = env.getLoadedProof();
@@ -130,7 +131,7 @@ public Integer call() throws Exception {
130131

131132
LOGGER.info("Number of proof found: {}", proofs.size());
132133

133-
try (var exec = Executors.newFixedThreadPool(numberOfThreads);) {
134+
try (var exec = Executors.newFixedThreadPool(numberOfThreads)) {
134135
LOGGER.info("Start processing with {} threads", numberOfThreads);
135136
var tasks = proofs.stream().map(
136137
p -> TestgenFacade.generateTestcasesTask(env, p, settings, log)).toList();

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java‎

Lines changed: 9 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -3,19 +3,13 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.testgen;
55

6-
import java.io.*;
7-
import java.nio.charset.StandardCharsets;
8-
import java.nio.file.*;
9-
import java.nio.file.attribute.BasicFileAttributes;
10-
import java.util.*;
11-
import java.util.concurrent.atomic.AtomicInteger;
12-
136
import java.io.IOException;
147
import java.nio.file.*;
158
import java.nio.file.attribute.BasicFileAttributes;
169
import java.util.*;
1710
import java.util.concurrent.atomic.AtomicInteger;
1811
import javax.lang.model.element.Modifier;
12+
1913
import de.uka.ilkd.key.java.JavaInfo;
2014
import de.uka.ilkd.key.java.Services;
2115
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
@@ -24,7 +18,10 @@
2418
import de.uka.ilkd.key.java.reference.TypeReference;
2519
import de.uka.ilkd.key.ldt.HeapLDT;
2620
import de.uka.ilkd.key.logic.JTerm;
27-
import de.uka.ilkd.key.logic.op.*;
21+
import de.uka.ilkd.key.logic.op.IProgramMethod;
22+
import de.uka.ilkd.key.logic.op.JFunction;
23+
import de.uka.ilkd.key.logic.op.ObserverFunction;
24+
import de.uka.ilkd.key.logic.op.ProgramVariable;
2825
import de.uka.ilkd.key.proof.Node;
2926
import de.uka.ilkd.key.proof.Proof;
3027
import de.uka.ilkd.key.settings.ProofIndependentSettings;
@@ -88,16 +85,10 @@ public class TestCaseGenerator {
8885
private final boolean rflAsInternalClass;
8986
private final AssignmentCreator assignmentCreator;
9087
private final ReflectionClassCreator rflCreator;
91-
private final String modDirName;
88+
private final Path modDirName;
9289
private final OutputEnvironment outputFolder;
9390
private final Path outputModDir;
9491
private final Path outputDontCopy;
95-
private final boolean rflAsInternalClass;
96-
protected final boolean useRFL;
97-
protected final ReflectionClassCreator rflCreator;
98-
private final Path dontCopy;
99-
protected final Path modDir;
100-
protected final String directory;
10192
private final TGReporter reporter;
10293
private final String fileName;
10394
private final String packageName;
@@ -123,7 +114,8 @@ public TestCaseGenerator(Proof proof, TestGenerationSettings settings, TGReporte
123114
: TestgenUtils::createAssignmentWithoutRfl;
124115

125116

126-
modDirName = services.getJavaModel().getModelDir();
117+
modDirName = Objects.requireNonNull(services.getJavaModel().getModelDir(),
118+
"No Java Source given in the JavaModel");
127119
outputFolder = new OutputEnvironment(Paths.get(settings.getOutputFolderPath()));
128120
outputModDir = outputFolder.getSourceDir();
129121
outputDontCopy = outputModDir.resolve(TestCaseGenerator.DONT_COPY);
@@ -282,7 +274,7 @@ public TypeSpec createRFLFileContent() {
282274
* Copy the involved classes without modification
283275
*/
284276
public void exportCodeUnderTest() throws IOException {
285-
copyFiles(Paths.get(modDirName), outputModDir);
277+
copyFiles(modDirName, outputModDir);
286278
}
287279

288280
public String getOracleAssertion(List<MethodSpec> oracleMethods) {

‎key.ui/src/main/java/de/uka/ilkd/key/core/Main.java‎

Lines changed: 12 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,6 @@
99
import java.net.URL;
1010
import java.nio.file.Files;
1111
import java.nio.file.Path;
12-
import java.nio.file.Paths;
13-
import java.util.ArrayList;
1412
import java.util.List;
1513
import java.util.Locale;
1614
import java.util.concurrent.Callable;
@@ -57,7 +55,7 @@
5755
*/
5856
public final class Main implements Callable<Integer> {
5957
private static final Logger LOGGER = LoggerFactory.getLogger(Main.class);
60-
private static File workingDir;
58+
private static Path workingDir;
6159

6260

6361
// @Option(names = "--help", description = "display this text")
@@ -129,7 +127,7 @@ public final class Main implements Callable<Integer> {
129127
@Option(names = "--tacletDir",
130128
description = "load base taclets from a directory, not from internal structures",
131129
paramLabel = "FOLDER")
132-
private @Nullable File tacletDir = null;
130+
private @Nullable Path tacletDir = null;
133131

134132
@Option(names = "--examples", paramLabel = "FOLDER",
135133
description = "load the directory containing the example files on startup")
@@ -140,7 +138,7 @@ public final class Main implements Callable<Integer> {
140138
*/
141139
@Option(names = "--rifl", paramLabel = "FILE",
142140
description = "load RIFL specifications from file (requires GUI and startup file)")
143-
public @Nullable File riflFileName = null;
141+
public @Nullable Path riflFileName = null;
144142

145143
/**
146144
* Save all contracts in selected location to automate the creation of multiple
@@ -223,7 +221,7 @@ public Main() {
223221
* The file names provided on the command line
224222
*/
225223
@Parameters(arity = "*")
226-
private List<File> inputFiles = List.of();
224+
private List<Path> inputFiles = List.of();
227225

228226
public static void main(final String[] args) {
229227
Locale.setDefault(Locale.US);
@@ -244,7 +242,7 @@ public Integer call() throws Exception {
244242

245243
if (tacletDir != null) {
246244
System.setProperty(RuleSourceFactory.STD_TACLET_DIR_PROP_KEY,
247-
tacletDir.getAbsolutePath());
245+
tacletDir.toAbsolutePath().toString());
248246
}
249247

250248
GeneralSettings.noPruningClosed = isNoPruningClosed;
@@ -312,7 +310,7 @@ public Integer call() throws Exception {
312310

313311
if (riflFileName != null) {
314312
LOGGER.info("Loading RIFL specification from {}", riflFileName);
315-
if (!riflFileName.exists()) {
313+
if (!Files.exists(riflFileName)) {
316314
LOGGER.info("RIFL does not exists {}", riflFileName);
317315
return 2;
318316
}
@@ -331,7 +329,7 @@ public Integer call() throws Exception {
331329

332330
if (macro != null) {
333331
for (ProofMacro m : ClassLoaderUtil.loadServices(ProofMacro.class)) {
334-
if (macro.equals(m.getScriptCommandName())) {
332+
if (macro.equals(m.getClass().getSimpleName())) {
335333
// memorize macro for later
336334
try {
337335
autoMacro = m.getClass().getDeclaredConstructor().newInstance();
@@ -352,7 +350,6 @@ public Integer call() throws Exception {
352350
}
353351
}
354352

355-
356353
AbstractMediatorUserInterfaceControl ui = createUserInterface(inputFiles);
357354
if (inputFiles.isEmpty()) {
358355
if (examplesFolder != null
@@ -364,7 +361,7 @@ public Integer call() throws Exception {
364361
} else {
365362
ui.setMacro(autoMacro);
366363
ui.setSaveOnly(isSaveAllContracts);
367-
for (File f : inputFiles) {
364+
for (Path f : inputFiles) {
368365
ui.loadProblem(f);
369366
}
370367

@@ -512,7 +509,7 @@ private static File createTempDirectory() throws IOException {
512509
*
513510
* @return {@link File} object representing working directory.
514511
*/
515-
public static File getWorkingDir() {
512+
public static Path getWorkingDir() {
516513
return workingDir;
517514
}
518515

@@ -539,11 +536,11 @@ private void preProcessInput()
539536
}
540537

541538
if (inputFiles != null && !inputFiles.isEmpty()) {
542-
File f = inputFiles.get(0);
543-
if (f.isDirectory()) {
539+
Path f = inputFiles.get(0);
540+
if (Files.isDirectory(f)) {
544541
workingDir = f;
545542
} else {
546-
workingDir = f.getParentFile();
543+
workingDir = f.getParent();
547544
}
548545
} else {
549546
workingDir = IOUtil.getCurrentDirectory();

‎key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
package de.uka.ilkd.key.gui.lemmatagenerator;
55

66
import java.io.File;
7+
import java.nio.file.Files;
8+
import java.nio.file.Path;
79
import java.util.Collection;
810
import java.util.LinkedList;
911

@@ -23,7 +25,7 @@ public class LemmataAutoModeOptions {
2325
* The path of the file containing the rules that should be proven.
2426
*/
2527
@CommandLine.Option(names = "--jr-rules", paramLabel = "FILE")
26-
private File pathOfRuleFile;
28+
private Path pathOfRuleFile;
2729

2830
/**
2931
* The maximum number of rules that are used within a proof.
@@ -63,7 +65,7 @@ public class LemmataAutoModeOptions {
6365

6466
@CommandLine.Option(names = "--jr-signature", paramLabel = "FILE",
6567
description = "read definitions from given file")
66-
public @Nullable File signature = null;
68+
public @Nullable Path signature = null;
6769

6870

6971
private final Collection<String> filesForAxioms = new LinkedList<>();
@@ -96,7 +98,7 @@ public boolean isSavingResultsToFile() {
9698
return saveResultsToFile;
9799
}
98100

99-
public File getPathOfRuleFile() {
101+
public Path getPathOfRuleFile() {
100102
return pathOfRuleFile;
101103
}
102104

@@ -117,7 +119,7 @@ public String createProofPath(Proof p) {
117119
}
118120

119121
private void checkForValidity() {
120-
if (pathOfRuleFile != null && !pathOfRuleFile.isFile()) {
122+
if (pathOfRuleFile != null && !Files.exists(pathOfRuleFile)) {
121123
throwError(String.format("Error while setting the file containing the rules:\n"
122124
+ "'%s' is not a valid file in your system.", pathOfRuleFile));
123125
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataHandler.java‎

Lines changed: 1 addition & 2 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.gui.lemmatagenerator;
55

6-
import java.io.File;
76
import java.io.IOException;
87
import java.nio.file.Path;
98
import java.nio.file.Paths;
@@ -62,7 +61,7 @@ public void start() throws IOException, ProofInputException {
6261
println("Start problem creation:");
6362
println(options.toString());
6463

65-
Path file = new File(options.getPathOfRuleFile()).toPath();
64+
Path file = options.getPathOfRuleFile();
6665
Collection<Path> filesForAxioms = createFilesForAxioms(options.getFilesForAxioms());
6766

6867
final ProblemInitializer problemInitializer =

‎keyext.slicing/src/main/java/org/key_project/slicing/Main.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -97,8 +97,8 @@ private void processFileOrDir(Path path, boolean overwrite) {
9797
}
9898
}
9999

100-
private void processFile(File proofFile, boolean overwrite) throws Exception {
101-
LOGGER.info("Processing proof: {}", proofFile.getName());
100+
private void processFile(Path proofFile, boolean overwrite) throws Exception {
101+
LOGGER.info("Processing proof: {}", proofFile.getFileName());
102102
GeneralSettings.noPruningClosed = false;
103103
AtomicReference<DependencyTracker> tracker = new AtomicReference<>();
104104
KeYEnvironment<?> environment =

0 commit comments

Comments
 (0)