repair normalform, wip

KeYProject · Jul 22, 2023 · 209349f · 209349f
1 parent 3da3422
commit 209349f
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
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
@@ -260,7 +260,8 @@ public IProgramMethod getConstructor(KeYJavaType ct, ImmutableList<KeYJavaType>
             List<ResolvedType> sig = signature.stream().map(this::getJavaParserType).toList();
 
             List<ResolvedConstructorDeclaration> 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<ResolvedType> 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/...main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java b/...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<Modifier> mods = new NodeList<>();
         var et = getImplicitEnclosingThis(cd);