From 17b01799d28fee73d0ae2bf313039b954ebb539b Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 12 Jul 2026 14:21:14 +0200 Subject: [PATCH 1/7] Transformer and test case --- .../pipeline/TryWithResourceReducer.java | 183 ++++++++++++++++++ .../pipeline/TryWithResourceReducerTest.java | 35 ++++ 2 files changed, 218 insertions(+) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java create mode 100644 key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java new file mode 100644 index 00000000000..8a03873d5a4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java @@ -0,0 +1,183 @@ +package de.uka.ilkd.key.java.transformations.pipeline; + +import com.github.javaparser.ast.NodeList; +import com.github.javaparser.ast.body.Parameter; +import com.github.javaparser.ast.body.TypeDeclaration; +import com.github.javaparser.ast.body.VariableDeclarator; +import com.github.javaparser.ast.expr.*; +import com.github.javaparser.ast.stmt.*; +import com.github.javaparser.ast.type.ClassOrInterfaceType; +import com.github.javaparser.ast.visitor.ModifierVisitor; +import com.github.javaparser.ast.visitor.Visitable; + +import java.util.List; +import java.util.concurrent.atomic.AtomicInteger; + +/// Rewrites every try-with-resources statement into the equivalent nested +/// try/finally form that javac itself generates, i.e. for +/// ```java +/// try (Resource r = open()) { +/// body; +/// } +/// ``` +/// this produces: +/// ```java +/// try { +/// Resource r = open(); +/// Throwable primaryExc$1 = null; +/// try { +/// body; +/// } catch (Throwable t$1) { +/// primaryExc$1 = t$1; +/// throw t$1; +/// } finally { +/// if (r != null) { +/// if (primaryExc$1 != null) { +/// try { r.close(); } catch (Throwable suppressedExc$1) { +/// primaryExc$1.addSuppressed(suppressedExc$1); +/// } +/// } else { r.close(); } +/// } +/// } +/// } +/// ``` +/// Multiple resources are handled by nesting (last-declared resource closes first), +/// and any catch/finally clauses that were attached to the original try are kept +/// on an outer try that wraps the whole resource-management block, exactly as +/// javac does it. +/// @author weigl, Claude Sonnet +public class TryWithResourceReducer implements JavaTransformer { + private final AtomicInteger counter = new AtomicInteger(); + + @Override + public void apply(TypeDeclaration td) { + td.accept(new TryWithResourcesDesugarer(), null); + } + + public class TryWithResourcesDesugarer extends ModifierVisitor { + @Override + public Visitable visit(TryStmt n, Void arg) { + // Desugar nested try statements first (in body/catches/finally) before + // handling this one, so everything ends up fully expanded. + super.visit(n, arg); + + if (n.getResources().isEmpty()) { + return n; + } + + List resources = n.getResources(); + BlockStmt innerBody = desugarResources(resources, 0, n.getTryBlock().clone()); + + // If the original try had no catch/finally of its own, the resource + // management block *is* the whole replacement. + if (n.getCatchClauses().isEmpty() && n.getFinallyBlock().isEmpty()) { + return innerBody; + } + + // Otherwise wrap the resource-management block in a try that keeps the + // user's original catch clauses / finally block. + TryStmt outer = new TryStmt(); + outer.setTryBlock(innerBody); + outer.setCatchClauses(n.getCatchClauses()); + n.getFinallyBlock().ifPresent(outer::setFinallyBlock); + return outer; + } + + /** + * Recursively builds the resource-closing nest starting at resources.get(index), + * with `body` as the innermost block (the original try-block statements). + */ + private BlockStmt desugarResources(List resources, int index, BlockStmt body) { + BlockStmt result = new BlockStmt(); + + Expression resourceExpr = resources.get(index); + String resourceName; + + if (resourceExpr instanceof VariableDeclarationExpr) { + // try (Resource r = new Resource()) { ... } + VariableDeclarationExpr vde = (VariableDeclarationExpr) resourceExpr; + VariableDeclarator vd = vde.getVariable(0); + resourceName = vd.getNameAsString(); + result.addStatement(new ExpressionStmt(vde.clone())); + } else { + // Java 9+ form: try (existingEffectivelyFinalVar) { ... } + // No declaration needed -- the variable already exists in scope. + resourceName = resourceExpr.toString(); + } + + int id = counter.incrementAndGet(); + String primaryExcName = "primaryExc$" + id; + String throwableName = "t$" + id; + String suppressedExcName = "suppressedExc$" + id; + + result.addStatement(declareVar("Throwable", primaryExcName, new NullLiteralExpr())); + + BlockStmt innerTryBlock = (index + 1 < resources.size()) + ? desugarResources(resources, index + 1, body) + : body; + + // catch (Throwable t$n) { primaryExc$n = t$n; throw t$n; } + CatchClause catchClause = new CatchClause(); + catchClause.setParameter(new Parameter(new ClassOrInterfaceType(null, "Throwable"), throwableName)); + BlockStmt catchBody = new BlockStmt(); + catchBody.addStatement(new ExpressionStmt( + new AssignExpr(new NameExpr(primaryExcName), new NameExpr(throwableName), AssignExpr.Operator.ASSIGN))); + catchBody.addStatement(new ThrowStmt(new NameExpr(throwableName))); + catchClause.setBody(catchBody); + + // finally { if (r != null) { if (primaryExc$n != null) { try { r.close(); } catch (Throwable s) { primaryExc$n.addSuppressed(s); } } else { r.close(); } } } + BlockStmt finallyBlock = new BlockStmt(); + + IfStmt excCheck = new IfStmt(); + excCheck.setCondition(notNull(new NameExpr(primaryExcName))); + + TryStmt closeWithSuppression = new TryStmt(); + BlockStmt closeTryBlock = new BlockStmt(); + closeTryBlock.addStatement(new ExpressionStmt(closeCall(resourceName))); + closeWithSuppression.setTryBlock(closeTryBlock); + + CatchClause suppressCatch = new CatchClause(); + suppressCatch.setParameter(new Parameter(new ClassOrInterfaceType(null, "Throwable"), suppressedExcName)); + BlockStmt suppressBody = new BlockStmt(); + suppressBody.addStatement(new ExpressionStmt(new MethodCallExpr( + new NameExpr(primaryExcName), "addSuppressed", NodeList.nodeList(new NameExpr(suppressedExcName))))); + suppressCatch.setBody(suppressBody); + closeWithSuppression.setCatchClauses(NodeList.nodeList(suppressCatch)); + + excCheck.setThenStmt(closeWithSuppression); + + BlockStmt plainClose = new BlockStmt(); + plainClose.addStatement(new ExpressionStmt(closeCall(resourceName))); + excCheck.setElseStmt(plainClose); + + IfStmt nullCheck = new IfStmt(); + nullCheck.setCondition(notNull(new NameExpr(resourceName))); + BlockStmt nullCheckThen = new BlockStmt(); + nullCheckThen.addStatement(excCheck); + nullCheck.setThenStmt(nullCheckThen); + + finallyBlock.addStatement(nullCheck); + + TryStmt resourceTry = new TryStmt(); + resourceTry.setTryBlock(innerTryBlock); + resourceTry.setCatchClauses(NodeList.nodeList(catchClause)); + resourceTry.setFinallyBlock(finallyBlock); + + result.addStatement(resourceTry); + return result; + } + + private static BinaryExpr notNull(Expression e) { + return new BinaryExpr(e, new NullLiteralExpr(), BinaryExpr.Operator.NOT_EQUALS); + } + + private static MethodCallExpr closeCall(String resourceName) { + return new MethodCallExpr(new NameExpr(resourceName), "close"); + } + + private static Statement declareVar(String typeName, String varName, Expression initializer) { + VariableDeclarator vd = new VariableDeclarator(new ClassOrInterfaceType(null, typeName), varName, initializer); + return new ExpressionStmt(new VariableDeclarationExpr(vd)); + } + } +} \ No newline at end of file diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java new file mode 100644 index 00000000000..7aef0839cee --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java @@ -0,0 +1,35 @@ +package de.uka.ilkd.key.java.transformations.pipeline; + +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.CompilationUnit; +import org.junit.jupiter.api.Test; + +/** + * + * @author Alexander Weigl + * @version 1 (12.07.26) + */ +class TryWithResourceReducerTest { + @Test + void test() { + String source = """ + class Demo { + void run() { + try (Resource r1 = new Resource1(); Resource r2 = new Resource2()) { + r1.use(); + r2.use(); + } catch (Exception e) { + System.out.println("caught: " + e); + } finally { + System.out.println("done"); + } + } + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var t = new TryWithResourceReducer(); + t.apply(cu); + System.out.println(cu); + } +} \ No newline at end of file From 976d1c0490e4f165713f9b9375511ed38e17c014 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 12 Jul 2026 14:22:05 +0200 Subject: [PATCH 2/7] add to pipeline # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java --- .../de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java | 1 + 1 file changed, 1 insertion(+) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java index 98470bef204..cf90a5109b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java @@ -40,6 +40,7 @@ public static KeYJavaPipeline createDefault(TransformationPipelineServices pipel KeYJavaPipeline p = new KeYJavaPipeline(pipelineServices); p.add(new TextblockTransformer()); p.add(new MultiCatchReducer()); + p.add(new TryWithResourceReducer()); p.add(new EnumClassBuilder(pipelineServices)); p.add(new RecordClassBuilder(pipelineServices)); p.add(new JMLTransformer(pipelineServices)); From b4e73f372448e564e4d7bc828cdcb043904f76d7 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 12 Jul 2026 14:38:14 +0200 Subject: [PATCH 3/7] more test --- .../pipeline/TryWithResourceReducerTest.java | 143 +++++++++++++++++- 1 file changed, 142 insertions(+), 1 deletion(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java index 7aef0839cee..98dc3ff4a3d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java @@ -4,6 +4,8 @@ import com.github.javaparser.ast.CompilationUnit; import org.junit.jupiter.api.Test; +import static org.assertj.core.api.Assertions.assertThat; + /** * * @author Alexander Weigl @@ -30,6 +32,145 @@ void run() { CompilationUnit cu = StaticJavaParser.parse(source); var t = new TryWithResourceReducer(); t.apply(cu); - System.out.println(cu); + var actual = cu.toString(); + var expected = """ + class Demo { + + void run() { + try { + Resource r1 = new Resource1(); + Throwable primaryExc$1 = null; + try { + Resource r2 = new Resource2(); + Throwable primaryExc$2 = null; + try { + r1.use(); + r2.use(); + } catch (Throwable t$2) { + primaryExc$2 = t$2; + throw t$2; + } finally { + if (r2 != null) { + if (primaryExc$2 != null) + try { + r2.close(); + } catch (Throwable suppressedExc$2) { + primaryExc$2.addSuppressed(suppressedExc$2); + } + else { + r2.close(); + } + } + } + } catch (Throwable t$1) { + primaryExc$1 = t$1; + throw t$1; + } finally { + if (r1 != null) { + if (primaryExc$1 != null) + try { + r1.close(); + } catch (Throwable suppressedExc$1) { + primaryExc$1.addSuppressed(suppressedExc$1); + } + else { + r1.close(); + } + } + } + } catch (Exception e) { + System.out.println("caught: " + e); + } finally { + System.out.println("done"); + } + } + } + """; + + assertThat(actual).isEqualToNormalizingWhitespace(expected); } + + @Test + void testJava9() { + String source = """ + class Demo { + void run() { + Resource r1 = new Resource1(); + try (r1; Resource r2 = new Resource2()) { + r1.use(); + r2.use(); + } catch (Exception e) { + System.out.println("caught: " + e); + } finally { + System.out.println("done"); + } + } + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var t = new TryWithResourceReducer(); + t.apply(cu); + var actual = cu.toString(); + + + var expected = """ + class Demo { + + void run() { + Resource r1 = new Resource1(); + try { + Throwable primaryExc$1 = null; + try { + Resource r2 = new Resource2(); + Throwable primaryExc$2 = null; + try { + r1.use(); + r2.use(); + } catch (Throwable t$2) { + primaryExc$2 = t$2; + throw t$2; + } finally { + if (r2 != null) { + if (primaryExc$2 != null) + try { + r2.close(); + } catch (Throwable suppressedExc$2) { + primaryExc$2.addSuppressed(suppressedExc$2); + } + else { + r2.close(); + } + } + } + } catch (Throwable t$1) { + primaryExc$1 = t$1; + throw t$1; + } finally { + if (r1 != null) { + if (primaryExc$1 != null) + try { + r1.close(); + } catch (Throwable suppressedExc$1) { + primaryExc$1.addSuppressed(suppressedExc$1); + } + else { + r1.close(); + } + } + } + } catch (Exception e) { + System.out.println("caught: " + e); + } finally { + System.out.println("done"); + } + } + } + """; + + System.out.println(actual); + + assertThat(actual).isEqualToNormalizingWhitespace(expected); + } + } \ No newline at end of file From 7204b7e877d421ba8d3154f649a63b3d81118184 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 12 Jul 2026 14:42:58 +0200 Subject: [PATCH 4/7] add sample to Java25 category --- .../examples/Java/TryWithResources/README.txt | 8 +++++ .../TryWithResources/TryWithResources.java | 34 +++++++++++++++++++ .../Java/TryWithResources/project.key | 8 +++++ key.ui/examples/index/samplesIndex.txt | 1 + 4 files changed, 51 insertions(+) create mode 100644 key.ui/examples/Java/TryWithResources/README.txt create mode 100644 key.ui/examples/Java/TryWithResources/TryWithResources.java create mode 100644 key.ui/examples/Java/TryWithResources/project.key diff --git a/key.ui/examples/Java/TryWithResources/README.txt b/key.ui/examples/Java/TryWithResources/README.txt new file mode 100644 index 00000000000..f8e6e05c5cc --- /dev/null +++ b/key.ui/examples/Java/TryWithResources/README.txt @@ -0,0 +1,8 @@ +example.name = Try With Resources +example.path = Java 25 +example.file = project.key +example.additionalFile.1 = TryWithResources.java + +Try-With-Resources statements are supported in KeY. They are reduced to nested try/finally blocks with proper exception suppression handling. + +The proof obligation is verifiable without user interaction. \ No newline at end of file diff --git a/key.ui/examples/Java/TryWithResources/TryWithResources.java b/key.ui/examples/Java/TryWithResources/TryWithResources.java new file mode 100644 index 00000000000..059c83e277d --- /dev/null +++ b/key.ui/examples/Java/TryWithResources/TryWithResources.java @@ -0,0 +1,34 @@ +public final class TryWithResources { + /*@ ensures true; requires true; */ + public void m() throws Exception { + // Simple try-with-resources + try (Resource r = new Resource()) { + r.use(); + } + + // Multiple resources + try (Resource r1 = new Resource(); Resource r2 = new Resource()) { + r1.use(); + r2.use(); + } + + // Java 9+ style with existing variable + Resource existing = new Resource(); + try (existing) { + existing.use(); + } + } + + static class Resource implements AutoCloseable { + /*@ ensures true; requires true; */ + public void use() { + // use the resource + } + + /*@ ensures true; requires true; */ + @Override + public void close() throws Exception { + // close the resource + } + } +} \ No newline at end of file diff --git a/key.ui/examples/Java/TryWithResources/project.key b/key.ui/examples/Java/TryWithResources/project.key new file mode 100644 index 00000000000..6df12214cc9 --- /dev/null +++ b/key.ui/examples/Java/TryWithResources/project.key @@ -0,0 +1,8 @@ +\profile "Java Profile"; +\javaSource "."; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "TryWithResources[TryWithResources::m()].JML operation contract.0", + "name" : "TryWithResources[TryWithResources::m()].JML operation contract.0" +} \ No newline at end of file diff --git a/key.ui/examples/index/samplesIndex.txt b/key.ui/examples/index/samplesIndex.txt index 7bb98991042..afa89037598 100644 --- a/key.ui/examples/index/samplesIndex.txt +++ b/key.ui/examples/index/samplesIndex.txt @@ -25,6 +25,7 @@ Java/MultiCatch/README.txt Java/Records/README.txt Java/Records+CompactConstructor/README.txt Java/TextBlockLiterals/README.txt +Java/TryWithResources/README.txt # The KeY Book (note: the comments here are only for maintainability, if you want to move an entry to a different section, look into the individual txt file!) ## Chapter 15 - Using the KeY Prover From 12372fc6da8ba87a95019451e9491b9cd858ef15 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 12 Jul 2026 22:16:25 +0200 Subject: [PATCH 5/7] fix test cases, adapt Java-Redux --- .../MostSimpleInner.java | 5 + .../CompactConstructor.java | 8 ++ .../InnerRecord.java | 7 ++ .../02_TryWithResourceReducer/NotAllowed.java | 36 ++++++ .../02_TryWithResourceReducer/Point3d.java | 2 + .../RecordOverwriting.java | 14 +++ .../SimpleRecord.java | 6 + .../02_TryWithResourceReducer/Test.java | 24 ++++ .../pipeline/TryWithResourceReducer.java | 82 +++++++------ .../JavaRedux/java/lang/AutoCloseable.java | 5 + .../java/JavaRedux/java/lang/Exception.java | 3 + .../pipeline/TryWithResourceReducerTest.java | 114 +++++++++--------- 12 files changed, 212 insertions(+), 94 deletions(-) create mode 100644 key.core/pipelineTests/innerclass/expected/02_TryWithResourceReducer/MostSimpleInner.java create mode 100644 key.core/pipelineTests/records/expected/02_TryWithResourceReducer/CompactConstructor.java create mode 100644 key.core/pipelineTests/records/expected/02_TryWithResourceReducer/InnerRecord.java create mode 100644 key.core/pipelineTests/records/expected/02_TryWithResourceReducer/NotAllowed.java create mode 100644 key.core/pipelineTests/records/expected/02_TryWithResourceReducer/Point3d.java create mode 100644 key.core/pipelineTests/records/expected/02_TryWithResourceReducer/RecordOverwriting.java create mode 100644 key.core/pipelineTests/records/expected/02_TryWithResourceReducer/SimpleRecord.java create mode 100644 key.core/pipelineTests/simple/expected/02_TryWithResourceReducer/Test.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/AutoCloseable.java diff --git a/key.core/pipelineTests/innerclass/expected/02_TryWithResourceReducer/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/02_TryWithResourceReducer/MostSimpleInner.java new file mode 100644 index 00000000000..a7764c2a007 --- /dev/null +++ b/key.core/pipelineTests/innerclass/expected/02_TryWithResourceReducer/MostSimpleInner.java @@ -0,0 +1,5 @@ +public class MostSimpleInner { + + public static class MyInnerClass { + } +} diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/CompactConstructor.java b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/CompactConstructor.java new file mode 100644 index 00000000000..7875031d112 --- /dev/null +++ b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/CompactConstructor.java @@ -0,0 +1,8 @@ +record Mapping(String from, String to) { + + Mapping { + // compact constructor! + from = "abc"; + to = "def"; + } +} diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/InnerRecord.java b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/InnerRecord.java new file mode 100644 index 00000000000..2046d14ecfc --- /dev/null +++ b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/InnerRecord.java @@ -0,0 +1,7 @@ +import java.lang.Object; + +public class OuterClass { + + final record MyRecord(String test) { + } +} diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/NotAllowed.java b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/NotAllowed.java new file mode 100644 index 00000000000..5941911ccf7 --- /dev/null +++ b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/NotAllowed.java @@ -0,0 +1,36 @@ +//https://mikemybytes.com/2022/02/16/java-records-and-compact-constructors/ +record // package-private +Name(// package-private +String name) { + + // fails with: 'invalid canonical constructor in record Name + // (attempting to assign stronger access privileges; + // was package)' + private Name(String name) { + this.name = name; + } + + static Name of(String name) { + return new Name(name); + } +} + +record Point(int x, int y) { + + Point(int x, int y) { + // boring! + this.x = x; + this.y = y; + } + + Point(int x) { + // a bit weird... + // ... but perfectly fine for the compiler + this(x, 0); + } + + Point() { + // fails with: 'constructor is not canonical, so its first + // statement must invoke another constructor' + } +} diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/Point3d.java b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/Point3d.java new file mode 100644 index 00000000000..cf984e9b6a6 --- /dev/null +++ b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/Point3d.java @@ -0,0 +1,2 @@ +record Point3d(int x, int y, int z) { +} diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/RecordOverwriting.java new file mode 100644 index 00000000000..4cffbb21982 --- /dev/null +++ b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/RecordOverwriting.java @@ -0,0 +1,14 @@ +record MyRecord(String test) { + + public int hashCode() { + return 0; + } + + public boolean equals(Object obj) { + return obj instanceof MyRecord; + } + + public String test() { + return ""; + } +} diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/SimpleRecord.java b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/SimpleRecord.java new file mode 100644 index 00000000000..72c63026dad --- /dev/null +++ b/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/SimpleRecord.java @@ -0,0 +1,6 @@ +public record SimpleRecord(/*@ nullable */ String name) implements Serializable { + + SimpleRecord(String name) { + this.name = name; + } +} diff --git a/key.core/pipelineTests/simple/expected/02_TryWithResourceReducer/Test.java b/key.core/pipelineTests/simple/expected/02_TryWithResourceReducer/Test.java new file mode 100644 index 00000000000..dba29c488a0 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/02_TryWithResourceReducer/Test.java @@ -0,0 +1,24 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java index 8a03873d5a4..c245d4455ec 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java @@ -1,5 +1,11 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.transformations.pipeline; +import java.util.List; +import java.util.concurrent.atomic.AtomicInteger; + import com.github.javaparser.ast.NodeList; import com.github.javaparser.ast.body.Parameter; import com.github.javaparser.ast.body.TypeDeclaration; @@ -10,41 +16,39 @@ import com.github.javaparser.ast.visitor.ModifierVisitor; import com.github.javaparser.ast.visitor.Visitable; -import java.util.List; -import java.util.concurrent.atomic.AtomicInteger; - /// Rewrites every try-with-resources statement into the equivalent nested /// try/finally form that javac itself generates, i.e. for /// ```java /// try (Resource r = open()) { -/// body; +/// body; /// } /// ``` /// this produces: /// ```java /// try { -/// Resource r = open(); -/// Throwable primaryExc$1 = null; -/// try { -/// body; -/// } catch (Throwable t$1) { -/// primaryExc$1 = t$1; -/// throw t$1; -/// } finally { -/// if (r != null) { -/// if (primaryExc$1 != null) { -/// try { r.close(); } catch (Throwable suppressedExc$1) { -/// primaryExc$1.addSuppressed(suppressedExc$1); -/// } -/// } else { r.close(); } -/// } -/// } +/// Resource r = open(); +/// Throwable primaryExc$1 = null; +/// try { +/// body; +/// } catch (Throwable t$1) { +/// primaryExc$1 = t$1; +/// throw t$1; +/// } finally { +/// if (r != null) { +/// if (primaryExc$1 != null) { +/// try { r.close(); } catch (Throwable suppressedExc$1) { +/// primaryExc$1.addSuppressed(suppressedExc$1); +/// } +/// } else { r.close(); } +/// } +/// } /// } /// ``` /// Multiple resources are handled by nesting (last-declared resource closes first), /// and any catch/finally clauses that were attached to the original try are kept /// on an outer try that wraps the whole resource-management block, exactly as /// javac does it. +/// /// @author weigl, Claude Sonnet public class TryWithResourceReducer implements JavaTransformer { private final AtomicInteger counter = new AtomicInteger(); @@ -91,18 +95,17 @@ private BlockStmt desugarResources(List resources, int index, BlockS BlockStmt result = new BlockStmt(); Expression resourceExpr = resources.get(index); - String resourceName; + Expression resourceName; - if (resourceExpr instanceof VariableDeclarationExpr) { + if (resourceExpr instanceof VariableDeclarationExpr vde) { // try (Resource r = new Resource()) { ... } - VariableDeclarationExpr vde = (VariableDeclarationExpr) resourceExpr; VariableDeclarator vd = vde.getVariable(0); - resourceName = vd.getNameAsString(); + resourceName = vd.getNameAsExpression(); result.addStatement(new ExpressionStmt(vde.clone())); } else { // Java 9+ form: try (existingEffectivelyFinalVar) { ... } // No declaration needed -- the variable already exists in scope. - resourceName = resourceExpr.toString(); + resourceName = resourceExpr; } int id = counter.incrementAndGet(); @@ -118,14 +121,17 @@ private BlockStmt desugarResources(List resources, int index, BlockS // catch (Throwable t$n) { primaryExc$n = t$n; throw t$n; } CatchClause catchClause = new CatchClause(); - catchClause.setParameter(new Parameter(new ClassOrInterfaceType(null, "Throwable"), throwableName)); + catchClause.setParameter( + new Parameter(new ClassOrInterfaceType(null, "Throwable"), throwableName)); BlockStmt catchBody = new BlockStmt(); catchBody.addStatement(new ExpressionStmt( - new AssignExpr(new NameExpr(primaryExcName), new NameExpr(throwableName), AssignExpr.Operator.ASSIGN))); + new AssignExpr(new NameExpr(primaryExcName), new NameExpr(throwableName), + AssignExpr.Operator.ASSIGN))); catchBody.addStatement(new ThrowStmt(new NameExpr(throwableName))); catchClause.setBody(catchBody); - // finally { if (r != null) { if (primaryExc$n != null) { try { r.close(); } catch (Throwable s) { primaryExc$n.addSuppressed(s); } } else { r.close(); } } } + // finally { if (r != null) { if (primaryExc$n != null) { try { r.close(); } catch + // (Throwable s) { primaryExc$n.addSuppressed(s); } } else { r.close(); } } } BlockStmt finallyBlock = new BlockStmt(); IfStmt excCheck = new IfStmt(); @@ -137,10 +143,12 @@ private BlockStmt desugarResources(List resources, int index, BlockS closeWithSuppression.setTryBlock(closeTryBlock); CatchClause suppressCatch = new CatchClause(); - suppressCatch.setParameter(new Parameter(new ClassOrInterfaceType(null, "Throwable"), suppressedExcName)); + suppressCatch.setParameter( + new Parameter(new ClassOrInterfaceType(null, "Throwable"), suppressedExcName)); BlockStmt suppressBody = new BlockStmt(); suppressBody.addStatement(new ExpressionStmt(new MethodCallExpr( - new NameExpr(primaryExcName), "addSuppressed", NodeList.nodeList(new NameExpr(suppressedExcName))))); + new NameExpr(primaryExcName), "addSuppressed", + NodeList.nodeList(new NameExpr(suppressedExcName))))); suppressCatch.setBody(suppressBody); closeWithSuppression.setCatchClauses(NodeList.nodeList(suppressCatch)); @@ -151,7 +159,7 @@ private BlockStmt desugarResources(List resources, int index, BlockS excCheck.setElseStmt(plainClose); IfStmt nullCheck = new IfStmt(); - nullCheck.setCondition(notNull(new NameExpr(resourceName))); + nullCheck.setCondition(notNull(resourceName.clone())); BlockStmt nullCheckThen = new BlockStmt(); nullCheckThen.addStatement(excCheck); nullCheck.setThenStmt(nullCheckThen); @@ -171,13 +179,15 @@ private static BinaryExpr notNull(Expression e) { return new BinaryExpr(e, new NullLiteralExpr(), BinaryExpr.Operator.NOT_EQUALS); } - private static MethodCallExpr closeCall(String resourceName) { - return new MethodCallExpr(new NameExpr(resourceName), "close"); + private static MethodCallExpr closeCall(Expression resourceName) { + return new MethodCallExpr(resourceName.clone(), "close"); } - private static Statement declareVar(String typeName, String varName, Expression initializer) { - VariableDeclarator vd = new VariableDeclarator(new ClassOrInterfaceType(null, typeName), varName, initializer); + private static Statement declareVar(String typeName, String varName, + Expression initializer) { + VariableDeclarator vd = new VariableDeclarator(new ClassOrInterfaceType(null, typeName), + varName, initializer); return new ExpressionStmt(new VariableDeclarationExpr(vd)); } } -} \ No newline at end of file +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/AutoCloseable.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/AutoCloseable.java new file mode 100644 index 00000000000..b6fbe467732 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/AutoCloseable.java @@ -0,0 +1,5 @@ +package java.lang; + +public interface AutoCloseable { + void close() throws Exception; +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java index 5be227222d9..4c95e2f36fb 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java @@ -10,4 +10,7 @@ public class Exception extends java.lang.Throwable public Exception(java.lang.String arg0) { super(arg0); } public Exception(java.lang.String arg0, java.lang.Throwable arg1) { super(arg0, arg1); } public Exception(java.lang.Throwable arg0) { super(arg0); } + + /// Try-With-Resource + public final synchronized void addSuppressed(Throwable exception); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java index 98dc3ff4a3d..ea295b29d2d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.transformations.pipeline; import com.github.javaparser.StaticJavaParser; @@ -35,7 +38,7 @@ void run() { var actual = cu.toString(); var expected = """ class Demo { - + void run() { try { Resource r1 = new Resource1(); @@ -94,9 +97,9 @@ void run() { void testJava9() { String source = """ class Demo { + Resource r1 = new Resource1(); void run() { - Resource r1 = new Resource1(); - try (r1; Resource r2 = new Resource2()) { + try (this.r1; Resource r2 = new Resource2()) { r1.use(); r2.use(); } catch (Exception e) { @@ -116,61 +119,56 @@ void run() { var expected = """ class Demo { - - void run() { - Resource r1 = new Resource1(); - try { - Throwable primaryExc$1 = null; - try { - Resource r2 = new Resource2(); - Throwable primaryExc$2 = null; - try { - r1.use(); - r2.use(); - } catch (Throwable t$2) { - primaryExc$2 = t$2; - throw t$2; - } finally { - if (r2 != null) { - if (primaryExc$2 != null) - try { - r2.close(); - } catch (Throwable suppressedExc$2) { - primaryExc$2.addSuppressed(suppressedExc$2); - } - else { - r2.close(); - } - } - } - } catch (Throwable t$1) { - primaryExc$1 = t$1; - throw t$1; - } finally { - if (r1 != null) { - if (primaryExc$1 != null) - try { - r1.close(); - } catch (Throwable suppressedExc$1) { - primaryExc$1.addSuppressed(suppressedExc$1); - } - else { - r1.close(); - } - } - } - } catch (Exception e) { - System.out.println("caught: " + e); - } finally { - System.out.println("done"); - } - } - } + Resource r1 = new Resource1(); + void run() { + try { + Throwable primaryExc$1 = null; + try { + Resource r2 = new Resource2(); + Throwable primaryExc$2 = null; + try { + r1.use(); + r2.use(); + } catch (Throwable t$2) { + primaryExc$2 = t$2; + throw t$2; + } finally { + if (r2 != null) { + if (primaryExc$2 != null) + try { + r2.close(); + } catch (Throwable suppressedExc$2) { + primaryExc$2.addSuppressed(suppressedExc$2); + } + else { + r2.close(); + } + } + } + } catch (Throwable t$1) { + primaryExc$1 = t$1; + throw t$1; + } finally { + if (this.r1 != null) { + if (primaryExc$1 != null) + try { + this.r1.close(); + } catch (Throwable suppressedExc$1) { + primaryExc$1.addSuppressed(suppressedExc$1); + } + else { + this.r1.close(); + } + } + } + } catch (Exception e) { + System.out.println("caught: " + e); + } finally { + System.out.println("done"); + } + } + } """; - - System.out.println(actual); - assertThat(actual).isEqualToNormalizingWhitespace(expected); } - -} \ No newline at end of file +} From f677fd65907dd1e7be444b556ac7de6fd508bb02 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 13 Jul 2026 20:08:17 +0200 Subject: [PATCH 6/7] Make Closeable subtype of AutoCloseable, move addSuppressed to Throwable Added some specifications to addSuppressed so that it is closed automatically --- .../key/java/JavaRedux/java/io/Closeable.java | 4 ++-- .../key/java/JavaRedux/java/lang/Exception.java | 2 -- .../key/java/JavaRedux/java/lang/Throwable.java | 17 +++++++++++++++++ .../Java/TryWithResources/TryWithResources.java | 2 +- 4 files changed, 20 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/io/Closeable.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/io/Closeable.java index d74e47556e1..8b0e182eb1f 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/io/Closeable.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/io/Closeable.java @@ -1,5 +1,5 @@ package java.io; -public interface Closeable { +public interface Closeable extends AutoCloseable { void close() throws IOException; -} \ No newline at end of file +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java index 4c95e2f36fb..4648719f6e0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Exception.java @@ -11,6 +11,4 @@ public class Exception extends java.lang.Throwable public Exception(java.lang.String arg0, java.lang.Throwable arg1) { super(arg0, arg1); } public Exception(java.lang.Throwable arg0) { super(arg0); } - /// Try-With-Resource - public final synchronized void addSuppressed(Throwable exception); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Throwable.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Throwable.java index dcfd3dc01a9..207b0062eb1 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Throwable.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Throwable.java @@ -12,6 +12,12 @@ public class Throwable extends java.lang.Object implements java.io.Serializable //@ protected nullable ghost String message = null; //@ protected nullable ghost Throwable cause = null; + //@ protected model \seq suppressedExceptions; + //@ protected model \locset suppressedListFootprint; + //@ accessible suppressedListFootprint: suppressedListFootprint; + //@ accessible suppressedExceptions: suppressedListFootprint; + //@ protected invariant \intersect(suppressedListFootprint,\set_union(this.message, this.cause))==\empty; + /*@ public normal_behavior @ requires true; @@ -78,4 +84,15 @@ public Throwable(java.lang.Throwable arg0) { public java.lang.Throwable fillInStackTrace(); // public java.lang.StackTraceElement[] getStackTrace(); // public void setStackTrace(java.lang.StackTraceElement[] arg0); + + /// Try-With-Resource + /// the helper modifier should not be needed, but otherwise proofs of callers stop because they cannot show the + /// throwable invariant + /*@ public normal_behavior + @ assignable suppressedListFootprint; + @ accessible suppressedListFootprint; + @ ensures suppressedExceptions == \seq_concat(suppressedExceptions, \seq_singleton(exception)); + */ + public /*@ helper @*/ final synchronized void addSuppressed(Throwable exception); + } diff --git a/key.ui/examples/Java/TryWithResources/TryWithResources.java b/key.ui/examples/Java/TryWithResources/TryWithResources.java index 059c83e277d..8a2c465a282 100644 --- a/key.ui/examples/Java/TryWithResources/TryWithResources.java +++ b/key.ui/examples/Java/TryWithResources/TryWithResources.java @@ -19,7 +19,7 @@ public void m() throws Exception { } } - static class Resource implements AutoCloseable { + static final class Resource implements AutoCloseable { /*@ ensures true; requires true; */ public void use() { // use the resource From e50c794d35e6b4bd7b27624ff7aa37e55adf39d0 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Tue, 14 Jul 2026 00:52:39 +0200 Subject: [PATCH 7/7] fix tests after rebasing --- .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../{05_JMLTransformer => 06_JMLTransformer}/MostSimpleInner.java | 0 .../{06_JmlDocRemoval => 07_JmlDocRemoval}/MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../{13_CreateBuilder => 14_CreateBuilder}/MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../{03_EnumClassBuilder => 04_EnumClassBuilder}/InnerRecord.java | 0 .../{03_EnumClassBuilder => 04_EnumClassBuilder}/NotAllowed.java | 0 .../{03_EnumClassBuilder => 04_EnumClassBuilder}/Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../{04_RecordClassBuilder => 05_RecordClassBuilder}/Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../{05_JMLTransformer => 06_JMLTransformer}/InnerRecord.java | 0 .../{05_JMLTransformer => 06_JMLTransformer}/NotAllowed.java | 0 .../{05_JMLTransformer => 06_JMLTransformer}/Point3d.java | 0 .../RecordOverwriting.java | 0 .../{05_JMLTransformer => 06_JMLTransformer}/SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../{06_JmlDocRemoval => 07_JmlDocRemoval}/InnerRecord.java | 0 .../{06_JmlDocRemoval => 07_JmlDocRemoval}/NotAllowed.java | 0 .../expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/Point3d.java | 0 .../{06_JmlDocRemoval => 07_JmlDocRemoval}/RecordOverwriting.java | 0 .../{06_JmlDocRemoval => 07_JmlDocRemoval}/SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../{13_CreateBuilder => 14_CreateBuilder}/InnerRecord.java | 0 .../{13_CreateBuilder => 14_CreateBuilder}/NotAllowed.java | 0 .../expected/{13_CreateBuilder => 14_CreateBuilder}/Point3d.java | 0 .../{13_CreateBuilder => 14_CreateBuilder}/RecordOverwriting.java | 0 .../{13_CreateBuilder => 14_CreateBuilder}/SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../CompactConstructor.java | 0 .../InnerRecord.java | 0 .../NotAllowed.java | 0 .../Point3d.java | 0 .../RecordOverwriting.java | 0 .../SimpleRecord.java | 0 .../Test.java | 0 .../{03_EnumClassBuilder => 04_EnumClassBuilder}/Test.java | 0 .../{04_RecordClassBuilder => 05_RecordClassBuilder}/Test.java | 0 .../expected/{05_JMLTransformer => 06_JMLTransformer}/Test.java | 0 .../expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/Test.java | 0 .../{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../expected/{13_CreateBuilder => 14_CreateBuilder}/Test.java | 0 .../{14_CreateObjectBuilder => 15_CreateObjectBuilder}/Test.java | 0 .../Test.java | 0 .../Test.java | 0 120 files changed, 0 insertions(+), 0 deletions(-) rename key.core/pipelineTests/innerclass/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{05_JMLTransformer => 06_JMLTransformer}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{13_CreateBuilder => 14_CreateBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/MostSimpleInner.java (100%) rename key.core/pipelineTests/records/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{05_JMLTransformer => 06_JMLTransformer}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{05_JMLTransformer => 06_JMLTransformer}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{05_JMLTransformer => 06_JMLTransformer}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{05_JMLTransformer => 06_JMLTransformer}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{05_JMLTransformer => 06_JMLTransformer}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{05_JMLTransformer => 06_JMLTransformer}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{13_CreateBuilder => 14_CreateBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{13_CreateBuilder => 14_CreateBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{13_CreateBuilder => 14_CreateBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{13_CreateBuilder => 14_CreateBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{13_CreateBuilder => 14_CreateBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{13_CreateBuilder => 14_CreateBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/SimpleRecord.java (100%) rename key.core/pipelineTests/records/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/CompactConstructor.java (100%) rename key.core/pipelineTests/records/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/InnerRecord.java (100%) rename key.core/pipelineTests/records/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/NotAllowed.java (100%) rename key.core/pipelineTests/records/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/Point3d.java (100%) rename key.core/pipelineTests/records/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/RecordOverwriting.java (100%) rename key.core/pipelineTests/records/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/SimpleRecord.java (100%) rename key.core/pipelineTests/simple/expected/{02_TryWithResourceReducer => 03_TryWithResourceReducer}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{03_EnumClassBuilder => 04_EnumClassBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{04_RecordClassBuilder => 05_RecordClassBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{05_JMLTransformer => 06_JMLTransformer}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{06_JmlDocRemoval => 07_JmlDocRemoval}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{07_ImplicitFieldAdder => 08_ImplicitFieldAdder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{08_InstanceAllocationMethodBuilder => 09_InstanceAllocationMethodBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{09_ConstructorNormalformBuilder => 10_ConstructorNormalformBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{10_ClassPreparationMethodBuilder => 11_ClassPreparationMethodBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{11_ClassInitializeMethodBuilder => 12_ClassInitializeMethodBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{12_PrepareObjectBuilder => 13_PrepareObjectBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{13_CreateBuilder => 14_CreateBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{14_CreateObjectBuilder => 15_CreateObjectBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{15_LocalClassTransformation => 16_LocalClassTransformation}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{16_ConstantStringExpressionEvaluator => 17_ConstantStringExpressionEvaluator}/Test.java (100%) diff --git a/key.core/pipelineTests/innerclass/expected/02_TryWithResourceReducer/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/03_TryWithResourceReducer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/02_TryWithResourceReducer/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/03_TryWithResourceReducer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/03_EnumClassBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/04_EnumClassBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/03_EnumClassBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/04_EnumClassBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/04_RecordClassBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/05_RecordClassBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/04_RecordClassBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/05_RecordClassBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/05_JMLTransformer/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/06_JMLTransformer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/05_JMLTransformer/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/06_JMLTransformer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/06_JmlDocRemoval/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/07_JmlDocRemoval/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/06_JmlDocRemoval/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/07_JmlDocRemoval/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/07_ImplicitFieldAdder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/08_ImplicitFieldAdder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/07_ImplicitFieldAdder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/08_ImplicitFieldAdder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/08_InstanceAllocationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/09_InstanceAllocationMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/08_InstanceAllocationMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/09_InstanceAllocationMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/09_ConstructorNormalformBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/10_ConstructorNormalformBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/09_ConstructorNormalformBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/10_ConstructorNormalformBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/10_ClassPreparationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/11_ClassPreparationMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/10_ClassPreparationMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/11_ClassPreparationMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/11_ClassInitializeMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/12_ClassInitializeMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/11_ClassInitializeMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/12_ClassInitializeMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/12_PrepareObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/13_PrepareObjectBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/12_PrepareObjectBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/13_PrepareObjectBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/13_CreateBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/14_CreateBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/13_CreateBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/14_CreateBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/14_CreateObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/15_CreateObjectBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/14_CreateObjectBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/15_CreateObjectBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/15_LocalClassTransformation/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/16_LocalClassTransformation/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/15_LocalClassTransformation/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/16_LocalClassTransformation/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/16_ConstantStringExpressionEvaluator/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/17_ConstantStringExpressionEvaluator/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/16_ConstantStringExpressionEvaluator/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/17_ConstantStringExpressionEvaluator/MostSimpleInner.java diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/CompactConstructor.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_TryWithResourceReducer/CompactConstructor.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/InnerRecord.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_TryWithResourceReducer/InnerRecord.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/NotAllowed.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_TryWithResourceReducer/NotAllowed.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/Point3d.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_TryWithResourceReducer/Point3d.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/Point3d.java diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_TryWithResourceReducer/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/02_TryWithResourceReducer/SimpleRecord.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_TryWithResourceReducer/SimpleRecord.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/04_EnumClassBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/04_EnumClassBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/04_EnumClassBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/04_EnumClassBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/04_EnumClassBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/04_RecordClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_RecordClassBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/05_RecordClassBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/04_RecordClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_RecordClassBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/05_RecordClassBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/04_RecordClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_RecordClassBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/05_RecordClassBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/04_RecordClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_RecordClassBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/05_RecordClassBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/04_RecordClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_RecordClassBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/05_RecordClassBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/04_RecordClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/05_RecordClassBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_RecordClassBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/05_RecordClassBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/05_JMLTransformer/CompactConstructor.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JMLTransformer/CompactConstructor.java rename to key.core/pipelineTests/records/expected/06_JMLTransformer/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/05_JMLTransformer/InnerRecord.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JMLTransformer/InnerRecord.java rename to key.core/pipelineTests/records/expected/06_JMLTransformer/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/05_JMLTransformer/NotAllowed.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JMLTransformer/NotAllowed.java rename to key.core/pipelineTests/records/expected/06_JMLTransformer/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/05_JMLTransformer/Point3d.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JMLTransformer/Point3d.java rename to key.core/pipelineTests/records/expected/06_JMLTransformer/Point3d.java diff --git a/key.core/pipelineTests/records/expected/05_JMLTransformer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JMLTransformer/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/06_JMLTransformer/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/05_JMLTransformer/SimpleRecord.java b/key.core/pipelineTests/records/expected/06_JMLTransformer/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JMLTransformer/SimpleRecord.java rename to key.core/pipelineTests/records/expected/06_JMLTransformer/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/06_JmlDocRemoval/CompactConstructor.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_JmlDocRemoval/CompactConstructor.java rename to key.core/pipelineTests/records/expected/07_JmlDocRemoval/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/06_JmlDocRemoval/InnerRecord.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_JmlDocRemoval/InnerRecord.java rename to key.core/pipelineTests/records/expected/07_JmlDocRemoval/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/06_JmlDocRemoval/NotAllowed.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_JmlDocRemoval/NotAllowed.java rename to key.core/pipelineTests/records/expected/07_JmlDocRemoval/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/06_JmlDocRemoval/Point3d.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_JmlDocRemoval/Point3d.java rename to key.core/pipelineTests/records/expected/07_JmlDocRemoval/Point3d.java diff --git a/key.core/pipelineTests/records/expected/06_JmlDocRemoval/RecordOverwriting.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_JmlDocRemoval/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/07_JmlDocRemoval/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/06_JmlDocRemoval/SimpleRecord.java b/key.core/pipelineTests/records/expected/07_JmlDocRemoval/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_JmlDocRemoval/SimpleRecord.java rename to key.core/pipelineTests/records/expected/07_JmlDocRemoval/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/CompactConstructor.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/InnerRecord.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/InnerRecord.java rename to key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/NotAllowed.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/NotAllowed.java rename to key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/Point3d.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/Point3d.java rename to key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/SimpleRecord.java b/key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/08_ImplicitFieldAdder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/09_InstanceAllocationMethodBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/Point3d.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/10_ConstructorNormalformBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/11_ClassPreparationMethodBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/12_ClassInitializeMethodBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/Point3d.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/13_PrepareObjectBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/13_CreateBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/14_CreateBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/13_CreateBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/14_CreateBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/13_CreateBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/14_CreateBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/13_CreateBuilder/Point3d.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/14_CreateBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/13_CreateBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/14_CreateBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/13_CreateBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/14_CreateBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/14_CreateBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_CreateObjectBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/15_CreateObjectBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_CreateObjectBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/15_CreateObjectBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_CreateObjectBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/15_CreateObjectBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/Point3d.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_CreateObjectBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/15_CreateObjectBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_CreateObjectBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/15_CreateObjectBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/15_CreateObjectBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_CreateObjectBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/15_CreateObjectBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/15_LocalClassTransformation/CompactConstructor.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_LocalClassTransformation/CompactConstructor.java rename to key.core/pipelineTests/records/expected/16_LocalClassTransformation/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/15_LocalClassTransformation/InnerRecord.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_LocalClassTransformation/InnerRecord.java rename to key.core/pipelineTests/records/expected/16_LocalClassTransformation/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/15_LocalClassTransformation/NotAllowed.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_LocalClassTransformation/NotAllowed.java rename to key.core/pipelineTests/records/expected/16_LocalClassTransformation/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/15_LocalClassTransformation/Point3d.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_LocalClassTransformation/Point3d.java rename to key.core/pipelineTests/records/expected/16_LocalClassTransformation/Point3d.java diff --git a/key.core/pipelineTests/records/expected/15_LocalClassTransformation/RecordOverwriting.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_LocalClassTransformation/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/16_LocalClassTransformation/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/15_LocalClassTransformation/SimpleRecord.java b/key.core/pipelineTests/records/expected/16_LocalClassTransformation/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_LocalClassTransformation/SimpleRecord.java rename to key.core/pipelineTests/records/expected/16_LocalClassTransformation/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/CompactConstructor.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/CompactConstructor.java rename to key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/InnerRecord.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/InnerRecord.java rename to key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/NotAllowed.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/NotAllowed.java rename to key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/Point3d.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/Point3d.java rename to key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/Point3d.java diff --git a/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/RecordOverwriting.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/SimpleRecord.java b/key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/SimpleRecord.java rename to key.core/pipelineTests/records/expected/17_ConstantStringExpressionEvaluator/SimpleRecord.java diff --git a/key.core/pipelineTests/simple/expected/02_TryWithResourceReducer/Test.java b/key.core/pipelineTests/simple/expected/03_TryWithResourceReducer/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/02_TryWithResourceReducer/Test.java rename to key.core/pipelineTests/simple/expected/03_TryWithResourceReducer/Test.java diff --git a/key.core/pipelineTests/simple/expected/03_EnumClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/04_EnumClassBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/03_EnumClassBuilder/Test.java rename to key.core/pipelineTests/simple/expected/04_EnumClassBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/04_RecordClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/05_RecordClassBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/04_RecordClassBuilder/Test.java rename to key.core/pipelineTests/simple/expected/05_RecordClassBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/05_JMLTransformer/Test.java b/key.core/pipelineTests/simple/expected/06_JMLTransformer/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/05_JMLTransformer/Test.java rename to key.core/pipelineTests/simple/expected/06_JMLTransformer/Test.java diff --git a/key.core/pipelineTests/simple/expected/06_JmlDocRemoval/Test.java b/key.core/pipelineTests/simple/expected/07_JmlDocRemoval/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/06_JmlDocRemoval/Test.java rename to key.core/pipelineTests/simple/expected/07_JmlDocRemoval/Test.java diff --git a/key.core/pipelineTests/simple/expected/07_ImplicitFieldAdder/Test.java b/key.core/pipelineTests/simple/expected/08_ImplicitFieldAdder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/07_ImplicitFieldAdder/Test.java rename to key.core/pipelineTests/simple/expected/08_ImplicitFieldAdder/Test.java diff --git a/key.core/pipelineTests/simple/expected/08_InstanceAllocationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/09_InstanceAllocationMethodBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/08_InstanceAllocationMethodBuilder/Test.java rename to key.core/pipelineTests/simple/expected/09_InstanceAllocationMethodBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/09_ConstructorNormalformBuilder/Test.java b/key.core/pipelineTests/simple/expected/10_ConstructorNormalformBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/09_ConstructorNormalformBuilder/Test.java rename to key.core/pipelineTests/simple/expected/10_ConstructorNormalformBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/10_ClassPreparationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/11_ClassPreparationMethodBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/10_ClassPreparationMethodBuilder/Test.java rename to key.core/pipelineTests/simple/expected/11_ClassPreparationMethodBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/11_ClassInitializeMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/12_ClassInitializeMethodBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/11_ClassInitializeMethodBuilder/Test.java rename to key.core/pipelineTests/simple/expected/12_ClassInitializeMethodBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/12_PrepareObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/13_PrepareObjectBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/12_PrepareObjectBuilder/Test.java rename to key.core/pipelineTests/simple/expected/13_PrepareObjectBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/13_CreateBuilder/Test.java b/key.core/pipelineTests/simple/expected/14_CreateBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/13_CreateBuilder/Test.java rename to key.core/pipelineTests/simple/expected/14_CreateBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/14_CreateObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/15_CreateObjectBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/14_CreateObjectBuilder/Test.java rename to key.core/pipelineTests/simple/expected/15_CreateObjectBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/15_LocalClassTransformation/Test.java b/key.core/pipelineTests/simple/expected/16_LocalClassTransformation/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/15_LocalClassTransformation/Test.java rename to key.core/pipelineTests/simple/expected/16_LocalClassTransformation/Test.java diff --git a/key.core/pipelineTests/simple/expected/16_ConstantStringExpressionEvaluator/Test.java b/key.core/pipelineTests/simple/expected/17_ConstantStringExpressionEvaluator/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/16_ConstantStringExpressionEvaluator/Test.java rename to key.core/pipelineTests/simple/expected/17_ConstantStringExpressionEvaluator/Test.java