Skip to content

Commit cf787ae

Browse files
committed
fix TestJavaDLASTExtensions
1 parent d908b8f commit cf787ae

3 files changed

Lines changed: 7 additions & 11 deletions

File tree

key.core/build.gradle

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ dependencies {
2222

2323
api project(':key.util')
2424

25-
def JP_VERSION = "3.28.0-K13.4"
25+
def JP_VERSION = "3.28.0-K13.5"
2626
api "org.key-project.proofjava:javaparser-core:$JP_VERSION"
2727
api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION"
2828
api "org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION"

key.core/src/test/java/de/uka/ilkd/key/java/TestJavaDLASTExtensions.java

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -62,16 +62,12 @@ public void testTypeNotInInnerScopeShouldNotBeFound() {
6262
@Test
6363
public void testNestedMethodFrameRedirects() {
6464
try {
65-
HelperClassForTests
66-
.parseThrowException(
65+
HelperClassForTests.parseThrowException(
6766
testpath.resolve("typeResolutionInNestedMethodFrameResolvable.key"));
6867
} catch (Throwable t) {
69-
Assertions.fail("Resolution of type " +
70-
"TestJavaCardDLExtensions should be successful as it is enclosed by the outer method frame "
71-
+
72-
"which redirects the scope to package sub1. Class Third should be resolvable (and visible) as the"
73-
+
74-
"inner method-frame redirects to package sub2.\n " + t);
68+
Assertions.fail("Resolution of type TestJavaCardDLExtensions should be successful as it is enclosed by the outer method frame " +
69+
"which redirects the scope to package sub1. Class Third should be resolvable (and visible) as the inner method-frame redirects to package sub2." +
70+
"\n\n" + t);
7571
}
7672

7773
}

key.core/src/test/resources/testcase/javaASTExtensions/typeResolutionInNestedMethodFrameResolvable.key

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@
1010
\problem {
1111

1212
\<{ method-frame(source=setSize(int)@sub1.TestJavaCardDLExtensions) {
13-
method-frame(source=setSize(int)@sub2.Other) {
14-
Third three = null;
13+
method-frame(source=setOther(int)@sub2.Other) {
14+
Third three = new Third();
1515
}
1616
TestJavaCardDLExtensions t = null;
1717
}

0 commit comments

Comments
 (0)