Recovering the overflow proofs

Squashed commit of the following:

commit ee2d765
Author: Mattias Ulbrich <ulbrich@kit.edu>
Date:   Sat Oct 28 02:25:58 2023 +0200

    deactivate overflow constructors for the moment

commit b55e386
Author: Mattias Ulbrich <ulbrich@kit.edu>
Date:   Sat Oct 28 01:59:10 2023 +0200

    Proof for Permute::swap

commit d5d4eb3
Author: Mattias Ulbrich <ulbrich@kit.edu>
Date:   Sat Oct 28 01:14:52 2023 +0200

    Proof for overflow of Permute::permute

commit bcc1319
Author: Mattias Ulbrich <ulbrich@kit.edu>
Date:   Fri Oct 27 23:54:48 2023 +0200

    overflow proof for Cleanup::cleanup

commit 2ca9e6a
Author: Mattias Ulbrich <ulbrich@kit.edu>
Date:   Fri Oct 27 20:27:57 2023 +0200

    Revert "reduced github checks"

    This reverts commit 164fe35.

.github/workflows/tests.yml

@@ -25,8 +25,8 @@ jobs:
             fail-fast: false
             matrix:
                 # target: [ check-overflow-methods, check-overflow-constructors, check-methods, check-constructors ]
-                #   Reduce checks until overflow is fixed
-                target: [ check-methods, check-constructors ]
+                target: [ check-overflow-methods, check-methods, check-constructors ]
+
         runs-on: ubuntu-latest
         env:
             GH_TOKEN: ${{ github.token }}

Makefile

@@ -14,6 +14,11 @@ proofSettings:
 	mkdir -p $${HOME}/.key
 	cp proofIndependentSettings.props $${HOME}/.key
 
+overflow-run:
+	@echo Consider loading one of the following files:
+	@find -iname "project*.key"
+	java -Dkey.contractOrder="contract-order.txt" -jar $(KEY_OVERFLOW_JAR)
+
 run:
 	@echo Consider loading one of the following files:
 	@find -iname "project*.key"

contracts/ignore.txt

@@ -1,4 +1,4 @@
-# block contracts
+# block contracts are proved inline and need not be proved explicitly
 de.wiesler.BucketPointers[de.wiesler.BucketPointers::<init>([I,int,int,[I)].JML normal_behavior block contract.0
 de.wiesler.BucketPointers[de.wiesler.BucketPointers::<init>([I,int,int,[I)].JML normal_behavior block contract.1
 de.wiesler.BucketPointers[de.wiesler.BucketPointers::<init>([I,int,int,[I)].JML normal_behavior block contract.2