Migrate to JMLtk

build.gradle

@@ -76,7 +76,7 @@ subprojects {
     repositories {
         mavenCentral()
         //maven { url = "https://git.key-project.org/api/v4/projects/35/packages/maven/" }
-        //maven { url = "https://central.sonatype.com/repository/maven-snapshots/" }
+        maven { url = "https://central.sonatype.com/repository/maven-snapshots/" }
     }
 
     dependencies {

gradle/libs.versions.toml

@@ -23,7 +23,7 @@ stringtemplate = "4.3.4"
 
 # Java parsing and analysis
 javapoet = "1.13.0"
-javaparser = "3.28.0-K13.6"
+javaparser = "3.28.2-J8.0-K13.5-SNAPSHOT"
 truth = "1.4.5"
 
 # UI and CLI
@@ -67,9 +67,9 @@ stringtemplate = { module = "org.antlr:ST4", version.ref = "stringtemplate" }
 
 # Java source code processing
 javapoet = { module = "com.squareup:javapoet", version.ref = "javapoet" }
-javaparser-core = { module = "org.key-project.proofjava:javaparser-core", version.ref = "javaparser" }
-javaparser-core-serialization = { module = "org.key-project.proofjava:javaparser-core-serialization", version.ref = "javaparser" }
-javaparser-symbol-solver-core = { module = "org.key-project.proofjava:javaparser-symbol-solver-core", version.ref = "javaparser" }
+javaparser-core = { module = "io.github.jmltoolkit:jmlparser-core", version.ref = "javaparser" }
+javaparser-core-serialization = { module = "io.github.jmltoolkit:jmlparser-core-serialization", version.ref = "javaparser" }
+javaparser-symbol-solver-core = { module = "io.github.jmltoolkit:jmlparser-symbol-solver-core", version.ref = "javaparser" }
 
 # Testing utilities
 truth = { module = "com.google.truth:truth", version.ref = "truth" }

key.core/pipelineTests/innerclass/expected/08_ImplicitFieldAdder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
     }
 
     @javax.annotation.processing.Generated()
@@ -34,8 +34,8 @@ public static class MyInnerClass {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 }

key.core/pipelineTests/innerclass/expected/09_InstanceAllocationMethodBuilder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
     }
@@ -36,10 +36,10 @@ public static class MyInnerClass {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 }

key.core/pipelineTests/innerclass/expected/10_ConstructorNormalformBuilder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -44,10 +44,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

key.core/pipelineTests/innerclass/expected/11_ClassPreparationMethodBuilder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -47,10 +47,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

key.core/pipelineTests/innerclass/expected/12_ClassInitializeMethodBuilder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -85,10 +85,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

key.core/pipelineTests/innerclass/expected/13_PrepareObjectBuilder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -93,10 +93,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

key.core/pipelineTests/innerclass/expected/14_CreateBuilder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -100,10 +100,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

key.core/pipelineTests/innerclass/expected/15_CreateObjectBuilder/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -108,10 +108,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

key.core/pipelineTests/innerclass/expected/16_LocalClassTransformation/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -108,10 +108,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

key.core/pipelineTests/innerclass/expected/17_ConstantStringExpressionEvaluator/MostSimpleInner.java

@@ -15,10 +15,10 @@ public static class MyInnerClass {
         static private boolean $classPrepared;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv;
+        static public /*@ model */ boolean $staticInv;
 
         @javax.annotation.processing.Generated()
-        static public model boolean $staticInv_free;
+        static public /*@ model */ boolean $staticInv_free;
 
         public static MyInnerClass $allocate();
 
@@ -108,10 +108,10 @@ public MyInnerClass() {
     static private boolean $classPrepared;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv;
+    static public /*@ model */ boolean $staticInv;
 
     @javax.annotation.processing.Generated()
-    static public model boolean $staticInv_free;
+    static public /*@ model */ boolean $staticInv_free;
 
     public static MostSimpleInner $allocate();
 

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

@@ -1,3 +1,6 @@
+//@ /*@ nullable */
+
+
 record MyRecord(String test) {
 
     public int hashCode() {

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

@@ -1,4 +1,4 @@
-public record SimpleRecord(/*@ nullable */ String name) implements Serializable {
+public record SimpleRecord([[JML modifiers]] String name) implements Serializable {
 
     SimpleRecord(String name) {
         this.name = name;

key.core/pipelineTests/records/expected/02_MultiCatchReducer/RecordOverwriting.java

@@ -1,3 +1,6 @@
+//@ /*@ nullable */
+
+
 record MyRecord(String test) {
 
     public int hashCode() {

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

@@ -1,4 +1,4 @@
-public record SimpleRecord(/*@ nullable */ String name) implements Serializable {
+public record SimpleRecord([[JML modifiers]] String name) implements Serializable {
 
     SimpleRecord(String name) {
         this.name = name;

key.core/pipelineTests/records/expected/03_TryWithResourceReducer/RecordOverwriting.java

@@ -1,3 +1,6 @@
+//@ /*@ nullable */
+
+
 record MyRecord(String test) {
 
     public int hashCode() {

key.core/pipelineTests/records/expected/03_TryWithResourceReducer/SimpleRecord.java

@@ -1,4 +1,4 @@
-public record SimpleRecord(/*@ nullable */ String name) implements Serializable {
+public record SimpleRecord([[JML modifiers]] String name) implements Serializable {
 
     SimpleRecord(String name) {
         this.name = name;

key.core/pipelineTests/records/expected/04_EnumClassBuilder/RecordOverwriting.java

@@ -1,3 +1,6 @@
+//@ /*@ nullable */
+
+
 record MyRecord(String test) {
 
     public int hashCode() {

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

@@ -1,4 +1,4 @@
-public record SimpleRecord(/*@ nullable */ String name) implements Serializable {
+public record SimpleRecord([[JML modifiers]] String name) implements Serializable {
 
     SimpleRecord(String name) {
         this.name = name;

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

@@ -60,7 +60,7 @@ public Mapping(String from, String to) {
 
     @Override()
     @javax.annotation.processing.Generated("RecordClassBuilder")
-    public final non_null String toString() {
+    public final /*@ non_null */ String toString() {
         return "Mapping[" + "from=" + from + "," + "to=" + to + "]";
     }
 }

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

@@ -49,7 +49,7 @@ public MyRecord(String test) {
 
         @Override()
         @javax.annotation.processing.Generated("RecordClassBuilder")
-        public final non_null String toString() {
+        public final /*@ non_null */ String toString() {
             return "MyRecord[" + "test=" + test + "]";
         }
     }

key.core/pipelineTests/records/expected/05_RecordClassBuilder/NotAllowed.java

@@ -46,7 +46,7 @@ private Name(String name) {
 
     @Override()
     @javax.annotation.processing.Generated("RecordClassBuilder")
-    public final non_null String toString() {
+    public final /*@ non_null */ String toString() {
         return "Name[" + "name=" + name + "]";
     }
 
@@ -121,7 +121,7 @@ public final int y() {
 
     @Override()
     @javax.annotation.processing.Generated("RecordClassBuilder")
-    public final non_null String toString() {
+    public final /*@ non_null */ String toString() {
         return "Point[" + "x=" + x + "," + "y=" + y + "]";
     }
 

key.core/pipelineTests/records/expected/05_RecordClassBuilder/Point3d.java

@@ -65,7 +65,7 @@ public Point3d(int x, int y, int z) {
 
     @Override()
     @javax.annotation.processing.Generated("RecordClassBuilder")
-    public final non_null String toString() {
+    public final /*@ non_null */ String toString() {
         return "Point3d[" + "x=" + x + "," + "y=" + y + "," + "z=" + z + "]";
     }
 }