Record support by transformation

key.core/pipelineTests/innerclass/expected/05_JmlDocRemoval/MostSimpleInner.java

@@ -0,0 +1,5 @@
+public class MostSimpleInner {
+
+    public static class MyInnerClass {
+    }
+}

key.core/pipelineTests/records/expected/01_TextblockTransformer/CompactConstructor.java

@@ -0,0 +1,8 @@
+record Mapping(String from, String to) {
+
+    Mapping {
+        // compact constructor!
+        from = "abc";
+        to = "def";
+    }
+}

key.core/pipelineTests/records/expected/01_TextblockTransformer/InnerRecord.java

@@ -0,0 +1,7 @@
+import java.lang.Object;
+
+public class OuterClass {
+
+    final record MyRecord(String test) {
+    }
+}

key.core/pipelineTests/records/expected/01_TextblockTransformer/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'
+    }
+}

key.core/pipelineTests/records/expected/01_TextblockTransformer/Point3d.java

@@ -0,0 +1,2 @@
+record Point3d(int x, int y, int z) {
+}

key.core/pipelineTests/records/expected/01_TextblockTransformer/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 "";
+    }
+}

key.core/pipelineTests/records/expected/01_TextblockTransformer/SimpleRecord.java

@@ -0,0 +1,6 @@
+public record SimpleRecord(/*@ nullable */ String name) implements Serializable {
+
+    SimpleRecord(String name) {
+        this.name = name;
+    }
+}

key.core/pipelineTests/records/expected/02_EnumClassBuilder/CompactConstructor.java

@@ -0,0 +1,8 @@
+record Mapping(String from, String to) {
+
+    Mapping {
+        // compact constructor!
+        from = "abc";
+        to = "def";
+    }
+}

key.core/pipelineTests/records/expected/02_EnumClassBuilder/InnerRecord.java

@@ -0,0 +1,7 @@
+import java.lang.Object;
+
+public class OuterClass {
+
+    final record MyRecord(String test) {
+    }
+}

key.core/pipelineTests/records/expected/02_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'
+    }
+}

key.core/pipelineTests/records/expected/02_EnumClassBuilder/Point3d.java

@@ -0,0 +1,2 @@
+record Point3d(int x, int y, int z) {
+}

key.core/pipelineTests/records/expected/02_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 "";
+    }
+}

key.core/pipelineTests/records/expected/02_EnumClassBuilder/SimpleRecord.java

@@ -0,0 +1,6 @@
+public record SimpleRecord(/*@ nullable */ String name) implements Serializable {
+
+    SimpleRecord(String name) {
+        this.name = name;
+    }
+}

key.core/pipelineTests/records/expected/03_RecordClassBuilder/CompactConstructor.java

@@ -0,0 +1,72 @@
+@javax.annotation.processing.Generated("RecordClassBuilder")
+final class Mapping extends Record {
+
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    private final String from;
+
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    public final String from() {
+        return from;
+    }
+
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    private final String to;
+
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    public final String to() {
+        return to;
+    }
+
+    /*@ public  normal_behavior 
+      @ requires true;
+      @ ensures from == this.from && to == this.to;
+      @ assignable this.*;
+
+      @*/
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    public Mapping(String from, String to) {
+        {
+            // compact constructor!
+            from = "abc";
+            to = "def";
+        }
+        //Created by RecordClassBuilder.java:131
+        this.from = from;
+        //Created by RecordClassBuilder.java:131
+        this.to = to;
+    }
+
+    /*@ public  normal_behavior 
+      @ requires true;
+      @ ensures ((this == o) || (o instanceof Mapping && o == null && this.from == ((Mapping) o).from && this.to == ((Mapping) o).to) || (o instanceof Mapping && o == null && (this.from == null? (this.from.equals(((Mapping) o).from)) : (o.from == null)) && (this.to == null? (this.to.equals(((Mapping) o).to)) : (o.to == null))))<==>\result;
+      @ ensures hashCode() == o.hashCode() ==> !\result;
+      @ ensures o == null ==> !\result;
+      @ assignable \strictly_nothing;
+
+      @*/
+    @Override()
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    public final boolean equals(java.lang.Object o);
+
+    /*@ public  normal_behavior 
+      @ ensures true;
+      @ requires true;
+      @ assignable \strictly_nothing;
+
+      @*/
+    @Override()
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    public final int hashCode();
+
+    @Override()
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    public final non_null String toString() {
+        return "Mapping[" + "from=" + from + "," + "to=" + to + "]";
+    }
+
+    Mapping {
+        // compact constructor!
+        from = "abc";
+        to = "def";
+    }
+}

key.core/pipelineTests/records/expected/03_RecordClassBuilder/InnerRecord.java

@@ -0,0 +1,56 @@
+import java.lang.Object;
+
+public class OuterClass {
+
+    @javax.annotation.processing.Generated("RecordClassBuilder")
+    final class MyRecord extends Record {
+
+        @javax.annotation.processing.Generated("RecordClassBuilder")
+        private final String test;
+
+        @javax.annotation.processing.Generated("RecordClassBuilder")
+        public final String test() {
+            return test;
+        }
+
+        /*@ public  normal_behavior 
+          @ requires true;
+          @ ensures test == this.test;
+          @ assignable this.*;
+
+          @*/
+        @javax.annotation.processing.Generated("RecordClassBuilder")
+        public MyRecord(String test) {
+            //Created by RecordClassBuilder.java:131
+            this.test = test;
+        }
+
+        /*@ public  normal_behavior 
+          @ requires true;
+          @ ensures ((this == o) || (o instanceof MyRecord && o == null && this.test == ((MyRecord) o).test) || (o instanceof MyRecord && o == null && (this.test == null? (this.test.equals(((MyRecord) o).test)) : (o.test == null))))<==>\result;
+          @ ensures hashCode() == o.hashCode() ==> !\result;
+          @ ensures o == null ==> !\result;
+          @ assignable \strictly_nothing;
+
+          @*/
+        @Override()
+        @javax.annotation.processing.Generated("RecordClassBuilder")
+        public final boolean equals(java.lang.Object o);
+
+        /*@ public  normal_behavior 
+          @ ensures true;
+          @ requires true;
+          @ assignable \strictly_nothing;
+
+          @*/
+        @Override()
+        @javax.annotation.processing.Generated("RecordClassBuilder")
+        public final int hashCode();
+
+        @Override()
+        @javax.annotation.processing.Generated("RecordClassBuilder")
+        public final non_null String toString() {
+            return "MyRecord[" + "test=" + test + "]";
+        }
+    }
+}