diff --git a/key.core/pipelineTests/innerclass/expected/03_EnumClassBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/03_TryWithResourceReducer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/03_EnumClassBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/03_TryWithResourceReducer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/04_RecordClassBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/04_EnumClassBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/04_RecordClassBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/04_EnumClassBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/05_JMLTransformer/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/05_RecordClassBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/05_JMLTransformer/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/05_RecordClassBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/06_JmlDocRemoval/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/06_JMLTransformer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/06_JmlDocRemoval/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/06_JMLTransformer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/07_JmlDocRemoval/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/07_JmlDocRemoval/MostSimpleInner.java new file mode 100644 index 00000000000..a7764c2a007 --- /dev/null +++ b/key.core/pipelineTests/innerclass/expected/07_JmlDocRemoval/MostSimpleInner.java @@ -0,0 +1,5 @@ +public class MostSimpleInner { + + public static class MyInnerClass { + } +} 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/03_EnumClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/Point3d.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_EnumClassBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/04_EnumClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/CompactConstructor.java new file mode 100644 index 00000000000..7875031d112 --- /dev/null +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/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/04_EnumClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/InnerRecord.java new file mode 100644 index 00000000000..2046d14ecfc --- /dev/null +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/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/04_EnumClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/NotAllowed.java new file mode 100644 index 00000000000..5941911ccf7 --- /dev/null +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/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/04_EnumClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/Point3d.java new file mode 100644 index 00000000000..cf984e9b6a6 --- /dev/null +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/Point3d.java @@ -0,0 +1,2 @@ +record Point3d(int x, int y, int z) { +} diff --git a/key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java new file mode 100644 index 00000000000..4cffbb21982 --- /dev/null +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/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/04_EnumClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/SimpleRecord.java new file mode 100644 index 00000000000..72c63026dad --- /dev/null +++ b/key.core/pipelineTests/records/expected/04_EnumClassBuilder/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/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/03_EnumClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/03_TryWithResourceReducer/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/03_EnumClassBuilder/Test.java rename to key.core/pipelineTests/simple/expected/03_TryWithResourceReducer/Test.java diff --git a/key.core/pipelineTests/simple/expected/04_RecordClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/04_EnumClassBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/04_RecordClassBuilder/Test.java rename to key.core/pipelineTests/simple/expected/04_EnumClassBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/05_JMLTransformer/Test.java b/key.core/pipelineTests/simple/expected/05_RecordClassBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/05_JMLTransformer/Test.java rename to key.core/pipelineTests/simple/expected/05_RecordClassBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/06_JmlDocRemoval/Test.java b/key.core/pipelineTests/simple/expected/06_JMLTransformer/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/06_JmlDocRemoval/Test.java rename to key.core/pipelineTests/simple/expected/06_JMLTransformer/Test.java diff --git a/key.core/pipelineTests/simple/expected/07_JmlDocRemoval/Test.java b/key.core/pipelineTests/simple/expected/07_JmlDocRemoval/Test.java new file mode 100644 index 00000000000..dba29c488a0 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/07_JmlDocRemoval/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/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 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)); 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..c245d4455ec --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java @@ -0,0 +1,193 @@ +/* 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; +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; + +/// 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); + Expression resourceName; + + if (resourceExpr instanceof VariableDeclarationExpr vde) { + // try (Resource r = new Resource()) { ... } + VariableDeclarator vd = vde.getVariable(0); + 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; + } + + 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(resourceName.clone())); + 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(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); + return new ExpressionStmt(new VariableDeclarationExpr(vd)); + } + } +} 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/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..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 @@ -10,4 +10,5 @@ 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); } + } 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.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..ea295b29d2d --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducerTest.java @@ -0,0 +1,174 @@ +/* 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; +import com.github.javaparser.ast.CompilationUnit; +import org.junit.jupiter.api.Test; + +import static org.assertj.core.api.Assertions.assertThat; + +/** + * + * @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); + 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 { + Resource r1 = new Resource1(); + void run() { + try (this.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 { + 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"); + } + } + } + """; + assertThat(actual).isEqualToNormalizingWhitespace(expected); + } +} 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..8a2c465a282 --- /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 final 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