diff --git a/build.gradle b/build.gradle index b6a7211b062..b4139d8e175 100644 --- a/build.gradle +++ b/build.gradle @@ -76,7 +76,7 @@ subprojects { repositories { mavenCentral() //maven { url = "https://git.key-project.org/api/v4/projects/35/packages/maven/" } - //maven { url = "https://central.sonatype.com/repository/maven-snapshots/" } + maven { url = "https://central.sonatype.com/repository/maven-snapshots/" } } dependencies { diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 4a4eb38b8f8..ba34b56236c 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -23,7 +23,7 @@ stringtemplate = "4.3.4" # Java parsing and analysis javapoet = "1.13.0" -javaparser = "3.28.0-K13.6" +javaparser = "3.28.2-J8.0-K13.5-SNAPSHOT" truth = "1.4.5" # UI and CLI @@ -67,9 +67,9 @@ stringtemplate = { module = "org.antlr:ST4", version.ref = "stringtemplate" } # Java source code processing javapoet = { module = "com.squareup:javapoet", version.ref = "javapoet" } -javaparser-core = { module = "org.key-project.proofjava:javaparser-core", version.ref = "javaparser" } -javaparser-core-serialization = { module = "org.key-project.proofjava:javaparser-core-serialization", version.ref = "javaparser" } -javaparser-symbol-solver-core = { module = "org.key-project.proofjava:javaparser-symbol-solver-core", version.ref = "javaparser" } +javaparser-core = { module = "io.github.jmltoolkit:jmlparser-core", version.ref = "javaparser" } +javaparser-core-serialization = { module = "io.github.jmltoolkit:jmlparser-core-serialization", version.ref = "javaparser" } +javaparser-symbol-solver-core = { module = "io.github.jmltoolkit:jmlparser-symbol-solver-core", version.ref = "javaparser" } # Testing utilities truth = { module = "com.google.truth:truth", version.ref = "truth" } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java index beb6fa277e1..d5245e39b4e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java @@ -5,24 +5,26 @@ import java.util.List; -import de.uka.ilkd.key.java.*; -import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Comment; +import de.uka.ilkd.key.java.ast.PositionInfo; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.SourceData; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.rule.MatchConditions; -import com.github.javaparser.ast.key.KeyTransactionStatement; +import com.github.javaparser.ast.key.KeyTransactionStmt; public class TransactionStatement extends JavaStatement { - private final KeyTransactionStatement.TransactionType type; + private final KeyTransactionStmt.TransactionType type; - public TransactionStatement(KeyTransactionStatement.TransactionType type) { + public TransactionStatement(KeyTransactionStmt.TransactionType type) { super(); this.type = type; } public TransactionStatement( PositionInfo pi, List c, - KeyTransactionStatement.TransactionType type) { + KeyTransactionStmt.TransactionType type) { super(pi, c); this.type = type; } 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 index 773c8bcbb0b..11e95e0e009 100644 --- 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 @@ -60,6 +60,8 @@ 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.jml.stmt.JmlExpressionStmt; +import com.github.javaparser.ast.jml.stmt.JmlExpressionStmt.JmlStmtKind; import com.github.javaparser.ast.key.*; import com.github.javaparser.ast.key.sv.*; import com.github.javaparser.ast.modules.*; @@ -278,6 +280,8 @@ public Object visit(BinaryExpr n, Void arg) { case MULTIPLY -> BinaryOperatorKind.TIMES; case DIVIDE -> BinaryOperatorKind.DIVIDE; case REMAINDER -> BinaryOperatorKind.MODULO; + default -> + throw new IllegalStateException("JML operators not allowed: " + n.getOperator()); }; return new BinaryOperator(pi, c, op, lhs, rhs); } @@ -760,32 +764,21 @@ private ClassOrInterfaceDeclaration getContainingClass(Node node) { } @Override - public Object visit(KeYMarkerStatement n, Void arg) { + public Object visit(JmlExpressionStmt n, Void arg) { PositionInfo pi = createPositionInfo(n); return switch (n.getKind()) { - case MarkerStatementHelper.KIND_ASSERT -> { + case JmlStmtKind.ASSERT -> { TextualJMLAssertStatement construct = n.getData(MarkerStatementHelper.KEY_ASSERT); yield new JmlAssert(TextualJMLAssertStatement.Kind.ASSERT, construct, pi); } - case MarkerStatementHelper.KIND_ASSUME -> { + case JmlStmtKind.ASSUME -> { TextualJMLAssertStatement construct = n.getData(MarkerStatementHelper.KEY_ASSERT); yield new JmlAssert(TextualJMLAssertStatement.Kind.ASSUME, construct, pi); } - case MarkerStatementHelper.KIND_SET -> { + case JmlStmtKind.SET -> { KeyAst.SetStatementContext context = n.getData(MarkerStatementHelper.KEY_ASSIGN); yield new SetStatement(context, pi); } - - - case MarkerStatementHelper.KIND_MERGE_POINT -> { - var loc = new LocationVariable( - services.getVariableNamer().getTemporaryNameProposal("x"), - services.getNamespaces().sorts().lookup("boolean")); - List c = createComments(n); - - TextualJMLMergePointDecl a = n.getData(MarkerStatementHelper.KEY_MERGE_POINT); - yield new MergePointStatement(pi, c, a, loc); - } default -> throw new IllegalStateException("Unexpected value: " + n.getKind()); }; } @@ -1696,7 +1689,7 @@ public Object visit(KeyCcatchReturn n, Void arg) { } @Override - public Object visit(KeyCatchAllStatement n, Void arg) { + public Object visit(KeyCatchAllStmt n, Void arg) { // TODO return reportUnsupportedElement(n); } @@ -1801,7 +1794,7 @@ private ImmutableArray map( } @Override - public Object visit(KeyExecStatement n, Void arg) { + public Object visit(KeyExecStmt n, Void arg) { PositionInfo pi = createPositionInfo(n); var c = createComments(n); StatementBlock body = accept(n.getExecBlock()); @@ -1825,7 +1818,7 @@ public Object visit(KeyExecutionContext n, Void arg) { } @Override - public Object visit(KeyLoopScopeBlock n, Void arg) { + public Object visit(KeyLoopScopeBlockStmt n, Void arg) { PositionInfo pi = createPositionInfo(n); List c = createComments(n); StatementBlock body = accept(n.getBlock()); @@ -1834,11 +1827,15 @@ public Object visit(KeyLoopScopeBlock n, Void arg) { } @Override - public Object visit(KeyMergePointStatement n, Void arg) { + public Object visit(KeyMergePointStmt n, Void arg) { var pi = createPositionInfo(n); List c = createComments(n); - IProgramVariable expr = accept(n.getExpr()); - return new MergePointStatement(pi, c, null, expr); + // IProgramVariable expr = accept(n.getExpr()); + var loc = new LocationVariable( + services.getVariableNamer().getTemporaryNameProposal("x"), + services.getNamespaces().sorts().lookup("boolean")); + TextualJMLMergePointDecl a = n.getData(MarkerStatementHelper.KEY_MERGE_POINT); + return new MergePointStatement(pi, c, a, loc); } @Override @@ -1861,7 +1858,7 @@ public Object visit(KeyMethodBodyStatement n, Void arg) { } @Override - public Object visit(KeyMethodCallStatement n, Void arg) { + public Object visit(KeyMethodCallStmt n, Void arg) { PositionInfo pi = createPositionInfo(n); List c = createComments(n); IProgramVariable resultVar = accepto(n.getName()); @@ -1885,7 +1882,7 @@ private IProgramMethod resolveMethodSignature(KeYJavaType type, KeyMethodSignatu } @Override - public Object visit(KeyTransactionStatement n, Void arg) { + public Object visit(KeyTransactionStmt n, Void arg) { PositionInfo pi = createPositionInfo(n); List c = createComments(n); return new TransactionStatement(pi, c, n.getType()); @@ -2190,11 +2187,6 @@ public Object visit(RecordDeclaration n, Void arg) { public Object visit(CompactConstructorDeclaration n, Void arg) { return reportUnsupportedElement(n); } - - @Override - public Object visit(KeyRangeExpression n, Void arg) { - return reportUnsupportedElement(n); - } // endregion @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java index f30cedc7188..7883b723445 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java @@ -11,7 +11,6 @@ import com.github.javaparser.ast.expr.*; import com.github.javaparser.ast.key.KeyEscapeExpression; import com.github.javaparser.ast.key.KeyPassiveExpression; -import com.github.javaparser.ast.key.KeyRangeExpression; import com.github.javaparser.ast.key.sv.KeyExpressionSV; import com.github.javaparser.ast.key.sv.KeyMetaConstructExpression; import com.github.javaparser.ast.stmt.ExplicitConstructorInvocationStmt; @@ -79,7 +78,7 @@ public Expression evaluate(String string) throws EvaluationException { private static class ConstantExpressionEvaluatorVisitor extends GenericVisitorAdapter { - private Queue path = new LinkedList(); + private final Queue path = new LinkedList<>(); @Override public Object visit(ArrayAccessExpr n, Void arg) { @@ -106,6 +105,9 @@ public Object visit(BinaryExpr n, Void arg) { Object left = n.getLeft().accept(this, arg); Object right = n.getRight().accept(this, arg); return switch (n.getOperator()) { + case IMPLICATION, ANTIVALENCE, EQUIVALENCE, RIMPLICATION, SUB_LOCKE, SUB_LOCK, + RANGE, SUBTYPE -> + throw new RuntimeException(); case OR -> { if (left instanceof Boolean && right instanceof Boolean) yield ((Boolean) left) || (Boolean) right; @@ -428,12 +430,6 @@ public Object visit(KeyEscapeExpression n, Void arg) { } - @Override - public Object visit(KeyRangeExpression n, Void arg) { - throw new RuntimeException("unsupported expression"); - - } - @Override public Object visit(KeyExpressionSV n, Void arg) { throw new RuntimeException("unsupported expression"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java index 7061b68e91c..e8c5d7fc483 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java @@ -28,6 +28,10 @@ import com.github.javaparser.ast.comments.MarkdownComment; import com.github.javaparser.ast.comments.TraditionalJavadocComment; import com.github.javaparser.ast.expr.*; +import com.github.javaparser.ast.jml.doc.JmlDoc; +import com.github.javaparser.ast.jml.doc.JmlDocDeclaration; +import com.github.javaparser.ast.jml.doc.JmlDocStmt; +import com.github.javaparser.ast.jml.doc.JmlDocType; import com.github.javaparser.ast.key.*; import com.github.javaparser.ast.key.sv.*; import com.github.javaparser.ast.modules.ModuleDeclaration; @@ -689,7 +693,7 @@ public void visit(KeyCcatchReturn n, Object arg) { } @Override - public void visit(KeyCatchAllStatement n, Object arg) { + public void visit(KeyCatchAllStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @@ -701,7 +705,7 @@ public void visit(KeyEscapeExpression n, Object arg) { } @Override - public void visit(KeyExecStatement n, Object arg) { + public void visit(KeyExecStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @@ -713,13 +717,13 @@ public void visit(KeyExecutionContext n, Object arg) { } @Override - public void visit(KeyLoopScopeBlock n, Object arg) { + public void visit(KeyLoopScopeBlockStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @Override - public void visit(KeyMergePointStatement n, Object arg) { + public void visit(KeyMergePointStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @@ -731,7 +735,7 @@ public void visit(KeyMethodBodyStatement n, Object arg) { } @Override - public void visit(KeyMethodCallStatement n, Object arg) { + public void visit(KeyMethodCallStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @@ -743,13 +747,7 @@ public void visit(KeyMethodSignature n, Object arg) { } @Override - public void visit(KeyRangeExpression n, Object arg) { - super.visit(n, arg); - defaultAction(n, arg); - } - - @Override - public void visit(KeyTransactionStatement n, Object arg) { + public void visit(KeyTransactionStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @@ -863,25 +861,19 @@ public void visit(JmlDoc n, Object arg) { } @Override - public void visit(JmlDocsBodyDeclaration n, Object arg) { - super.visit(n, arg); - defaultAction(n, arg); - } - - @Override - public void visit(JmlDocsTypeDeclaration n, Object arg) { + public void visit(JmlDocDeclaration n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @Override - public void visit(JmlDocsStatements n, Object arg) { + public void visit(JmlDocType n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @Override - public void visit(KeYMarkerStatement n, Object arg) { + public void visit(JmlDocStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } 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 index 6db5f5ed9ed..8b8ed76b566 100644 --- 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 @@ -20,10 +20,17 @@ import org.key_project.util.collection.ImmutableList; import com.github.javaparser.*; -import com.github.javaparser.ast.*; +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.DataKey; +import com.github.javaparser.ast.Modifier; +import com.github.javaparser.ast.NodeList; import com.github.javaparser.ast.body.*; +import com.github.javaparser.ast.expr.BooleanLiteralExpr; import com.github.javaparser.ast.expr.VariableDeclarationExpr; -import com.github.javaparser.ast.key.*; +import com.github.javaparser.ast.jml.doc.*; +import com.github.javaparser.ast.jml.stmt.JmlExpressionStmt; +import com.github.javaparser.ast.jml.stmt.JmlExpressionStmt.JmlStmtKind; +import com.github.javaparser.ast.key.KeyMergePointStmt; import com.github.javaparser.ast.nodeTypes.NodeWithBody; import com.github.javaparser.ast.nodeTypes.NodeWithModifiers; import com.github.javaparser.ast.nodeTypes.NodeWithOptionalBlockStmt; @@ -59,7 +66,7 @@ /// {@link MethodDeclaration}, or {@link BlockStmt}, {@link FieldDeclaration} and /// {@link MethodDeclaration} were introduced for ghost and model declarations, /// JML statements (assume, assert, ...) are inserted into the bodies using -/// {@link KeYMarkerStatement}. +/// {@link JmlExpressionStmt}. /// /// You can access attached JML information using the {@link DataKey} in /// [JMLTransformer#KEY_SPEC_CASE], @@ -230,11 +237,12 @@ public JMLTransformer(TransformationPipelineServices services) { private Statement transformAssertStatement(TextualJMLAssertStatement stat) { KeyAst.Expression ctx = stat.getContext(); org.key_project.util.parsing.Position pos = ctx.getStartLocation().getPosition(); - int kind = switch (stat.getKind()) { - case ASSERT -> KIND_ASSERT; - case ASSUME -> KIND_ASSUME; + var kind = switch (stat.getKind()) { + case ASSERT -> JmlStmtKind.ASSERT; + case ASSUME -> JmlStmtKind.ASSUME; }; - KeYMarkerStatement stmt = new KeYMarkerStatement(kind); + JmlExpressionStmt stmt = + new JmlExpressionStmt(new NodeList<>(), kind, new BooleanLiteralExpr(true)); stmt.setData(KEY_ASSERT, stat); return stmt; } @@ -242,14 +250,15 @@ private Statement transformAssertStatement(TextualJMLAssertStatement stat) { private Statement transformSetStatement(TextualJMLSetStatement stat) { KeyAst.SetStatementContext ctx = new KeyAst.SetStatementContext(stat.getAssignment()); // org.key_project.util.parsing.Position pos = ctx.getStartLocation().getPosition(); - KeYMarkerStatement stmt = new KeYMarkerStatement(KIND_SET); + JmlExpressionStmt stmt = + new JmlExpressionStmt(new NodeList<>(), JmlStmtKind.SET, new BooleanLiteralExpr(true)); // TODO simulate/ copy token range. stmt.setData(KEY_ASSIGN, ctx); return stmt; } - private KeYMarkerStatement transformMergePointDecl(TextualJMLMergePointDecl stat) { - KeYMarkerStatement mps = new KeYMarkerStatement(KIND_MERGE_POINT); + private KeyMergePointStmt transformMergePointDecl(TextualJMLMergePointDecl stat) { + KeyMergePointStmt mps = new KeyMergePointStmt(new BooleanLiteralExpr(true)); mps.setData(KEY_MERGE_POINT, stat); return mps; } @@ -274,8 +283,8 @@ private void transformClassLevelComments(TypeDeclaration td) throws SLTransla for (BodyDeclaration member : members) { // JMLDocsBodyDeclaration: JML comments inside a class/interface/... body - if (member instanceof JmlDocsBodyDeclaration bd) { - String concatenatedComment = sanitizer.asString(bd.jmlDocs()); + if (member instanceof JmlDocDeclaration bd) { + String concatenatedComment = sanitizer.asString(bd.getJmlComments()); // The preparser split along the grammar rules in KeYParser.g4, and gives you a list // of JML entities. @@ -402,7 +411,7 @@ private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName) while (stmt instanceof LabeledStmt labeledStmt) { var inner = labeledStmt.getStatement(); - if (inner instanceof JmlDocsStatements) { + if (inner instanceof JmlDocStmt) { throw new SLTranslationException( ("Here is something wrong. Your label '%s' is glued to a " + "JML annotation instead of a Java statement. Please consider the use of braces") @@ -429,8 +438,8 @@ private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName) } } else if (stmt instanceof NodeWithBody b && b.getBody().isBlockStmt()) { transformMethodLevelCommentsAt(b.getBody().asBlockStmt(), fileName); - } else if (stmt instanceof JmlDocsStatements doc) { - String concat = sanitizer.asString(doc.getJmlDocs()); + } else if (stmt instanceof JmlDocStmt doc) { + String concat = sanitizer.asString(doc.getJmlComments()); ImmutableList constructs = io.parseMethodLevel(concat, fileName, pos); services.addWarnings(io.getWarnings()); @@ -513,10 +522,10 @@ public void apply(@NonNull CompilationUnit cu) { final var types = new ArrayList<>(cu.getTypes()); ImmutableList modifiers = null; for (TypeDeclaration td : types) { - if (td instanceof JmlDocsTypeDeclaration jdtd) { + if (td instanceof JmlDocType jdtd) { // Currently, we only support modifier at type declaration level. // Other things would be ghost classes or model imports. - var input = sanitizer.asString(jdtd.jmlDocs()); + var input = sanitizer.asString(jdtd.getJmlComments()); PreParser pp = TransformationPipelineServices.getPreParser(); modifiers = pp.parseModifiers(input); } else { @@ -555,7 +564,7 @@ private void transformModifiers(NodeWithModifiers hasMods) { for (Modifier mod : hasMods.getModifiers()) { var kw = mod.getKeyword(); if (kw instanceof JmlDocModifier jdm) { - var modifiers = sanitizer.asString(jdm.getJmlDocs()); + var modifiers = sanitizer.asString(jdm.getJmlComments()); var jmlMods = pp.parseModifiers(modifiers); for (var jmlMod : jmlMods) { hasMods.addModifier(jmlMod.getParserKeyword()); @@ -607,7 +616,10 @@ public String asString(Collection jmlDocs, boolean emulateGlobalPosition) } public String asString(NodeList jmlDocs, boolean emulateGlobalPosition) { - return asStringJT(jmlDocs.stream().map(JmlDoc::getContent).toList(), emulateGlobalPosition); + final var tokenList = jmlDocs.stream().map(JmlDoc::getTokenRange) + .map(it -> it.get().getBegin()) + .toList(); + return asStringJT(tokenList, emulateGlobalPosition); } public String toSanitizedString(StringBuilder s) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java index d862d1d42a1..1536ce2c28f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java @@ -5,10 +5,7 @@ import com.github.javaparser.ast.CompilationUnit; import com.github.javaparser.ast.Modifier; -import com.github.javaparser.ast.key.JmlDocModifier; -import com.github.javaparser.ast.key.JmlDocsBodyDeclaration; -import com.github.javaparser.ast.key.JmlDocsStatements; -import com.github.javaparser.ast.key.JmlDocsTypeDeclaration; +import com.github.javaparser.ast.jml.doc.*; import org.jspecify.annotations.NonNull; /** @@ -30,9 +27,9 @@ public void apply(CompilationUnit cu) { } } - if (it instanceof JmlDocsStatements || - it instanceof JmlDocsTypeDeclaration || - it instanceof JmlDocsBodyDeclaration) { + if (it instanceof JmlDocStmt || + it instanceof JmlDocType || + it instanceof JmlDocDeclaration) { it.remove(); } }); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/RecordClassBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/RecordClassBuilder.java index a0d4170b24b..26ae74849d8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/RecordClassBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/RecordClassBuilder.java @@ -13,7 +13,7 @@ import com.github.javaparser.ast.NodeList; import com.github.javaparser.ast.body.*; import com.github.javaparser.ast.expr.*; -import com.github.javaparser.ast.key.JmlDocModifier; +import com.github.javaparser.ast.jml.doc.JmlDocModifier; import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName; import com.github.javaparser.ast.stmt.ReturnStmt; import com.github.javaparser.ast.type.PrimitiveType; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java index c06b12508eb..3b048b6c52c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java @@ -39,7 +39,7 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; -import com.github.javaparser.ast.key.KeyTransactionStatement; +import com.github.javaparser.ast.key.KeyTransactionStmt; import org.jspecify.annotations.Nullable; import static de.uka.ilkd.key.java.ast.expression.BinaryAssignment.BinaryAssignmentKind.COPY; @@ -923,19 +923,19 @@ protected JavaBlock buildJavaBlock(ImmutableList formalParVars sb2 = new StatementBlock(transaction ? new Statement[] { new TransactionStatement( - KeyTransactionStatement.TransactionType.BEGIN), + KeyTransactionStmt.TransactionType.BEGIN), nullStat, tryStat, new TransactionStatement( - KeyTransactionStatement.TransactionType.FINISH) } + KeyTransactionStmt.TransactionType.FINISH) } : new Statement[] { nullStat, tryStat }); } else { sb2 = new StatementBlock(transaction ? new Statement[] { new TransactionStatement( - KeyTransactionStatement.TransactionType.BEGIN), + KeyTransactionStmt.TransactionType.BEGIN), nullStat, beforeTry, tryStat, new TransactionStatement( - KeyTransactionStatement.TransactionType.FINISH) } + KeyTransactionStmt.TransactionType.FINISH) } : new Statement[] { nullStat, beforeTry, tryStat }); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java index ae5b3f0f1df..ca9deb09038 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java @@ -52,7 +52,7 @@ import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.*; -import com.github.javaparser.ast.key.KeyTransactionStatement; +import com.github.javaparser.ast.key.KeyTransactionStmt; import org.jspecify.annotations.NonNull; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; @@ -1585,7 +1585,7 @@ private StatementBlock finishTransactionIfModalityIsTransactional( final Statement statement) { if (instantiation.isTransactional()) { return new StatementBlock(statement, - new TransactionStatement(KeyTransactionStatement.TransactionType.FINISH)); + new TransactionStatement(KeyTransactionStmt.TransactionType.FINISH)); } else { if (statement instanceof StatementBlock) { return (StatementBlock) statement; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java index 2a1f35ab326..12ce83e4734 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java @@ -37,7 +37,7 @@ import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; -import com.github.javaparser.ast.key.KeyTransactionStatement; +import com.github.javaparser.ast.key.KeyTransactionStmt; public final class WhileInvariantTransformer { /** the outer label that is used to leave the while loop ('l1') */ @@ -223,7 +223,7 @@ public JTerm transform(TermLabelState termLabelState, Rule rule, JavaBlock mainJavaBlock = JavaBlock.createJavaBlock(transaction ? new StatementBlock(resSta, new TransactionStatement( - KeyTransactionStatement.TransactionType.FINISH)) + KeyTransactionStmt.TransactionType.FINISH)) : new StatementBlock(resSta)); return services.getTermBuilder().prog(loopBodyModalityKind, mainJavaBlock, result, computeLoopBodyModalityLabels(termLabelState, services, applicationPos, rule, ruleApp, diff --git a/key.core/src/main/javacc/de/uka/ilkd/key/parser/proofjava/ProofJavaParser.jj b/key.core/src/main/javacc/de/uka/ilkd/key/parser/proofjava/ProofJavaParser.jj index 51d8692200f..18c7365e644 100644 --- a/key.core/src/main/javacc/de/uka/ilkd/key/parser/proofjava/ProofJavaParser.jj +++ b/key.core/src/main/javacc/de/uka/ilkd/key/parser/proofjava/ProofJavaParser.jj @@ -3729,7 +3729,7 @@ Statement Statement() : | result = LoopScope() | result = TryStatement() | result = AssertStatement() -| result = KeYCatchAllStatement() +| result = KeyCatchAllStmt() | result = ExecStatement() ) { @@ -3739,7 +3739,7 @@ Statement Statement() : } } -Statement KeYCatchAllStatement() : +Statement KeyCatchAllStmt() : { Statement result; UncollatedReferenceQualifier qn;