diff --git a/key.core/pipelineTests/innerclass/expected/02_EnumClassBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/02_MultiCatchReducer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/02_EnumClassBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/02_MultiCatchReducer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/03_RecordClassBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/03_EnumClassBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/03_RecordClassBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/03_EnumClassBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/04_JMLTransformer/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/04_RecordClassBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/04_JMLTransformer/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/04_RecordClassBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/05_JmlDocRemoval/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/05_JMLTransformer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/05_JmlDocRemoval/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/05_JMLTransformer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/06_JmlDocRemoval/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/06_JmlDocRemoval/MostSimpleInner.java new file mode 100644 index 00000000000..a7764c2a007 --- /dev/null +++ b/key.core/pipelineTests/innerclass/expected/06_JmlDocRemoval/MostSimpleInner.java @@ -0,0 +1,5 @@ +public class MostSimpleInner { + + public static class MyInnerClass { + } +} diff --git a/key.core/pipelineTests/innerclass/expected/06_ImplicitFieldAdder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/07_ImplicitFieldAdder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/06_ImplicitFieldAdder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/07_ImplicitFieldAdder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/07_InstanceAllocationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/08_InstanceAllocationMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/07_InstanceAllocationMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/08_InstanceAllocationMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/08_ConstructorNormalformBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/09_ConstructorNormalformBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/08_ConstructorNormalformBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/09_ConstructorNormalformBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/09_ClassPreparationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/10_ClassPreparationMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/09_ClassPreparationMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/10_ClassPreparationMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/10_ClassInitializeMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/11_ClassInitializeMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/10_ClassInitializeMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/11_ClassInitializeMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/11_PrepareObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/12_PrepareObjectBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/11_PrepareObjectBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/12_PrepareObjectBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/12_CreateBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/13_CreateBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/12_CreateBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/13_CreateBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/13_CreateObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/14_CreateObjectBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/13_CreateObjectBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/14_CreateObjectBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/14_LocalClassTransformation/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/15_LocalClassTransformation/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/14_LocalClassTransformation/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/15_LocalClassTransformation/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/15_ConstantStringExpressionEvaluator/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/16_ConstantStringExpressionEvaluator/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/15_ConstantStringExpressionEvaluator/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/16_ConstantStringExpressionEvaluator/MostSimpleInner.java diff --git a/key.core/pipelineTests/records/expected/02_EnumClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_EnumClassBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/02_MultiCatchReducer/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/02_EnumClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_EnumClassBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/02_MultiCatchReducer/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/02_EnumClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_EnumClassBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/02_MultiCatchReducer/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/02_EnumClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_EnumClassBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/02_MultiCatchReducer/Point3d.java diff --git a/key.core/pipelineTests/records/expected/02_EnumClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_EnumClassBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/02_MultiCatchReducer/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/02_EnumClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/02_MultiCatchReducer/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/02_EnumClassBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/02_MultiCatchReducer/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/03_EnumClassBuilder/CompactConstructor.java new file mode 100644 index 00000000000..7875031d112 --- /dev/null +++ b/key.core/pipelineTests/records/expected/03_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/03_EnumClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/03_EnumClassBuilder/InnerRecord.java new file mode 100644 index 00000000000..2046d14ecfc --- /dev/null +++ b/key.core/pipelineTests/records/expected/03_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/03_EnumClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/03_EnumClassBuilder/NotAllowed.java new file mode 100644 index 00000000000..5941911ccf7 --- /dev/null +++ b/key.core/pipelineTests/records/expected/03_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/03_EnumClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/03_EnumClassBuilder/Point3d.java new file mode 100644 index 00000000000..cf984e9b6a6 --- /dev/null +++ b/key.core/pipelineTests/records/expected/03_EnumClassBuilder/Point3d.java @@ -0,0 +1,2 @@ +record Point3d(int x, int y, int z) { +} diff --git a/key.core/pipelineTests/records/expected/03_EnumClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/03_EnumClassBuilder/RecordOverwriting.java new file mode 100644 index 00000000000..4cffbb21982 --- /dev/null +++ b/key.core/pipelineTests/records/expected/03_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/03_EnumClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/03_EnumClassBuilder/SimpleRecord.java new file mode 100644 index 00000000000..72c63026dad --- /dev/null +++ b/key.core/pipelineTests/records/expected/03_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/03_RecordClassBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/04_RecordClassBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_RecordClassBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/04_RecordClassBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/03_RecordClassBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/04_RecordClassBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_RecordClassBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/04_RecordClassBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/03_RecordClassBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/04_RecordClassBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_RecordClassBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/04_RecordClassBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/03_RecordClassBuilder/Point3d.java b/key.core/pipelineTests/records/expected/04_RecordClassBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_RecordClassBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/04_RecordClassBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/03_RecordClassBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/04_RecordClassBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_RecordClassBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/04_RecordClassBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/03_RecordClassBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/04_RecordClassBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/03_RecordClassBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/04_RecordClassBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/04_JMLTransformer/CompactConstructor.java b/key.core/pipelineTests/records/expected/05_JMLTransformer/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_JMLTransformer/CompactConstructor.java rename to key.core/pipelineTests/records/expected/05_JMLTransformer/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/04_JMLTransformer/InnerRecord.java b/key.core/pipelineTests/records/expected/05_JMLTransformer/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_JMLTransformer/InnerRecord.java rename to key.core/pipelineTests/records/expected/05_JMLTransformer/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/04_JMLTransformer/NotAllowed.java b/key.core/pipelineTests/records/expected/05_JMLTransformer/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_JMLTransformer/NotAllowed.java rename to key.core/pipelineTests/records/expected/05_JMLTransformer/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/04_JMLTransformer/Point3d.java b/key.core/pipelineTests/records/expected/05_JMLTransformer/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_JMLTransformer/Point3d.java rename to key.core/pipelineTests/records/expected/05_JMLTransformer/Point3d.java diff --git a/key.core/pipelineTests/records/expected/04_JMLTransformer/RecordOverwriting.java b/key.core/pipelineTests/records/expected/05_JMLTransformer/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_JMLTransformer/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/05_JMLTransformer/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/04_JMLTransformer/SimpleRecord.java b/key.core/pipelineTests/records/expected/05_JMLTransformer/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/04_JMLTransformer/SimpleRecord.java rename to key.core/pipelineTests/records/expected/05_JMLTransformer/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/05_JmlDocRemoval/CompactConstructor.java b/key.core/pipelineTests/records/expected/06_JmlDocRemoval/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JmlDocRemoval/CompactConstructor.java rename to key.core/pipelineTests/records/expected/06_JmlDocRemoval/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/05_JmlDocRemoval/InnerRecord.java b/key.core/pipelineTests/records/expected/06_JmlDocRemoval/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JmlDocRemoval/InnerRecord.java rename to key.core/pipelineTests/records/expected/06_JmlDocRemoval/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/05_JmlDocRemoval/NotAllowed.java b/key.core/pipelineTests/records/expected/06_JmlDocRemoval/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JmlDocRemoval/NotAllowed.java rename to key.core/pipelineTests/records/expected/06_JmlDocRemoval/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/05_JmlDocRemoval/Point3d.java b/key.core/pipelineTests/records/expected/06_JmlDocRemoval/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JmlDocRemoval/Point3d.java rename to key.core/pipelineTests/records/expected/06_JmlDocRemoval/Point3d.java diff --git a/key.core/pipelineTests/records/expected/05_JmlDocRemoval/RecordOverwriting.java b/key.core/pipelineTests/records/expected/06_JmlDocRemoval/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JmlDocRemoval/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/06_JmlDocRemoval/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/05_JmlDocRemoval/SimpleRecord.java b/key.core/pipelineTests/records/expected/06_JmlDocRemoval/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/05_JmlDocRemoval/SimpleRecord.java rename to key.core/pipelineTests/records/expected/06_JmlDocRemoval/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/CompactConstructor.java b/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/InnerRecord.java b/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/InnerRecord.java rename to key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/NotAllowed.java b/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/NotAllowed.java rename to key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/Point3d.java b/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/Point3d.java rename to key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/SimpleRecord.java b/key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/06_ImplicitFieldAdder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/07_ImplicitFieldAdder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/07_InstanceAllocationMethodBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/08_InstanceAllocationMethodBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/Point3d.java b/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/08_ConstructorNormalformBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/09_ConstructorNormalformBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/09_ClassPreparationMethodBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/10_ClassPreparationMethodBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/Point3d.java b/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/10_ClassInitializeMethodBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/11_ClassInitializeMethodBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/Point3d.java b/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/11_PrepareObjectBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/12_PrepareObjectBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/12_CreateBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/13_CreateBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_CreateBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/13_CreateBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/12_CreateBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/13_CreateBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_CreateBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/13_CreateBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/12_CreateBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/13_CreateBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_CreateBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/13_CreateBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/12_CreateBuilder/Point3d.java b/key.core/pipelineTests/records/expected/13_CreateBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_CreateBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/13_CreateBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/12_CreateBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/13_CreateBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_CreateBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/13_CreateBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/12_CreateBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/13_CreateBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/12_CreateBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/13_CreateBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/13_CreateObjectBuilder/CompactConstructor.java b/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateObjectBuilder/CompactConstructor.java rename to key.core/pipelineTests/records/expected/14_CreateObjectBuilder/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/13_CreateObjectBuilder/InnerRecord.java b/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateObjectBuilder/InnerRecord.java rename to key.core/pipelineTests/records/expected/14_CreateObjectBuilder/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/13_CreateObjectBuilder/NotAllowed.java b/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateObjectBuilder/NotAllowed.java rename to key.core/pipelineTests/records/expected/14_CreateObjectBuilder/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/13_CreateObjectBuilder/Point3d.java b/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateObjectBuilder/Point3d.java rename to key.core/pipelineTests/records/expected/14_CreateObjectBuilder/Point3d.java diff --git a/key.core/pipelineTests/records/expected/13_CreateObjectBuilder/RecordOverwriting.java b/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateObjectBuilder/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/14_CreateObjectBuilder/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/13_CreateObjectBuilder/SimpleRecord.java b/key.core/pipelineTests/records/expected/14_CreateObjectBuilder/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/13_CreateObjectBuilder/SimpleRecord.java rename to key.core/pipelineTests/records/expected/14_CreateObjectBuilder/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/14_LocalClassTransformation/CompactConstructor.java b/key.core/pipelineTests/records/expected/15_LocalClassTransformation/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_LocalClassTransformation/CompactConstructor.java rename to key.core/pipelineTests/records/expected/15_LocalClassTransformation/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/14_LocalClassTransformation/InnerRecord.java b/key.core/pipelineTests/records/expected/15_LocalClassTransformation/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_LocalClassTransformation/InnerRecord.java rename to key.core/pipelineTests/records/expected/15_LocalClassTransformation/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/14_LocalClassTransformation/NotAllowed.java b/key.core/pipelineTests/records/expected/15_LocalClassTransformation/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_LocalClassTransformation/NotAllowed.java rename to key.core/pipelineTests/records/expected/15_LocalClassTransformation/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/14_LocalClassTransformation/Point3d.java b/key.core/pipelineTests/records/expected/15_LocalClassTransformation/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_LocalClassTransformation/Point3d.java rename to key.core/pipelineTests/records/expected/15_LocalClassTransformation/Point3d.java diff --git a/key.core/pipelineTests/records/expected/14_LocalClassTransformation/RecordOverwriting.java b/key.core/pipelineTests/records/expected/15_LocalClassTransformation/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_LocalClassTransformation/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/15_LocalClassTransformation/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/14_LocalClassTransformation/SimpleRecord.java b/key.core/pipelineTests/records/expected/15_LocalClassTransformation/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/14_LocalClassTransformation/SimpleRecord.java rename to key.core/pipelineTests/records/expected/15_LocalClassTransformation/SimpleRecord.java diff --git a/key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/CompactConstructor.java b/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/CompactConstructor.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/CompactConstructor.java rename to key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/CompactConstructor.java diff --git a/key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/InnerRecord.java b/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/InnerRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/InnerRecord.java rename to key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/InnerRecord.java diff --git a/key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/NotAllowed.java b/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/NotAllowed.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/NotAllowed.java rename to key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/NotAllowed.java diff --git a/key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/Point3d.java b/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/Point3d.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/Point3d.java rename to key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/Point3d.java diff --git a/key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/RecordOverwriting.java b/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/RecordOverwriting.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/RecordOverwriting.java rename to key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/RecordOverwriting.java diff --git a/key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/SimpleRecord.java b/key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/SimpleRecord.java similarity index 100% rename from key.core/pipelineTests/records/expected/15_ConstantStringExpressionEvaluator/SimpleRecord.java rename to key.core/pipelineTests/records/expected/16_ConstantStringExpressionEvaluator/SimpleRecord.java diff --git a/key.core/pipelineTests/simple/expected/02_EnumClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/02_MultiCatchReducer/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/02_EnumClassBuilder/Test.java rename to key.core/pipelineTests/simple/expected/02_MultiCatchReducer/Test.java diff --git a/key.core/pipelineTests/simple/expected/03_EnumClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/03_EnumClassBuilder/Test.java new file mode 100644 index 00000000000..dba29c488a0 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/03_EnumClassBuilder/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/04_RecordClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/04_RecordClassBuilder/Test.java new file mode 100644 index 00000000000..dba29c488a0 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/04_RecordClassBuilder/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/05_JMLTransformer/Test.java b/key.core/pipelineTests/simple/expected/05_JMLTransformer/Test.java new file mode 100644 index 00000000000..dba29c488a0 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/05_JMLTransformer/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/06_JmlDocRemoval/Test.java b/key.core/pipelineTests/simple/expected/06_JmlDocRemoval/Test.java new file mode 100644 index 00000000000..dba29c488a0 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/06_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/07_ImplicitFieldAdder/Test.java new file mode 100644 index 00000000000..e3c9d609b0d --- /dev/null +++ b/key.core/pipelineTests/simple/expected/07_ImplicitFieldAdder/Test.java @@ -0,0 +1,60 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; +} diff --git a/key.core/pipelineTests/simple/expected/08_InstanceAllocationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/08_InstanceAllocationMethodBuilder/Test.java new file mode 100644 index 00000000000..939c13da9ba --- /dev/null +++ b/key.core/pipelineTests/simple/expected/08_InstanceAllocationMethodBuilder/Test.java @@ -0,0 +1,64 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); +} diff --git a/key.core/pipelineTests/simple/expected/09_ConstructorNormalformBuilder/Test.java b/key.core/pipelineTests/simple/expected/09_ConstructorNormalformBuilder/Test.java new file mode 100644 index 00000000000..0fcacd6fef9 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/09_ConstructorNormalformBuilder/Test.java @@ -0,0 +1,100 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } +} diff --git a/key.core/pipelineTests/simple/expected/10_ClassPreparationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/10_ClassPreparationMethodBuilder/Test.java new file mode 100644 index 00000000000..825b89f91cf --- /dev/null +++ b/key.core/pipelineTests/simple/expected/10_ClassPreparationMethodBuilder/Test.java @@ -0,0 +1,106 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } +} diff --git a/key.core/pipelineTests/simple/expected/11_ClassInitializeMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/11_ClassInitializeMethodBuilder/Test.java new file mode 100644 index 00000000000..5d8570e373a --- /dev/null +++ b/key.core/pipelineTests/simple/expected/11_ClassInitializeMethodBuilder/Test.java @@ -0,0 +1,186 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + { + // should be resolved to 2 + abc = 1 + 1; + } + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(Test.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } +} diff --git a/key.core/pipelineTests/simple/expected/12_PrepareObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/12_PrepareObjectBuilder/Test.java new file mode 100644 index 00000000000..53a5436e9ab --- /dev/null +++ b/key.core/pipelineTests/simple/expected/12_PrepareObjectBuilder/Test.java @@ -0,0 +1,210 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + { + // should be resolved to 2 + abc = 1 + 1; + } + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(Test.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } +} diff --git a/key.core/pipelineTests/simple/expected/13_CreateBuilder/Test.java b/key.core/pipelineTests/simple/expected/13_CreateBuilder/Test.java new file mode 100644 index 00000000000..0116b540187 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/13_CreateBuilder/Test.java @@ -0,0 +1,224 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + { + // should be resolved to 2 + abc = 1 + 1; + } + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public Test $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(Test.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public SubClass $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } +} diff --git a/key.core/pipelineTests/simple/expected/14_CreateObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/14_CreateObjectBuilder/Test.java new file mode 100644 index 00000000000..44f496647fc --- /dev/null +++ b/key.core/pipelineTests/simple/expected/14_CreateObjectBuilder/Test.java @@ -0,0 +1,240 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + { + // should be resolved to 2 + abc = 1 + 1; + } + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public Test $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static Test $createObject() { + Test __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = Test.$allocate(); + __NEW__.$create()@Test + return __NEW__; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(Test.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public SubClass $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static SubClass $createObject() { + SubClass __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = SubClass.$allocate(); + __NEW__.$create()@SubClass + return __NEW__; + } +} diff --git a/key.core/pipelineTests/simple/expected/15_LocalClassTransformation/Test.java b/key.core/pipelineTests/simple/expected/15_LocalClassTransformation/Test.java new file mode 100644 index 00000000000..44f496647fc --- /dev/null +++ b/key.core/pipelineTests/simple/expected/15_LocalClassTransformation/Test.java @@ -0,0 +1,240 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + { + // should be resolved to 2 + abc = 1 + 1; + } + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public Test $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static Test $createObject() { + Test __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = Test.$allocate(); + __NEW__.$create()@Test + return __NEW__; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(Test.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public SubClass $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static SubClass $createObject() { + SubClass __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = SubClass.$allocate(); + __NEW__.$create()@SubClass + return __NEW__; + } +} diff --git a/key.core/pipelineTests/simple/expected/16_ConstantStringExpressionEvaluator/Test.java b/key.core/pipelineTests/simple/expected/16_ConstantStringExpressionEvaluator/Test.java new file mode 100644 index 00000000000..44f496647fc --- /dev/null +++ b/key.core/pipelineTests/simple/expected/16_ConstantStringExpressionEvaluator/Test.java @@ -0,0 +1,240 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + { + // should be resolved to 2 + abc = 1 + 1; + } + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public Test $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static Test $createObject() { + Test __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = Test.$allocate(); + __NEW__.$create()@Test + return __NEW__; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(Test.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public SubClass $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static SubClass $createObject() { + SubClass __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = SubClass.$allocate(); + __NEW__.$create()@SubClass + return __NEW__; + } +} 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 a5fd03e0dcd..98470bef204 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 @@ -39,6 +39,7 @@ public List getSteps() { public static KeYJavaPipeline createDefault(TransformationPipelineServices pipelineServices) { KeYJavaPipeline p = new KeYJavaPipeline(pipelineServices); p.add(new TextblockTransformer()); + p.add(new MultiCatchReducer()); 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/MultiCatchReducer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/MultiCatchReducer.java new file mode 100644 index 00000000000..db04fa85dd1 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/MultiCatchReducer.java @@ -0,0 +1,90 @@ +/* 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.ast.Modifier; +import com.github.javaparser.ast.body.TypeDeclaration; +import com.github.javaparser.ast.stmt.CatchClause; +import com.github.javaparser.ast.stmt.TryStmt; +import com.github.javaparser.ast.type.UnionType; + +/// Desugaring of Multi-Catch statements to multiple single catch statements. +/// ## Transformation Rules (per JLS 14.20) +/// ### Multi-Catch: +/// ```java +/// try { +/// body +/// } catch (ExceptionType1 | ExceptionType2 | ExceptionType3 e) { +/// handler +/// } +/// ``` +/// +/// becomes: +/// ```java +/// try { +/// body +/// } catch (final ExceptionType1 e) { +/// handler +/// } catch (final ExceptionType2 e) { +/// handler +/// } catch (final ExceptionType3 e) { +/// handler +/// } +/// ``` +/// +/// Important notes: +/// +/// - The exception variable `e` in a multi-catch is implicitly final. +/// - Each resulting catch clause gets its own copy of the handler body. +/// - The order of catch clauses follows the order of exception types in the union. +/// - Catch clause ordering must respect subtype relationships (more specific exceptions first). +/// +/// @author Alexander Weigl +/// @version 1 (12.07.26) +/// @see [JLS 14.20](https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.20) +public class MultiCatchReducer implements JavaTransformer { + @Override + public void apply(TypeDeclaration td) { + td.walk(TryStmt.class, this::rewrite); + } + + /** + * Rewrites a try statement with multi-catch clauses to use only single catch clauses. + * Each multi-catch clause is replaced by multiple single-type catch clauses. + */ + private void rewrite(TryStmt tryStmt) { + var catchClauses = tryStmt.getCatchClauses(); + var originalClauses = catchClauses.stream().toList(); + var insertAt = 0; + for (int i = 0; i < originalClauses.size(); i++) { + CatchClause catchClause = originalClauses.get(i); + var paramType = catchClause.getParameter().getType(); + if (paramType instanceof UnionType unionType) { + catchClauses.remove(catchClause); // delete original clause + + // Create individual catch clauses for each exception type in the union + for (var elementType : unionType.getElements()) { + CatchClause newCatchClause = new CatchClause(); + // Create a new parameter with the single exception type + var originalParam = catchClause.getParameter(); + var newParam = new com.github.javaparser.ast.body.Parameter( + elementType.clone(), + originalParam.getName().clone()); + + // Copy modifiers (the parameter is implicitly final in multi-catch) + newParam.addModifier(Modifier.DefaultKeyword.FINAL); + newCatchClause.setParameter(newParam); + + // Clone the body for each catch clause + newCatchClause.setBody(catchClause.getBody().clone()); + + // Insert after the current position (will be before due to reverse iteration) + catchClauses.add(insertAt++, newCatchClause); + } + } else { + insertAt++; + } + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/MultiCatchReducerTest.java b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/MultiCatchReducerTest.java new file mode 100644 index 00000000000..bcea982916f --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/MultiCatchReducerTest.java @@ -0,0 +1,278 @@ +/* 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; + +/** + * Tests for the {@link MultiCatchReducer} transformer. + * + * @author Alexander Weigl + * @version 1 (12.07.26) + */ +class MultiCatchReducerTest { + @Test + void testSimpleMultiCatch() { + String source = """ + class Demo { + void run() { + try { + doSomething(); + } catch (Exception1 | Exception2 e) { + System.out.println("caught: " + e); + } + } + void doSomething() throws Exception1, Exception2 {} + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var t = new MultiCatchReducer(); + t.apply(cu); + var actual = cu.toString(); + + var expected = """ + class Demo { + + void run() { + try { + doSomething(); + } catch (final Exception1 e) { + System.out.println("caught: " + e); + } catch (final Exception2 e) { + System.out.println("caught: " + e); + } + } + + void doSomething() throws Exception1, Exception2 { + } + } + """; + + assertThat(actual).isEqualToNormalizingWhitespace(expected); + } + + @Test + void testThreeExceptionTypes() { + String source = """ + class Demo { + void run() { + try { + doSomething(); + } catch (IOException | SQLException | RuntimeException e) { + handle(e); + } + } + void doSomething() throws IOException, SQLException, RuntimeException {} + void handle(Exception e) {} + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var t = new MultiCatchReducer(); + t.apply(cu); + var actual = cu.toString(); + + var expected = """ + class Demo { + + void run() { + try { + doSomething(); + } catch (final IOException e) { + handle(e); + } catch (final SQLException e) { + handle(e); + } catch (final RuntimeException e) { + handle(e); + } + } + + void doSomething() throws IOException, SQLException, RuntimeException { + } + + void handle(Exception e) { + } + } + """; + + assertThat(actual).isEqualToNormalizingWhitespace(expected); + } + + @Test + void testMixedSingleAndMultiCatch() { + String source = """ + class Demo { + void run() { + try { + doSomething(); + } catch (IllegalArgumentException e) { + log("illegal arg"); + } catch (IOException | SQLException e) { + log("io/sql error"); + } catch (RuntimeException e) { + throw e; + } + } + void doSomething() throws IOException, SQLException {} + void log(String s) {} + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var t = new MultiCatchReducer(); + t.apply(cu); + var actual = cu.toString(); + + var expected = """ + class Demo { + + void run() { + try { + doSomething(); + } catch (IllegalArgumentException e) { + log("illegal arg"); + } catch (final IOException e) { + log("io/sql error"); + } catch (final SQLException e) { + log("io/sql error"); + } catch (RuntimeException e) { + throw e; + } + } + + void doSomething() throws IOException, SQLException { + } + + void log(String s) { + } + } + """; + + assertThat(actual).isEqualToNormalizingWhitespace(expected); + } + + @Test + void testMultiCatchWithFinally() { + String source = """ + class Demo { + void run() { + try { + doSomething(); + } catch (Exception1 | Exception2 e) { + handle(e); + } finally { + cleanup(); + } + } + void doSomething() throws Exception1, Exception2 {} + void handle(Exception e) {} + void cleanup() {} + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var t = new MultiCatchReducer(); + t.apply(cu); + var actual = cu.toString(); + + var expected = """ + class Demo { + + void run() { + try { + doSomething(); + } catch (final Exception1 e) { + handle(e); + } catch (final Exception2 e) { + handle(e); + } finally { + cleanup(); + } + } + + void doSomething() throws Exception1, Exception2 { + } + + void handle(Exception e) { + } + + void cleanup() { + } + } + """; + + assertThat(actual).isEqualToNormalizingWhitespace(expected); + } + + @Test + void testNoMultiCatchUnchanged() { + String source = """ + class Demo { + void run() { + try { + doSomething(); + } catch (Exception e) { + handle(e); + } + } + void doSomething() throws Exception {} + void handle(Exception e) {} + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var original = cu.toString(); + var t = new MultiCatchReducer(); + t.apply(cu); + var actual = cu.toString(); + + // Should remain unchanged since there's no multi-catch + assertThat(actual).isEqualToNormalizingWhitespace(original); + } + + @Test + void testMultiMultiCatch() { + String source = """ + class Demo { + int f() { + try { m(); } + catch (IllegalArgumentException | NullPointerException e) { return 1; } + catch (ArithmeticException | ArrayStoreException e) { return 2; } + return 0; + } + } + """; + + CompilationUnit cu = StaticJavaParser.parse(source); + var original = cu.toString(); + var t = new MultiCatchReducer(); + t.apply(cu); + var actual = cu.toString(); + + // Should remain unchanged since there's no multi-catch + assertThat(actual).isEqualToNormalizingWhitespace(""" + class Demo { + int f() { + try { + m(); + } catch (final IllegalArgumentException e) { + return 1; + } catch (final NullPointerException e) { + return 1; + } catch (final ArithmeticException e) { + return 2; + } catch (final ArrayStoreException e) { + return 2; + } + return 0; + } + } + """); + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/multi-catch/MultiCatch.java b/key.core/src/test/resources/de/uka/ilkd/key/java/coverage/supported/multi-catch/MultiCatch.java similarity index 100% rename from key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/multi-catch/MultiCatch.java rename to key.core/src/test/resources/de/uka/ilkd/key/java/coverage/supported/multi-catch/MultiCatch.java diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/multi-catch/problem.key b/key.core/src/test/resources/de/uka/ilkd/key/java/coverage/supported/multi-catch/problem.key similarity index 100% rename from key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/multi-catch/problem.key rename to key.core/src/test/resources/de/uka/ilkd/key/java/coverage/supported/multi-catch/problem.key diff --git a/key.ui/examples/Java/MultiCatch/MultiCatch.java b/key.ui/examples/Java/MultiCatch/MultiCatch.java new file mode 100644 index 00000000000..5078d3817b1 --- /dev/null +++ b/key.ui/examples/Java/MultiCatch/MultiCatch.java @@ -0,0 +1,49 @@ +public final class MultiCatch { + /*@ ensures true; requires true; */ + public void m() throws Exception { + // Simple multi-catch with two exception types + try { + doSomethingRisky(); + } catch (ArrayIndexOutOfBoundsException | AssertionError e) { + System.out.println("Caught exception: " + e); + } + + // Multi-catch with three exception types + try { + doAnotherRiskyThing(); + } catch (IllegalArgumentException | IndexOutOfBoundsException | InterruptedException e) { + handleError(e); + } + + // Mixed single and multi-catch + try { + doComplexOperation(); + } catch (NullPointerException e) { + System.out.println("Null pointer!"); + } catch (IndexOutOfBoundsException | IllegalArgumentException e) { + System.out.println("Illegal state or argument"); + } catch (Exception e) { + System.out.println("Other exception"); + } + } + + /*@ ensures true; requires true; */ + private void doSomethingRisky() throws ArrayIndexOutOfBoundsException, AssertionError { + // might throw + } + + /*@ ensures true; requires true; */ + private void doAnotherRiskyThing() throws IllegalArgumentException, IndexOutOfBoundsException, InterruptedException { + // might throw + } + + /*@ ensures true; requires true; */ + private void doComplexOperation() throws NullPointerException, IndexOutOfBoundsException, IllegalArgumentException, Exception { + // might throw + } + + /*@ ensures true; requires true; */ + private void handleError(Exception e) { + // handle error + } +} \ No newline at end of file diff --git a/key.ui/examples/Java/MultiCatch/README.txt b/key.ui/examples/Java/MultiCatch/README.txt new file mode 100644 index 00000000000..4e9992cf6b5 --- /dev/null +++ b/key.ui/examples/Java/MultiCatch/README.txt @@ -0,0 +1,8 @@ +example.name = Multi Catch +example.path = Java 25 +example.file = project.key +example.additionalFile.1 = MultiCatch.java + +Multi-Catch statements are supported in KeY. They are reduced to multiple single catch clauses. + +The proof obligation is verifiable without user interaction. \ No newline at end of file diff --git a/key.ui/examples/Java/MultiCatch/project.key b/key.ui/examples/Java/MultiCatch/project.key new file mode 100644 index 00000000000..31e0c2215d5 --- /dev/null +++ b/key.ui/examples/Java/MultiCatch/project.key @@ -0,0 +1,8 @@ +\profile "Java Profile"; +\javaSource "."; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "MultiCatch[MultiCatch::m()].JML operation contract.0", + "name" : "MultiCatch[MultiCatch::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 74c05fa1718..7bb98991042 100644 --- a/key.ui/examples/index/samplesIndex.txt +++ b/key.ui/examples/index/samplesIndex.txt @@ -21,11 +21,11 @@ firstTouch/10-SITA/README.txt firstTouch/11-StateMerging/README.txt # Java Features +Java/MultiCatch/README.txt Java/Records/README.txt Java/Records+CompactConstructor/README.txt Java/TextBlockLiterals/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 newBook/Using_KeY/Building_Propositional_Proofs/README.txt