Merge branch 'weigl/key-javaparser3' of github.com:KeYProject/key into weigl/key-javaparser3

Author: flo2702

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java

@@ -387,7 +387,7 @@ private Statement transformSetStatement(TextualJMLSetStatement stat) {
         // TODO javaparser error handling!
         NodeList<Statement> stmtList = result.getResult().orElseThrow().getStatements();
         assert stmtList.size() == 1;
-        Statement assignStmt = stmtList.get(0);
+        Statement assignStmt = stmtList.getFirst();
         shiftPosition(assignStmt, location.getPosition());
         // updatePositionInformation(assignStmt, pos);
         return assignStmt;

key.ui/examples/heap/SmansEtAl/ArrayList_footprint.key

@@ -34,4 +34,4 @@
 
 \javaSource "src";
 
-\chooseContract "ArrayList[ArrayList::$footprint()].JML accessible clause.0";
+\chooseContract "ArrayList[ArrayList::#footprint()].JML accessible clause.0";

key.ui/examples/heap/SmansEtAl/Cell_footprint.key

@@ -34,4 +34,4 @@
 
 \javaSource "src";
 
-\chooseContract "Cell[Cell::$footprint()].JML accessible clause.0";
+\chooseContract "Cell[Cell::#footprint()].JML accessible clause.0";

key.ui/examples/heap/SmansEtAl/Iterator_footprint.key

@@ -34,4 +34,4 @@
 
 \javaSource "src";
 
-\chooseContract "Iterator[Iterator::$footprint()].JML accessible clause.0";
+\chooseContract "Iterator[Iterator::#footprint()].JML accessible clause.0";

key.ui/examples/heap/SmansEtAl/Stack_footprint.key

@@ -34,4 +34,4 @@
 
 \javaSource "src";
 
-\chooseContract "Stack[Stack::$footprint()].JML accessible clause.0";
+\chooseContract "Stack[Stack::#footprint()].JML accessible clause.0";

key.ui/examples/heap/fm12_01_LRS/SuffixArray.java

@@ -66,7 +66,7 @@ private int compare(int x, int y) {
 
 
 
-    private void /*@ helper @*/ sort(final int[] data) {
+    private /*@ helper @*/ void sort(final int[] data) {
         /*@ maintaining data.length == a.length;
           @ maintaining 0 <= k && k <= data.length;
           @ maintaining (\forall int i; 0 <= i && i < a.length;
@@ -77,7 +77,7 @@ private int compare(int x, int y) {
           @ decreasing data.length - k;
           @ assignable data[*];
           @*/
-        for(int k = 0; k < data.length; k++)
+        for(int k = 0; k < data.length; k++) {
             /*@ maintaining 0 <= l && l <= k;
               @ maintaining (\forall int i; l < i && i <= k;
               @                 compare(data[i],data[i-1]) > 0);
@@ -87,8 +87,9 @@ private int compare(int x, int y) {
               @ decreasing l;
               @ assignable data[*];
               @*/
-            for(int l = k; l > 0 && compare(data[l - 1], data[l]) > 0; l--)
+            for (int l = k; l > 0 && compare(data[l - 1], data[l]) > 0; l--)
                 swap(data, l);
+        }
     }
 
     /*@ normal_behavior
@@ -97,7 +98,7 @@ private int compare(int x, int y) {
       @ ensures data[x-1] == \old(data[x]);
       @ assignable data[x], data[x-1];
       @*/
-    private static void /*@ helper @*/ swap(int[] data, int x) {
+    private static /*@ helper @*/ void swap(int[] data, int x) {
         final int y = x-1;
         final int t = data[x];
         data[x] = data[y];