diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java index cc1a9ea62ab..3ac2e643f85 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java @@ -260,7 +260,8 @@ public IProgramMethod getConstructor(KeYJavaType ct, ImmutableList List sig = signature.stream().map(this::getJavaParserType).toList(); List constructors = rt.get().getConstructors(); - constr: for (var constructor : constructors) { + constr: + for (var constructor : constructors) { if (sig.size() != constructor.getNumberOfParams()) { continue; } @@ -336,6 +337,10 @@ public IProgramMethod getProgramMethod(@Nonnull KeYJavaType ct, String name, List jpSignature = StreamSupport.stream(signature.spliterator(), false) .map(this::getJavaParserType).toList(); var method = MethodResolutionLogic.solveMethodInType(rct, name, jpSignature); + + if (!method.isSolved()) + return null; + return method.getDeclaration() .map(d -> (IProgramMethod) Objects.requireNonNull(mapping.resolvedDeclarationToKeY(d))) .orElse(null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java index f77734e8c04..a3b9f004c02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java @@ -73,9 +73,6 @@ private void attachDefaultConstructor(ClassOrInterfaceDeclaration cd) { */ private void normalform(ClassOrInterfaceDeclaration cd, ConstructorDeclaration cons) { final var enclosingClass = getEnclosingClass(cd); - if (enclosingClass.isEmpty()) { - return; // throw reportError(cd, "No enclosing class found"); - } NodeList mods = new NodeList<>(); var et = getImplicitEnclosingThis(cd);