From 74aa438be18804903644ca6c5cc3bfd772e62a80 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 15 Aug 2026 23:21:14 +0200 Subject: [PATCH 1/2] Migrate to JMLtk --- build.gradle | 2 +- gradle/libs.versions.toml | 8 +-- .../ast/statement/TransactionStatement.java | 14 +++--- .../ilkd/key/java/loader/JP2KeYConverter.java | 48 ++++++++---------- .../ConstantExpressionEvaluator.java | 12 ++--- .../ConstantStringExpressionEvaluator.java | 34 +++++-------- .../pipeline/JMLTransformer.java | 50 ++++++++++++------- .../pipeline/JmlDocRemoval.java | 11 ++-- .../pipeline/RecordClassBuilder.java | 2 +- .../key/proof/init/AbstractOperationPO.java | 10 ++-- .../key/rule/AuxiliaryContractBuilders.java | 4 +- .../WhileInvariantTransformer.java | 4 +- .../key/parser/proofjava/ProofJavaParser.jj | 4 +- 13 files changed, 97 insertions(+), 106 deletions(-) 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; From 8c05d88446c11c5a337553c96218579db7d213d2 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 16 Aug 2026 14:02:03 +0200 Subject: [PATCH 2/2] update KeYJavaPipelineTest --- .../08_ImplicitFieldAdder/MostSimpleInner.java | 8 ++++---- .../MostSimpleInner.java | 8 ++++---- .../MostSimpleInner.java | 8 ++++---- .../MostSimpleInner.java | 8 ++++---- .../MostSimpleInner.java | 8 ++++---- .../13_PrepareObjectBuilder/MostSimpleInner.java | 8 ++++---- .../expected/14_CreateBuilder/MostSimpleInner.java | 8 ++++---- .../15_CreateObjectBuilder/MostSimpleInner.java | 8 ++++---- .../16_LocalClassTransformation/MostSimpleInner.java | 8 ++++---- .../MostSimpleInner.java | 8 ++++---- .../01_TextblockTransformer/RecordOverwriting.java | 3 +++ .../01_TextblockTransformer/SimpleRecord.java | 2 +- .../02_MultiCatchReducer/RecordOverwriting.java | 3 +++ .../expected/02_MultiCatchReducer/SimpleRecord.java | 2 +- .../03_TryWithResourceReducer/RecordOverwriting.java | 3 +++ .../03_TryWithResourceReducer/SimpleRecord.java | 2 +- .../04_EnumClassBuilder/RecordOverwriting.java | 3 +++ .../expected/04_EnumClassBuilder/SimpleRecord.java | 2 +- .../05_RecordClassBuilder/CompactConstructor.java | 2 +- .../expected/05_RecordClassBuilder/InnerRecord.java | 2 +- .../expected/05_RecordClassBuilder/NotAllowed.java | 4 ++-- .../expected/05_RecordClassBuilder/Point3d.java | 2 +- .../05_RecordClassBuilder/RecordOverwriting.java | 5 ++++- .../expected/05_RecordClassBuilder/SimpleRecord.java | 6 +++--- .../06_JMLTransformer/CompactConstructor.java | 2 +- .../expected/06_JMLTransformer/InnerRecord.java | 2 +- .../expected/06_JMLTransformer/NotAllowed.java | 4 ++-- .../records/expected/06_JMLTransformer/Point3d.java | 2 +- .../06_JMLTransformer/RecordOverwriting.java | 7 +++++-- .../expected/06_JMLTransformer/SimpleRecord.java | 6 +++--- .../07_JmlDocRemoval/CompactConstructor.java | 2 +- .../expected/07_JmlDocRemoval/InnerRecord.java | 2 +- .../expected/07_JmlDocRemoval/NotAllowed.java | 4 ++-- .../records/expected/07_JmlDocRemoval/Point3d.java | 2 +- .../expected/07_JmlDocRemoval/RecordOverwriting.java | 4 ++-- .../expected/07_JmlDocRemoval/SimpleRecord.java | 6 +++--- .../08_ImplicitFieldAdder/CompactConstructor.java | 6 +++--- .../expected/08_ImplicitFieldAdder/InnerRecord.java | 10 +++++----- .../expected/08_ImplicitFieldAdder/NotAllowed.java | 12 ++++++------ .../expected/08_ImplicitFieldAdder/Point3d.java | 6 +++--- .../08_ImplicitFieldAdder/RecordOverwriting.java | 8 ++++---- .../expected/08_ImplicitFieldAdder/SimpleRecord.java | 10 +++++----- .../CompactConstructor.java | 6 +++--- .../InnerRecord.java | 10 +++++----- .../NotAllowed.java | 12 ++++++------ .../09_InstanceAllocationMethodBuilder/Point3d.java | 6 +++--- .../RecordOverwriting.java | 8 ++++---- .../SimpleRecord.java | 10 +++++----- .../CompactConstructor.java | 6 +++--- .../10_ConstructorNormalformBuilder/InnerRecord.java | 10 +++++----- .../10_ConstructorNormalformBuilder/NotAllowed.java | 12 ++++++------ .../10_ConstructorNormalformBuilder/Point3d.java | 6 +++--- .../RecordOverwriting.java | 8 ++++---- .../SimpleRecord.java | 10 +++++----- .../CompactConstructor.java | 6 +++--- .../InnerRecord.java | 10 +++++----- .../11_ClassPreparationMethodBuilder/NotAllowed.java | 12 ++++++------ .../11_ClassPreparationMethodBuilder/Point3d.java | 6 +++--- .../RecordOverwriting.java | 8 ++++---- .../SimpleRecord.java | 10 +++++----- .../CompactConstructor.java | 6 +++--- .../12_ClassInitializeMethodBuilder/InnerRecord.java | 10 +++++----- .../12_ClassInitializeMethodBuilder/NotAllowed.java | 12 ++++++------ .../12_ClassInitializeMethodBuilder/Point3d.java | 6 +++--- .../RecordOverwriting.java | 8 ++++---- .../SimpleRecord.java | 10 +++++----- .../13_PrepareObjectBuilder/CompactConstructor.java | 6 +++--- .../13_PrepareObjectBuilder/InnerRecord.java | 10 +++++----- .../expected/13_PrepareObjectBuilder/NotAllowed.java | 12 ++++++------ .../expected/13_PrepareObjectBuilder/Point3d.java | 6 +++--- .../13_PrepareObjectBuilder/RecordOverwriting.java | 8 ++++---- .../13_PrepareObjectBuilder/SimpleRecord.java | 10 +++++----- .../14_CreateBuilder/CompactConstructor.java | 6 +++--- .../expected/14_CreateBuilder/InnerRecord.java | 10 +++++----- .../expected/14_CreateBuilder/NotAllowed.java | 12 ++++++------ .../records/expected/14_CreateBuilder/Point3d.java | 6 +++--- .../expected/14_CreateBuilder/RecordOverwriting.java | 8 ++++---- .../expected/14_CreateBuilder/SimpleRecord.java | 10 +++++----- .../15_CreateObjectBuilder/CompactConstructor.java | 6 +++--- .../expected/15_CreateObjectBuilder/InnerRecord.java | 10 +++++----- .../expected/15_CreateObjectBuilder/NotAllowed.java | 12 ++++++------ .../expected/15_CreateObjectBuilder/Point3d.java | 6 +++--- .../15_CreateObjectBuilder/RecordOverwriting.java | 8 ++++---- .../15_CreateObjectBuilder/SimpleRecord.java | 10 +++++----- .../CompactConstructor.java | 6 +++--- .../16_LocalClassTransformation/InnerRecord.java | 10 +++++----- .../16_LocalClassTransformation/NotAllowed.java | 12 ++++++------ .../16_LocalClassTransformation/Point3d.java | 6 +++--- .../RecordOverwriting.java | 8 ++++---- .../16_LocalClassTransformation/SimpleRecord.java | 10 +++++----- .../CompactConstructor.java | 6 +++--- .../InnerRecord.java | 10 +++++----- .../NotAllowed.java | 12 ++++++------ .../Point3d.java | 6 +++--- .../RecordOverwriting.java | 8 ++++---- .../SimpleRecord.java | 10 +++++----- .../simple/expected/08_ImplicitFieldAdder/Test.java | 8 ++++---- .../09_InstanceAllocationMethodBuilder/Test.java | 8 ++++---- .../10_ConstructorNormalformBuilder/Test.java | 8 ++++---- .../11_ClassPreparationMethodBuilder/Test.java | 8 ++++---- .../12_ClassInitializeMethodBuilder/Test.java | 8 ++++---- .../expected/13_PrepareObjectBuilder/Test.java | 8 ++++---- .../simple/expected/14_CreateBuilder/Test.java | 8 ++++---- .../simple/expected/15_CreateObjectBuilder/Test.java | 8 ++++---- .../expected/16_LocalClassTransformation/Test.java | 8 ++++---- .../17_ConstantStringExpressionEvaluator/Test.java | 8 ++++---- 106 files changed, 391 insertions(+), 373 deletions(-) diff --git a/key.core/pipelineTests/innerclass/expected/08_ImplicitFieldAdder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/08_ImplicitFieldAdder/MostSimpleInner.java index ae893d9a18f..554c70ab546 100644 --- a/key.core/pipelineTests/innerclass/expected/08_ImplicitFieldAdder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/08_ImplicitFieldAdder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } @javax.annotation.processing.Generated() @@ -34,8 +34,8 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/innerclass/expected/09_InstanceAllocationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/09_InstanceAllocationMethodBuilder/MostSimpleInner.java index cbb206f2577..60260e6c205 100644 --- a/key.core/pipelineTests/innerclass/expected/09_InstanceAllocationMethodBuilder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/09_InstanceAllocationMethodBuilder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); } @@ -36,10 +36,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); } diff --git a/key.core/pipelineTests/innerclass/expected/10_ConstructorNormalformBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/10_ConstructorNormalformBuilder/MostSimpleInner.java index 59fd6e1b318..6c9b7a5d148 100644 --- a/key.core/pipelineTests/innerclass/expected/10_ConstructorNormalformBuilder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/10_ConstructorNormalformBuilder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -44,10 +44,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/innerclass/expected/11_ClassPreparationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/11_ClassPreparationMethodBuilder/MostSimpleInner.java index 803b9be00b4..f09f2a65d25 100644 --- a/key.core/pipelineTests/innerclass/expected/11_ClassPreparationMethodBuilder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/11_ClassPreparationMethodBuilder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -47,10 +47,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/innerclass/expected/12_ClassInitializeMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/12_ClassInitializeMethodBuilder/MostSimpleInner.java index 3c160373169..e451315c5ed 100644 --- a/key.core/pipelineTests/innerclass/expected/12_ClassInitializeMethodBuilder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/12_ClassInitializeMethodBuilder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -85,10 +85,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/innerclass/expected/13_PrepareObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/13_PrepareObjectBuilder/MostSimpleInner.java index b4d0f07a148..4a5ce55b4da 100644 --- a/key.core/pipelineTests/innerclass/expected/13_PrepareObjectBuilder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/13_PrepareObjectBuilder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -93,10 +93,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/innerclass/expected/14_CreateBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/14_CreateBuilder/MostSimpleInner.java index 3bc13f1ae18..21c82daa31e 100644 --- a/key.core/pipelineTests/innerclass/expected/14_CreateBuilder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/14_CreateBuilder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -100,10 +100,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/innerclass/expected/15_CreateObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/15_CreateObjectBuilder/MostSimpleInner.java index decd2bad906..b76178daf4f 100644 --- a/key.core/pipelineTests/innerclass/expected/15_CreateObjectBuilder/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/15_CreateObjectBuilder/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -108,10 +108,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/innerclass/expected/16_LocalClassTransformation/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/16_LocalClassTransformation/MostSimpleInner.java index decd2bad906..b76178daf4f 100644 --- a/key.core/pipelineTests/innerclass/expected/16_LocalClassTransformation/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/16_LocalClassTransformation/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -108,10 +108,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/innerclass/expected/17_ConstantStringExpressionEvaluator/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/17_ConstantStringExpressionEvaluator/MostSimpleInner.java index decd2bad906..b76178daf4f 100644 --- a/key.core/pipelineTests/innerclass/expected/17_ConstantStringExpressionEvaluator/MostSimpleInner.java +++ b/key.core/pipelineTests/innerclass/expected/17_ConstantStringExpressionEvaluator/MostSimpleInner.java @@ -15,10 +15,10 @@ public static class MyInnerClass { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyInnerClass $allocate(); @@ -108,10 +108,10 @@ public MyInnerClass() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MostSimpleInner $allocate(); diff --git a/key.core/pipelineTests/records/expected/01_TextblockTransformer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/01_TextblockTransformer/RecordOverwriting.java index 4cffbb21982..cbd1115be65 100644 --- a/key.core/pipelineTests/records/expected/01_TextblockTransformer/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/01_TextblockTransformer/RecordOverwriting.java @@ -1,3 +1,6 @@ +//@ /*@ nullable */ + + record MyRecord(String test) { public int hashCode() { diff --git a/key.core/pipelineTests/records/expected/01_TextblockTransformer/SimpleRecord.java b/key.core/pipelineTests/records/expected/01_TextblockTransformer/SimpleRecord.java index 72c63026dad..d0970ab50a9 100644 --- a/key.core/pipelineTests/records/expected/01_TextblockTransformer/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/01_TextblockTransformer/SimpleRecord.java @@ -1,4 +1,4 @@ -public record SimpleRecord(/*@ nullable */ String name) implements Serializable { +public record SimpleRecord([[JML modifiers]] String name) implements Serializable { SimpleRecord(String name) { this.name = name; diff --git a/key.core/pipelineTests/records/expected/02_MultiCatchReducer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/RecordOverwriting.java index 4cffbb21982..cbd1115be65 100644 --- a/key.core/pipelineTests/records/expected/02_MultiCatchReducer/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/RecordOverwriting.java @@ -1,3 +1,6 @@ +//@ /*@ nullable */ + + record MyRecord(String test) { public int hashCode() { diff --git a/key.core/pipelineTests/records/expected/02_MultiCatchReducer/SimpleRecord.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/SimpleRecord.java index 72c63026dad..d0970ab50a9 100644 --- a/key.core/pipelineTests/records/expected/02_MultiCatchReducer/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/SimpleRecord.java @@ -1,4 +1,4 @@ -public record SimpleRecord(/*@ nullable */ String name) implements Serializable { +public record SimpleRecord([[JML modifiers]] String name) implements Serializable { SimpleRecord(String name) { this.name = name; diff --git a/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java index 4cffbb21982..cbd1115be65 100644 --- a/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java @@ -1,3 +1,6 @@ +//@ /*@ nullable */ + + record MyRecord(String test) { public int hashCode() { diff --git a/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java index 72c63026dad..d0970ab50a9 100644 --- a/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java @@ -1,4 +1,4 @@ -public record SimpleRecord(/*@ nullable */ String name) implements Serializable { +public record SimpleRecord([[JML modifiers]] String name) implements Serializable { SimpleRecord(String name) { this.name = name; diff --git a/key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java index 4cffbb21982..cbd1115be65 100644 --- a/key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java @@ -1,3 +1,6 @@ +//@ /*@ nullable */ + + record MyRecord(String test) { public int hashCode() { diff --git a/key.core/pipelineTests/records/expected/04_EnumClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/SimpleRecord.java index 72c63026dad..d0970ab50a9 100644 --- a/key.core/pipelineTests/records/expected/04_EnumClassBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/SimpleRecord.java @@ -1,4 +1,4 @@ -public record SimpleRecord(/*@ nullable */ String name) implements Serializable { +public record SimpleRecord([[JML modifiers]] String name) implements Serializable { SimpleRecord(String name) { this.name = name; diff --git a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/CompactConstructor.java index e025ccf3c9c..5f4fe148221 100644 --- a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } } diff --git a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/InnerRecord.java index 6a0f18a5713..15fb4b9cc41 100644 --- a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } } diff --git a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/NotAllowed.java index e24980575b0..974a13188c5 100644 --- a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -121,7 +121,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } diff --git a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/Point3d.java index 57ca946054a..d4cfbbfe592 100644 --- a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } } diff --git a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/RecordOverwriting.java index 3855634abfb..2e86e75d89a 100644 --- a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/RecordOverwriting.java @@ -1,3 +1,6 @@ +//@ /*@ nullable */ + + @javax.annotation.processing.Generated("RecordClassBuilder") final class MyRecord extends Record { @@ -18,7 +21,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } diff --git a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/SimpleRecord.java index 8ca64b04d48..a4fee4a1ceb 100644 --- a/key.core/pipelineTests/records/expected/05_RecordClassBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final /*@ nullable */ String name; + private final [[JML modifiers]] String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final /*@ nullable */ String name() { + public final [[JML modifiers]] String name() { return name; } @@ -43,7 +43,7 @@ public final class SimpleRecord extends Record { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } diff --git a/key.core/pipelineTests/records/expected/06_JMLTransformer/CompactConstructor.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/CompactConstructor.java index e025ccf3c9c..5f4fe148221 100644 --- a/key.core/pipelineTests/records/expected/06_JMLTransformer/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/06_JMLTransformer/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } } diff --git a/key.core/pipelineTests/records/expected/06_JMLTransformer/InnerRecord.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/InnerRecord.java index 6a0f18a5713..15fb4b9cc41 100644 --- a/key.core/pipelineTests/records/expected/06_JMLTransformer/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/06_JMLTransformer/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } } diff --git a/key.core/pipelineTests/records/expected/06_JMLTransformer/NotAllowed.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/NotAllowed.java index e24980575b0..974a13188c5 100644 --- a/key.core/pipelineTests/records/expected/06_JMLTransformer/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/06_JMLTransformer/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -121,7 +121,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } diff --git a/key.core/pipelineTests/records/expected/06_JMLTransformer/Point3d.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/Point3d.java index 57ca946054a..d4cfbbfe592 100644 --- a/key.core/pipelineTests/records/expected/06_JMLTransformer/Point3d.java +++ b/key.core/pipelineTests/records/expected/06_JMLTransformer/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } } diff --git a/key.core/pipelineTests/records/expected/06_JMLTransformer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/RecordOverwriting.java index 3855634abfb..e79f5471037 100644 --- a/key.core/pipelineTests/records/expected/06_JMLTransformer/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/06_JMLTransformer/RecordOverwriting.java @@ -1,5 +1,8 @@ +//@ /*@ nullable */ + + @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +21,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } diff --git a/key.core/pipelineTests/records/expected/06_JMLTransformer/SimpleRecord.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/SimpleRecord.java index 96b71909246..41b38a917d2 100644 --- a/key.core/pipelineTests/records/expected/06_JMLTransformer/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/06_JMLTransformer/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final /*@ nullable */ nullable String name; + private final [[JML modifiers]] /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final /*@ nullable */ nullable String name() { + public final [[JML modifiers]] /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final class SimpleRecord extends Record { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } diff --git a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/CompactConstructor.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/CompactConstructor.java index e025ccf3c9c..5f4fe148221 100644 --- a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } } diff --git a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/InnerRecord.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/InnerRecord.java index 6a0f18a5713..15fb4b9cc41 100644 --- a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } } diff --git a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/NotAllowed.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/NotAllowed.java index e24980575b0..974a13188c5 100644 --- a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -121,7 +121,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } diff --git a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/Point3d.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/Point3d.java index 57ca946054a..d4cfbbfe592 100644 --- a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/Point3d.java +++ b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } } diff --git a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/RecordOverwriting.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/RecordOverwriting.java index 3855634abfb..a4de3343ad3 100644 --- a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } diff --git a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/SimpleRecord.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/SimpleRecord.java index 078bdc6b68f..2016d3bd31f 100644 --- a/key.core/pipelineTests/records/expected/07_JmlDocRemoval/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } diff --git a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/CompactConstructor.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/CompactConstructor.java index e1c3a521c88..3b3a2040abf 100644 --- a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,8 +77,8 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/InnerRecord.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/InnerRecord.java index 68cc41744d9..8629edbb95a 100644 --- a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } @javax.annotation.processing.Generated() @@ -87,8 +87,8 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/NotAllowed.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/NotAllowed.java index 230306fea93..7aae9a39f58 100644 --- a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } @javax.annotation.processing.Generated("RecordClassBuilder") @@ -139,7 +139,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -179,8 +179,8 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/Point3d.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/Point3d.java index b9493890596..fedc1fdb8d7 100644 --- a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/Point3d.java +++ b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,8 +82,8 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/RecordOverwriting.java index f9a587af522..30dcf85d51d 100644 --- a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,8 +47,8 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/SimpleRecord.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/SimpleRecord.java index 1a3aba6eea0..14a88f2ea5c 100644 --- a/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,8 +70,8 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/CompactConstructor.java index fc186802964..eaba09b590d 100644 --- a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); } diff --git a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/InnerRecord.java index 7524ddc0c99..f5a0d78fdfc 100644 --- a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); } @@ -89,10 +89,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); } diff --git a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/NotAllowed.java index 5b781dbc564..6f05e108012 100644 --- a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -142,7 +142,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -182,10 +182,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); } diff --git a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/Point3d.java index eebbf0b31eb..aeca44382e2 100644 --- a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); } diff --git a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/RecordOverwriting.java index 19dfabeaeda..e20e57ac3fd 100644 --- a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); } diff --git a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/SimpleRecord.java index 2770c420e89..5c79f7cc92d 100644 --- a/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); } diff --git a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/CompactConstructor.java index fc92bececca..43a9b578110 100644 --- a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/InnerRecord.java index d57bd0f3df1..7db7dbe5588 100644 --- a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -96,10 +96,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/NotAllowed.java index 6e8d125d2e5..e646eeb5a5e 100644 --- a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -152,7 +152,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -192,10 +192,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/Point3d.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/Point3d.java index 877b658f071..1ca24eedba9 100644 --- a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/RecordOverwriting.java index c7ef795a98f..a88d0fe9d70 100644 --- a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/SimpleRecord.java index c1b6d559752..e0f2755dc3c 100644 --- a/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/CompactConstructor.java index 8680706dd0d..14035dd5250 100644 --- a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/InnerRecord.java index 5343de77652..4eab3862a88 100644 --- a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -99,10 +99,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/NotAllowed.java index 4a627f614e6..0ddc6a52fa7 100644 --- a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -155,7 +155,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -195,10 +195,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/Point3d.java index 405663186f2..947aa529bf4 100644 --- a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/RecordOverwriting.java index 78bcc964375..7808ea1b0a1 100644 --- a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/SimpleRecord.java index ec029a6c470..d445c2eb087 100644 --- a/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/CompactConstructor.java index 2b52b0658dc..65f394e00c7 100644 --- a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/InnerRecord.java index 0bb91a8b64b..bc45f7a231b 100644 --- a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -137,10 +137,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/NotAllowed.java index 7c2de807880..ddfd92c6c17 100644 --- a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -193,7 +193,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -233,10 +233,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/Point3d.java index 8de6841caac..dcd93138c1c 100644 --- a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/RecordOverwriting.java index 650d3b99e37..568b168d97f 100644 --- a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/SimpleRecord.java index a1dc322b51e..05b486fa021 100644 --- a/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/CompactConstructor.java index 389f48ba02a..49ad810f7a6 100644 --- a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/InnerRecord.java index 77e2f1b4f50..921deac226c 100644 --- a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -153,10 +153,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/NotAllowed.java index ed66ca9b67f..2d11f8db3e0 100644 --- a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -205,7 +205,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -245,10 +245,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/Point3d.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/Point3d.java index 2c47de74cd1..eeb13750dd7 100644 --- a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/RecordOverwriting.java index 18d7410da06..f98da7fac80 100644 --- a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/SimpleRecord.java index ad16913d9b6..ab7592cdeb3 100644 --- a/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/14_CreateBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/CompactConstructor.java index efa6174b66d..eaff10914b0 100644 --- a/key.core/pipelineTests/records/expected/14_CreateBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/14_CreateBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/14_CreateBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/InnerRecord.java index 486d8e8e159..628b08d9208 100644 --- a/key.core/pipelineTests/records/expected/14_CreateBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/14_CreateBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -160,10 +160,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/14_CreateBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/NotAllowed.java index ae03a6dc1ef..80193c46df5 100644 --- a/key.core/pipelineTests/records/expected/14_CreateBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/14_CreateBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -212,7 +212,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -252,10 +252,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/14_CreateBuilder/Point3d.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/Point3d.java index 80ae7db375e..3bae7485005 100644 --- a/key.core/pipelineTests/records/expected/14_CreateBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/14_CreateBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/14_CreateBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/RecordOverwriting.java index 288403e2c81..59fcc92463a 100644 --- a/key.core/pipelineTests/records/expected/14_CreateBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/14_CreateBuilder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/14_CreateBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/SimpleRecord.java index cc2c86f7c10..cf3db5cd2ba 100644 --- a/key.core/pipelineTests/records/expected/14_CreateBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/14_CreateBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/CompactConstructor.java index 8cb5d45d4a2..689876ca042 100644 --- a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/InnerRecord.java index 673914b4299..4401928faa5 100644 --- a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -168,10 +168,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/NotAllowed.java index 25d4d0c36e5..9d8850fc066 100644 --- a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -224,7 +224,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -264,10 +264,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/Point3d.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/Point3d.java index 8e0ecc2a3f9..edcdb80e39c 100644 --- a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/Point3d.java +++ b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/RecordOverwriting.java index 7bf6853be18..38d5fe026e6 100644 --- a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/SimpleRecord.java index 02f77c47f31..249abb6c0bd 100644 --- a/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/CompactConstructor.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/CompactConstructor.java index 8cb5d45d4a2..689876ca042 100644 --- a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/InnerRecord.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/InnerRecord.java index 673914b4299..4401928faa5 100644 --- a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -168,10 +168,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/NotAllowed.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/NotAllowed.java index 25d4d0c36e5..9d8850fc066 100644 --- a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -224,7 +224,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -264,10 +264,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/Point3d.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/Point3d.java index 8e0ecc2a3f9..edcdb80e39c 100644 --- a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/Point3d.java +++ b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/RecordOverwriting.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/RecordOverwriting.java index 7bf6853be18..38d5fe026e6 100644 --- a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/SimpleRecord.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/SimpleRecord.java index 02f77c47f31..249abb6c0bd 100644 --- a/key.core/pipelineTests/records/expected/16_LocalClassTransformation/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/CompactConstructor.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/CompactConstructor.java index 8cb5d45d4a2..689876ca042 100644 --- a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/CompactConstructor.java +++ b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/CompactConstructor.java @@ -60,7 +60,7 @@ public Mapping(String from, String to) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Mapping[" + "from=" + from + "," + "to=" + to + "]"; } @@ -77,10 +77,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Mapping $allocate(); diff --git a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/InnerRecord.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/InnerRecord.java index 673914b4299..4401928faa5 100644 --- a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/InnerRecord.java +++ b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/InnerRecord.java @@ -49,7 +49,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -68,10 +68,10 @@ public final non_null String toString() { private OuterClass $enclosingThis; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); @@ -168,10 +168,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static OuterClass $allocate(); diff --git a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/NotAllowed.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/NotAllowed.java index 25d4d0c36e5..9d8850fc066 100644 --- a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/NotAllowed.java +++ b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/NotAllowed.java @@ -46,7 +46,7 @@ private Name(String name) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Name[" + "name=" + name + "]"; } @@ -78,10 +78,10 @@ static Name of(String name) { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static // package-private Name $allocate(); @@ -224,7 +224,7 @@ public final int y() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point[" + "x=" + x + "," + "y=" + y + "]"; } @@ -264,10 +264,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point $allocate(); diff --git a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/Point3d.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/Point3d.java index 8e0ecc2a3f9..edcdb80e39c 100644 --- a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/Point3d.java +++ b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/Point3d.java @@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]"; } @@ -82,10 +82,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Point3d $allocate(); diff --git a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/RecordOverwriting.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/RecordOverwriting.java index 7bf6853be18..38d5fe026e6 100644 --- a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/RecordOverwriting.java +++ b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/RecordOverwriting.java @@ -1,5 +1,5 @@ @javax.annotation.processing.Generated("RecordClassBuilder") -final class MyRecord extends Record { +final /*@ nullable */ class MyRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") private final String test; @@ -18,7 +18,7 @@ public MyRecord(String test) { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "MyRecord[" + "test=" + test + "]"; } @@ -47,10 +47,10 @@ public String test() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static MyRecord $allocate(); diff --git a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/SimpleRecord.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/SimpleRecord.java index 02f77c47f31..249abb6c0bd 100644 --- a/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/SimpleRecord.java +++ b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/SimpleRecord.java @@ -2,10 +2,10 @@ public final class SimpleRecord extends Record { @javax.annotation.processing.Generated("RecordClassBuilder") - private final nullable String name; + private final /*@ nullable */ String name; @javax.annotation.processing.Generated("RecordClassBuilder") - public final nullable String name() { + public final /*@ nullable */ String name() { return name; } @@ -43,7 +43,7 @@ public final nullable String name() { @Override() @javax.annotation.processing.Generated("RecordClassBuilder") - public final non_null String toString() { + public final /*@ non_null */ String toString() { return "SimpleRecord[" + "name=" + name + "]"; } @@ -70,10 +70,10 @@ public final non_null String toString() { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SimpleRecord $allocate(); diff --git a/key.core/pipelineTests/simple/expected/08_ImplicitFieldAdder/Test.java b/key.core/pipelineTests/simple/expected/08_ImplicitFieldAdder/Test.java index e3c9d609b0d..40ec6e2ec07 100644 --- a/key.core/pipelineTests/simple/expected/08_ImplicitFieldAdder/Test.java +++ b/key.core/pipelineTests/simple/expected/08_ImplicitFieldAdder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } public class SubClass extends Test { @@ -53,8 +53,8 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; } diff --git a/key.core/pipelineTests/simple/expected/09_InstanceAllocationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/09_InstanceAllocationMethodBuilder/Test.java index 939c13da9ba..47cea33c755 100644 --- a/key.core/pipelineTests/simple/expected/09_InstanceAllocationMethodBuilder/Test.java +++ b/key.core/pipelineTests/simple/expected/09_InstanceAllocationMethodBuilder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); } @@ -55,10 +55,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); } diff --git a/key.core/pipelineTests/simple/expected/10_ConstructorNormalformBuilder/Test.java b/key.core/pipelineTests/simple/expected/10_ConstructorNormalformBuilder/Test.java index 0fcacd6fef9..6522e5a960c 100644 --- a/key.core/pipelineTests/simple/expected/10_ConstructorNormalformBuilder/Test.java +++ b/key.core/pipelineTests/simple/expected/10_ConstructorNormalformBuilder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -73,10 +73,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); diff --git a/key.core/pipelineTests/simple/expected/11_ClassPreparationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/11_ClassPreparationMethodBuilder/Test.java index 825b89f91cf..a3093ef167e 100644 --- a/key.core/pipelineTests/simple/expected/11_ClassPreparationMethodBuilder/Test.java +++ b/key.core/pipelineTests/simple/expected/11_ClassPreparationMethodBuilder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -76,10 +76,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); diff --git a/key.core/pipelineTests/simple/expected/12_ClassInitializeMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/12_ClassInitializeMethodBuilder/Test.java index 5d8570e373a..b615ea4df4c 100644 --- a/key.core/pipelineTests/simple/expected/12_ClassInitializeMethodBuilder/Test.java +++ b/key.core/pipelineTests/simple/expected/12_ClassInitializeMethodBuilder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -118,10 +118,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); diff --git a/key.core/pipelineTests/simple/expected/13_PrepareObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/13_PrepareObjectBuilder/Test.java index 53a5436e9ab..30677e46253 100644 --- a/key.core/pipelineTests/simple/expected/13_PrepareObjectBuilder/Test.java +++ b/key.core/pipelineTests/simple/expected/13_PrepareObjectBuilder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -130,10 +130,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); diff --git a/key.core/pipelineTests/simple/expected/14_CreateBuilder/Test.java b/key.core/pipelineTests/simple/expected/14_CreateBuilder/Test.java index 0116b540187..f4c580884c8 100644 --- a/key.core/pipelineTests/simple/expected/14_CreateBuilder/Test.java +++ b/key.core/pipelineTests/simple/expected/14_CreateBuilder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -137,10 +137,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); diff --git a/key.core/pipelineTests/simple/expected/15_CreateObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/15_CreateObjectBuilder/Test.java index 44f496647fc..71ed30ece94 100644 --- a/key.core/pipelineTests/simple/expected/15_CreateObjectBuilder/Test.java +++ b/key.core/pipelineTests/simple/expected/15_CreateObjectBuilder/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -145,10 +145,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); diff --git a/key.core/pipelineTests/simple/expected/16_LocalClassTransformation/Test.java b/key.core/pipelineTests/simple/expected/16_LocalClassTransformation/Test.java index 44f496647fc..71ed30ece94 100644 --- a/key.core/pipelineTests/simple/expected/16_LocalClassTransformation/Test.java +++ b/key.core/pipelineTests/simple/expected/16_LocalClassTransformation/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -145,10 +145,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate(); diff --git a/key.core/pipelineTests/simple/expected/17_ConstantStringExpressionEvaluator/Test.java b/key.core/pipelineTests/simple/expected/17_ConstantStringExpressionEvaluator/Test.java index 44f496647fc..71ed30ece94 100644 --- a/key.core/pipelineTests/simple/expected/17_ConstantStringExpressionEvaluator/Test.java +++ b/key.core/pipelineTests/simple/expected/17_ConstantStringExpressionEvaluator/Test.java @@ -26,10 +26,10 @@ public class Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static Test $allocate(); @@ -145,10 +145,10 @@ public class SubClass extends Test { static private boolean $classPrepared; @javax.annotation.processing.Generated() - static public model boolean $staticInv; + static public /*@ model */ boolean $staticInv; @javax.annotation.processing.Generated() - static public model boolean $staticInv_free; + static public /*@ model */ boolean $staticInv_free; public static SubClass $allocate();