Skip to content

Commit 8256cc5

Browse files
committed
Fix some tests
1 parent 70607d7 commit 8256cc5

3 files changed

Lines changed: 22 additions & 13 deletions

File tree

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
import de.uka.ilkd.key.java.statement.*;
3232
import de.uka.ilkd.key.ldt.HeapLDT;
3333
import de.uka.ilkd.key.ldt.JavaDLTheory;
34+
import de.uka.ilkd.key.logic.GenericArgument;
3435
import de.uka.ilkd.key.logic.NamespaceSet;
3536
import de.uka.ilkd.key.logic.ProgramElementName;
3637
import de.uka.ilkd.key.logic.VariableNamer;
@@ -794,7 +795,15 @@ public DLEmbeddedExpression convert(EscapeExpression e) {
794795
}
795796

796797

797-
final Function named = namespaceSet.functions().lookup(new Name(name));
798+
Function named = namespaceSet.functions().lookup(new Name(name));
799+
800+
if (named == null && name.contains("<[")) {
801+
int index = name.indexOf("<");
802+
name = name.substring(0, index);
803+
ParametricFunctionDecl base = namespaceSet.parametricFunctions().lookup(name);
804+
named = ParametricFunctionInstance.get(base,
805+
ImmutableList.of(new GenericArgument(JavaDLTheory.ANY)), services);
806+
}
798807

799808
if (named == null) {
800809
// TODO provide position information?!

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ public Expression getDefaultValue(Type type) {
7878
case "\\locset" -> EmptySetLiteral.INSTANCE;
7979
case "\\seq" -> EmptySeqLiteral.INSTANCE;
8080
case "\\set" -> new DLEmbeddedExpression("emptySet", Collections.emptyList());
81-
case "\\TYPE" -> new DLEmbeddedExpression("any::ssort", Collections.emptyList());
81+
case "\\TYPE" -> new DLEmbeddedExpression("ssort<[any]>", Collections.emptyList());
8282
case "\\free" -> new DLEmbeddedExpression("atom", Collections.emptyList());
8383
case "\\map" -> EmptyMapLiteral.INSTANCE;
8484
default -> {

key.ui/examples/standard_key/staticInitialisation/objectOfErroneousClass.key

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -44,43 +44,43 @@
4444
wellFormed(heap)
4545
& select<[boolean]>(heap,
4646
null,
47-
java.lang.NoClassDefFoundError::<classInitialized>)
47+
<classInitialized><[java.lang.NoClassDefFoundError]>)
4848
= TRUE
4949
& select<[boolean]>(heap,
5050
null,
51-
java.lang.ArithmeticException::<classInitialized>)
51+
<classInitialized><[java.lang.ArithmeticException]>)
5252
= TRUE
5353
& select<[boolean]>(heap,
5454
null,
55-
java.lang.NullPointerException::<classInitialized>)
55+
<classInitialized><[java.lang.NullPointerException]>)
5656
= TRUE
5757
& select<[boolean]>(heap,
5858
null,
59-
A::<classInitialized>)
59+
<classInitialized><[A]>)
6060
= FALSE
6161
& select<[boolean]>(heap, null, A::<classPrepared>)
6262
= FALSE
6363
& select<[boolean]>(heap,
6464
null,
65-
A::<classInitializationInProgress>)
65+
<classInitializationInProgress><[A]>)
6666
= FALSE
67-
& select<[boolean]>(heap, null, A::<classErroneous>)
67+
& select<[boolean]>(heap, null, <classErroneous><[A]>)
6868
= FALSE
6969
& select<[boolean]>(heap,
7070
null,
71-
FailedStaticInit::<classInitialized>)
71+
<classInitialized><[FailedStaticInit]>)
7272
= FALSE
7373
& select<[boolean]>(heap,
7474
null,
75-
FailedStaticInit::<classPrepared>)
75+
<classPrepared><[FailedStaticInit]>)
7676
= FALSE
7777
& select<[boolean]>(heap,
7878
null,
79-
FailedStaticInit::<classInitializationInProgress>)
79+
<classInitializationInProgress><[FailedStaticInit]>)
8080
= FALSE
8181
& select<[boolean]>(heap,
8282
null,
83-
FailedStaticInit::<classErroneous>)
83+
<classErroneous><[FailedStaticInit]>)
8484
= FALSE
8585
-> \<{
8686
errorWhileProcessingMethod=false;try {
@@ -92,7 +92,7 @@
9292
}
9393
}\> ( select<[boolean]>(heap,
9494
null,
95-
FailedStaticInit::<classErroneous>)
95+
<classErroneous><[FailedStaticInit]>)
9696
= TRUE
9797
& select<[int]>(heap,
9898
fsi,

0 commit comments

Comments
 (0)