Skip to content

Commit 73ee6c3

Browse files
committed
fix some tests
1 parent 4f9eaab commit 73ee6c3

7 files changed

Lines changed: 73 additions & 13 deletions

File tree

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
import java.io.IOException;
77
import java.util.Collection;
88
import java.util.List;
9+
import java.util.NoSuchElementException;
910
import java.util.concurrent.Callable;
1011

1112
import de.uka.ilkd.key.control.KeYEnvironment;
@@ -66,7 +67,7 @@ public void launcherStopped(SolverLauncher launcher,
6667

6768
tg.generateJUnitTestSuite(finishedSolvers);
6869
reporter.writeln("Compile the generated files using a Java compiler.");
69-
} catch (IOException e) {
70+
} catch (NoSuchElementException | IOException e) {
7071
reporter.reportException(e);
7172
}
7273
}

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Assignment.java

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
package de.uka.ilkd.key.java.ast.expression;
55

66
import java.util.List;
7+
import java.util.Objects;
78

89
import de.uka.ilkd.key.java.Services;
910
import de.uka.ilkd.key.java.ast.Comment;
@@ -130,4 +131,18 @@ public String reuseSignature(Services services, ExecutionContext ec) {
130131
return base;
131132
}
132133
}
134+
135+
@Override
136+
public boolean equals(Object o) {
137+
if (!(o instanceof Assignment that))
138+
return false;
139+
if (!super.equals(o))
140+
return false;
141+
return kind == that.kind && Objects.equals(that.children, children);
142+
}
143+
144+
@Override
145+
protected int computeHashCode() {
146+
return Objects.hash(kind, children);
147+
}
133148
}

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,4 +114,18 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
114114
public void visit(Visitor v) {
115115
v.performActionOnBinaryOperator(this);
116116
}
117+
118+
@Override
119+
public boolean equals(Object o) {
120+
if (this == o)
121+
return true;
122+
if (!(o instanceof BinaryOperator b))
123+
return false;
124+
return Objects.equals(getKind(), b.getKind()) && Objects.equals(children, b.children);
125+
}
126+
127+
@Override
128+
protected int computeHashCode() {
129+
return Objects.hash(kind, children);
130+
}
117131
}

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LogicFunctionalOperator.java

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
package de.uka.ilkd.key.java.ast.expression.operator;
55

66
import java.util.List;
7+
import java.util.Objects;
78

89
import de.uka.ilkd.key.java.Services;
910
import de.uka.ilkd.key.java.ast.Comment;
@@ -105,4 +106,18 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
105106
public void visit(Visitor v) {
106107
v.performActionOnLogicFunctionalOperator(this);
107108
}
109+
110+
@Override
111+
public boolean equals(Object o) {
112+
if (!(o instanceof LogicFunctionalOperator that))
113+
return false;
114+
if (!super.equals(o))
115+
return false;
116+
return function == that.function && Objects.equals(that.children, children);
117+
}
118+
119+
@Override
120+
protected int computeHashCode() {
121+
return Objects.hash(function, children);
122+
}
108123
}

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/UnaryOperator.java

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
package de.uka.ilkd.key.java.ast.expression.operator;
55

66
import java.util.List;
7+
import java.util.Objects;
78

89
import de.uka.ilkd.key.java.Services;
910
import de.uka.ilkd.key.java.ast.Comment;
@@ -90,4 +91,18 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
9091
public void visit(Visitor v) {
9192
v.performActionOnUnaryOperator(this);
9293
}
94+
95+
@Override
96+
public boolean equals(Object o) {
97+
if (!(o instanceof UnaryOperator that))
98+
return false;
99+
if (!super.equals(o))
100+
return false;
101+
return kind == that.kind && Objects.equals(that.children, children);
102+
}
103+
104+
@Override
105+
protected int computeHashCode() {
106+
return Objects.hash(kind, children);
107+
}
93108
}

key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/DiskFileRepo.java

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import java.nio.file.Paths;
1313
import java.util.Comparator;
1414
import java.util.HashMap;
15+
import java.util.stream.Stream;
1516

1617
import de.uka.ilkd.key.settings.GeneralSettings;
1718

@@ -342,17 +343,15 @@ protected void dispose() {
342343
*/
343344
private void deleteDiskContent() throws IOException {
344345
if (!isDisposed() && !GeneralSettings.keepFileRepos) {
345-
try (var s = Files.walk(tmpDir)) {
346-
s.sorted(Comparator.reverseOrder())
347-
// .map(Path::toFile)
348-
.forEach(path -> {
349-
try {
350-
Files.delete(path);
351-
// path.delete();
352-
} catch (IOException e) {
353-
LOGGER.info("Failed to delete file", e);
354-
}
355-
});
346+
try (Stream<Path> s = Files.walk(tmpDir).sorted(Comparator.reverseOrder())) {
347+
s.forEach(path -> {
348+
try {
349+
Files.deleteIfExists(path);
350+
// path.delete();
351+
} catch (IOException e) {
352+
LOGGER.info("Could not clean up temp directory {}", path);
353+
}
354+
});
356355
}
357356
}
358357
}

key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1635,7 +1635,8 @@ private StatementBlock constructAbruptTerminationIfCascade() {
16351635
KeYJavaASTFactory.returnClause(variables.result)));
16361636
}
16371637
ifCascade.add(KeYJavaASTFactory.ifThen(
1638-
new BinaryOperator(BinaryOperator.BinaryOperatorKind.NOT_EQUALS, variables.exception,
1638+
new BinaryOperator(BinaryOperator.BinaryOperatorKind.NOT_EQUALS,
1639+
variables.exception,
16391640
NullLiteral.NULL),
16401641
KeYJavaASTFactory.throwClause(variables.exception)));
16411642
return new StatementBlock(ifCascade.toArray(new Statement[0]));

0 commit comments

Comments
 (0)