Merge branch 'weigl/key-javaparser3' of https://github.com/KeYProject/key into weigl/key-javaparser3

Drodt · Drodt · commit 8e9cf61a7a5e · 2026-03-04T10:32:38.000+01:00
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java
@@ -94,7 +94,7 @@ public StatementBlock(Statement... body) {
     }
 
     public StatementBlock(PositionInfo pi, List<Comment> c, ImmutableArray<Statement> body,
-            List<TextualJMLSpecCase> spec) {
+            List<TextualJMLConstruct> spec) {
         this(pi, c, body);
         attacedJml.addAll(spec);
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java
@@ -3,8 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.ast.declaration;
 
-import java.util.List;
-
 import de.uka.ilkd.key.java.ast.Comment;
 import de.uka.ilkd.key.java.ast.PositionInfo;
 import de.uka.ilkd.key.java.ast.ProgramElement;
@@ -13,12 +11,13 @@
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
-
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
+import java.util.List;
+
 /**
  * There are several types of class declarations:
  * <ul>
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java
@@ -12,8 +12,9 @@
 import de.uka.ilkd.key.java.ast.reference.TypeReference;
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
 
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
@@ -69,7 +70,7 @@ public ConstructorDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<M
             TypeReference o, Comment[] comments, ProgramElementName name,
             ImmutableArray<ParameterDeclaration> map1,
             Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration,
-            List<TextualJMLSpecCase> specs) {
+            List<TextualJMLConstruct> specs) {
         this(pi, c, map, o, comments, name, map1, exceptions, body, parentIsInterfaceDeclaration);
         attachedJml.addAll(specs);
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java
@@ -25,12 +25,15 @@
 import de.uka.ilkd.key.java.ast.JavaNonTerminalProgramElement;
 import de.uka.ilkd.key.java.ast.PositionInfo;
 import de.uka.ilkd.key.java.ast.declaration.modifier.*;
+
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
 import org.jspecify.annotations.NonNull;
+import org.key_project.util.collection.ImmutableList;
 
 /**
  * Java declaration.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java
@@ -13,7 +13,7 @@
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
 import de.uka.ilkd.key.speclang.njml.SpecMathMode;
 
 import org.key_project.util.ExtList;
@@ -111,7 +111,7 @@ public MethodDeclaration(
             Comment[] voidComments, ProgramElementName name,
             ImmutableArray<ParameterDeclaration> parameters, Throws exceptions,
             StatementBlock body, boolean parentIsInterfaceDeclaration,
-            List<TextualJMLSpecCase> specs) {
+            List<TextualJMLConstruct> specs) {
         this(pi, comments, modArray, returnType, voidComments, name, parameters, exceptions,
             body, parentIsInterfaceDeclaration);
         attachedJml.addAll(specs);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java
@@ -8,8 +8,9 @@
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
 
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
 import org.key_project.util.ExtList;
 
 /**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java
@@ -9,8 +9,9 @@
 import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration;
 import de.uka.ilkd.key.java.visitor.CreatingASTVisitor;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
 
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
 import org.key_project.util.ExtList;
 
 import org.jspecify.annotations.NonNull;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java
@@ -10,8 +10,10 @@
 import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
 
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java
@@ -8,8 +8,9 @@
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
 
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec;
+import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase;
 import org.key_project.util.ExtList;
 
 /**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java
@@ -3,11 +3,30 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.loader;
 
-import java.net.URI;
-import java.util.*;
-import java.util.function.Predicate;
-import java.util.stream.Collectors;
-
+import com.github.javaparser.ast.*;
+import com.github.javaparser.ast.Modifier;
+import com.github.javaparser.ast.body.*;
+import com.github.javaparser.ast.body.ConstructorDeclaration;
+import com.github.javaparser.ast.body.FieldDeclaration;
+import com.github.javaparser.ast.body.MethodDeclaration;
+import com.github.javaparser.ast.comments.TraditionalJavadocComment;
+import com.github.javaparser.ast.expr.*;
+import com.github.javaparser.ast.key.*;
+import com.github.javaparser.ast.key.sv.*;
+import com.github.javaparser.ast.modules.*;
+import com.github.javaparser.ast.nodeTypes.NodeWithModifiers;
+import com.github.javaparser.ast.stmt.*;
+import com.github.javaparser.ast.type.*;
+import com.github.javaparser.ast.visitor.GenericVisitorAdapter;
+import com.github.javaparser.ast.visitor.Visitable;
+import com.github.javaparser.resolution.UnsolvedSymbolException;
+import com.github.javaparser.resolution.declarations.ResolvedValueDeclaration;
+import com.github.javaparser.resolution.model.typesystem.ReferenceTypeImpl;
+import com.github.javaparser.resolution.types.ResolvedType;
+import com.github.javaparser.resolution.types.ResolvedVoidType;
+import com.github.javaparser.symbolsolver.JavaSymbolSolver;
+import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserFieldDeclaration;
+import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserVariableDeclaration;
 import de.uka.ilkd.key.java.*;
 import de.uka.ilkd.key.java.ast.*;
 import de.uka.ilkd.key.java.ast.CompilationUnit;
@@ -38,43 +57,22 @@
 import de.uka.ilkd.key.logic.sort.ProgramSVSort;
 import de.uka.ilkd.key.rule.metaconstruct.*;
 import de.uka.ilkd.key.speclang.jml.pretranslation.*;
-
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 import org.key_project.logic.Namespace;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.op.sv.OperatorSV;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
 import org.key_project.util.collection.ImmutableArray;
-
-import com.github.javaparser.ast.*;
-import com.github.javaparser.ast.Modifier;
-import com.github.javaparser.ast.body.*;
-import com.github.javaparser.ast.body.ConstructorDeclaration;
-import com.github.javaparser.ast.body.FieldDeclaration;
-import com.github.javaparser.ast.body.MethodDeclaration;
-import com.github.javaparser.ast.comments.TraditionalJavadocComment;
-import com.github.javaparser.ast.expr.*;
-import com.github.javaparser.ast.key.*;
-import com.github.javaparser.ast.key.sv.*;
-import com.github.javaparser.ast.modules.*;
-import com.github.javaparser.ast.nodeTypes.NodeWithModifiers;
-import com.github.javaparser.ast.stmt.*;
-import com.github.javaparser.ast.type.*;
-import com.github.javaparser.ast.visitor.GenericVisitorAdapter;
-import com.github.javaparser.ast.visitor.Visitable;
-import com.github.javaparser.resolution.UnsolvedSymbolException;
-import com.github.javaparser.resolution.declarations.ResolvedValueDeclaration;
-import com.github.javaparser.resolution.model.typesystem.ReferenceTypeImpl;
-import com.github.javaparser.resolution.types.ResolvedType;
-import com.github.javaparser.resolution.types.ResolvedVoidType;
-import com.github.javaparser.symbolsolver.JavaSymbolSolver;
-import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserFieldDeclaration;
-import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserVariableDeclaration;
-import org.jspecify.annotations.NonNull;
-import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import java.net.URI;
+import java.util.*;
+import java.util.function.Predicate;
+import java.util.stream.Collectors;
+
 import static com.github.javaparser.ast.Modifier.DefaultKeyword.*;
 import static java.lang.String.format;
 
@@ -809,7 +807,7 @@ public Object visit(ForStmt n, Void arg) {
         return new For(pi, c, forInit, forUpdates, forGuard, accept(n.getBody()), getLoopSpec(n));
     }
 
-    public static List<TextualJMLSpecCase> getSpec(Node n) {
+    public static List<TextualJMLConstruct> getSpec(Node n) {
         try {
             return n.getData(JMLTransformer.KEY_SPEC_CASE);
         } catch (IllegalStateException e) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java
@@ -16,22 +16,6 @@
 
 package de.uka.ilkd.key.java.transformations.pipeline;
 
-import java.net.URI;
-import java.util.*;
-import java.util.regex.Pattern;
-
-import de.uka.ilkd.key.parser.Location;
-import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.speclang.PositionedString;
-import de.uka.ilkd.key.speclang.jml.pretranslation.*;
-import de.uka.ilkd.key.speclang.njml.PreParser;
-import de.uka.ilkd.key.speclang.translation.SLTranslationException;
-import de.uka.ilkd.key.util.MiscTools;
-
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.StringUtil;
-
 import com.github.javaparser.*;
 import com.github.javaparser.ast.*;
 import com.github.javaparser.ast.body.*;
@@ -51,12 +35,26 @@
 import com.github.javaparser.ast.type.Type;
 import com.github.javaparser.ast.visitor.VoidVisitorWithDefaults;
 import com.google.common.base.Strings;
+import de.uka.ilkd.key.parser.Location;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
+import de.uka.ilkd.key.speclang.PositionedString;
+import de.uka.ilkd.key.speclang.jml.pretranslation.*;
+import de.uka.ilkd.key.speclang.njml.PreParser;
+import de.uka.ilkd.key.speclang.translation.SLTranslationException;
+import de.uka.ilkd.key.util.MiscTools;
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.misc.Interval;
 import org.jspecify.annotations.NonNull;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.java.StringUtil;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import java.net.URI;
+import java.util.*;
+import java.util.regex.Pattern;
+
 
 /**
  * RecodeR transformation that parses JML comments, and attaches code-like
@@ -342,6 +340,7 @@ private MethodDeclaration transformMethodDecl(TextualJMLMethodDecl decl)
         if (decl.getModifiers().contains(JMLModifier.NO_STATE)) {
             methodDecl.addModifier(Modifier.DefaultKeyword.JML_NO_STATE);
         }
+        addSpec(methodDecl, decl);
         return methodDecl;
     }
 
@@ -410,7 +409,7 @@ private static <T> Optional<T> extractData(Node node, DataKey<T> key) {
     private final JmlDocSanitizer sanitizer = new JmlDocSanitizer(Set.of("key"));
 
 
-    public static final DataKey<List<TextualJMLSpecCase>> KEY_SPEC_CASE = new DataKey<>() {
+    public static final DataKey<List<TextualJMLConstruct>> KEY_SPEC_CASE = new DataKey<>() {
     };
     public static final DataKey<List<TextualJMLConstruct>> KEY_CLASS_SPEC = new DataKey<>() {
     };
@@ -483,11 +482,11 @@ private void addClassSpec(TypeDeclaration<?> td, TextualJMLConstruct c) {
         specList.add(c);
     }
 
-    private void addSpec(Node nextMember, TextualJMLSpecCase specCase) {
+    private void addSpec(Node nextMember, TextualJMLConstruct specCase) {
         if (!nextMember.containsData(KEY_SPEC_CASE)) {
             nextMember.setData(KEY_SPEC_CASE, new ArrayList<>(4));
         }
-        List<TextualJMLSpecCase> specList = nextMember.getData(KEY_SPEC_CASE);
+        List<TextualJMLConstruct> specList = nextMember.getData(KEY_SPEC_CASE);
         specList.add(specCase);
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
@@ -337,13 +337,22 @@ public List<SpecificationElement> extractMethodSpecs(IProgramMethod pm, boolean
         // get textual JML constructs
         var constructs = pm.getMethodDeclaration().getAttachedJml();
 
+        ParserRuleContext modelMethodDefinition = null;
+        for (var c : constructs) {
+            if (c instanceof TextualJMLMethodDecl m) {
+                if (pm.getMethodDeclaration().containsModifier(Modifiers.JML_MODEL.class)) {
+                    modelMethodDefinition = m.getMethodDefinition();
+                    break;
+                }
+            }
+        }
+
+
         for (var c : constructs) {
             if (c instanceof TextualJMLSpecCase specCase) {
-                /*
-                 * if (modelMethodDecl != null && modelMethodDecl.getMethodDefinition() != null) {
-                 * specCase.addClause(AXIOMS, null, modelMethodDecl.getMethodDefinition());
-                 * }
-                 */
+                if (modelMethodDefinition != null) {
+                    specCase.addClause(AXIOMS, null, modelMethodDefinition);
+                }
 
                 // add purity. Strict purity overrides purity.
                 if (isStrictlyPure || pm.isModel()) {

Original file line number	Diff line number	Diff line change
`@@ -94,7 +94,7 @@ public StatementBlock(Statement... body) {`
`94`	`94`	`}`
`95`	`95`
`96`	`96`	`public StatementBlock(PositionInfo pi, List<Comment> c, ImmutableArray<Statement> body,`
`97`		`- List<TextualJMLSpecCase> spec) {`
	`97`	`+ List<TextualJMLConstruct> spec) {`
`98`	`98`	`this(pi, c, body);`
`99`	`99`	`attacedJml.addAll(spec);`
`100`	`100`	`}`