sync code of cleanup method (overflow) with non-overflow version, fix…

… proof
KeYProject · Oct 27, 2023 · 4d525c7 · 4d525c7
1 parent 164fe35
commit 4d525c7
Show file tree

Hide file tree

Showing 2 changed files with 47,016 additions and 32,846 deletions.
diff --git a/src/main/java-overflow/de/wiesler/Cleanup.java b/src/main/java-overflow/de/wiesler/Cleanup.java
@@ -320,7 +320,16 @@ public static void cleanup(
               @
               @ assignable_free values[start..stop - 1];
               @*/
-            {}
+            {
+                if (stop - start <= Constants.ACTUAL_BASE_CASE_SIZE || is_last_level) {
+                    //@ ghost \seq bucketValuesBeforeSort = \dl_seq_def_workaround(start, stop, values);
+                    // seqPerm(seq, seq2)
+                    // forall i in seq2; f(i) ==> forall i in seq; f(i)
+                    Sorter.fallback_sort(values, start, stop);
+                    //@ ghost \seq bucketValuesAfterSort = \dl_seq_def_workaround(start, stop, values);
+                    //@ assert (\forall int i; 0 <= i < bucketValuesAfterSort.length; classifier.classOf((int)bucketValuesAfterSort[i]) == bucket);
+                }
+            }
 
             /*@ assume \invariant_for(classifier) && \invariant_for(bucket_pointers) && \invariant_for(buffers) &&
               @     Functions.countElementSplit(values, begin, begin + \old(bucket_starts[bucket]), begin + \old(bucket_starts[bucket + 1])) &&