From 43c7f9a165e05b3e3506bb30a5ef57495e7c719e Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 09:58:37 +0100
Subject: [PATCH 01/38] splits workflow into multiple jobs

---
 .github/workflows/test.yml | 132 +++++++++++++++++++++++++++----------
 1 file changed, 96 insertions(+), 36 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 5a01f5fd9..f2b5496a3 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -10,9 +10,15 @@ on:
   push: # run this workflow on every push
   pull_request: # run this workflow on every pull_request
 
+env:
+  BUILD_IMAGE_WORKFLOW_ARTIFACT_NAME: gobra-build-image
+  BUILD_IMAGE_FILENAME: build-image.tar
+  FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME: gobra-final-image
+  FINAL_IMAGE_FILENAME: final-image.tar
+
+
 jobs:
-  # there is a single job to avoid copying the built docker image from one job to the other
-  build-test-deploy-container:
+  build-container:
     runs-on: ubuntu-latest
     env:
       IMAGE_ID: ghcr.io/${{ github.repository_owner }}/gobra
@@ -24,13 +30,6 @@ jobs:
         org.opencontainers.image.revision=${{ github.sha }}
         org.opencontainers.image.licenses=MPL-2.0
         org.opencontainers.image.description=Gobra image for revision ${{ github.sha }} built by workflow run ${{ github.run_id }}
-      CONCLUSION_SUCCESS: "success"
-      CONCLUSION_FAILURE: "failure"
-      # Output levels according to severity.
-      # They identify the kinds of annotations to be printed by Github.
-      NOTICE_LEVEL: "info"
-      WARNING_LEVEL: "warning"
-      FAILURE_LEVEL: "error"
     steps:
       - name: Checkout Gobra
         uses: actions/checkout@v6
@@ -89,6 +88,62 @@ jobs:
           # use GitHub cache:
           cache-from: type=gha, scope=${{ github.workflow }}
           cache-to: type=gha, scope=${{ github.workflow }}
+          outputs: type=docker,dest=/tmp/${{ env.BUILD_IMAGE_FILENAME }}
+
+      - name: Upload build image
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ env.BUILD_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp/${{ env.BUILD_IMAGE_FILENAME }}
+          retention-days: 1
+
+      - name: Build entire image
+        uses: docker/build-push-action@v6
+        with:
+          context: .
+          load: true # make the built image available in docker (locally)
+          file: workflow-container/Dockerfile
+          tags: ${{ steps.image-metadata.outputs.tags }}
+          labels: ${{ steps.image-metadata.outputs.labels }}
+          push: false
+          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
+          # use GitHub cache:
+          cache-from: type=gha, scope=${{ github.workflow }}
+          cache-to: type=gha, scope=${{ github.workflow }}
+          outputs: type=docker,dest=/tmp/${{ env.FINAL_IMAGE_FILENAME }}
+
+      - name: Upload final image
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ env.FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp/${{ env.FINAL_IMAGE_FILENAME }}
+          retention-days: 1
+
+      - name: Set job output
+        id: output_step
+        run: echo "IMAGE_TAG=${{ steps.image-metadata.outputs.tags }}" >> $GITHUB_OUTPUT
+
+
+  run-all-tests:
+    runs-on: ubuntu-latest
+    needs: build-container
+    env:
+      CONCLUSION_SUCCESS: "success"
+      CONCLUSION_FAILURE: "failure"
+      # Output levels according to severity.
+      # They identify the kinds of annotations to be printed by Github.
+      NOTICE_LEVEL: "info"
+      WARNING_LEVEL: "warning"
+      FAILURE_LEVEL: "error"
+    steps:
+      - name: Download build image
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ env.BUILD_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp
+
+      - name: Load image
+        run: docker load --input /tmp/${{ env.BUILD_IMAGE_FILENAME }}
 
       - name: Execute all tests
         run: |
@@ -96,7 +151,7 @@ jobs:
           mkdir -p $PWD/sync
           docker run \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
-            ${{ env.IMAGE_TAG }} \
+            ${{ needs.build-container.outputs.IMAGE_TAG }} \
             /bin/sh -c "$(cat .github/test-and-measure-ram.sh)"
 
       - name: Get max RAM usage by Java and Z3
@@ -190,26 +245,31 @@ jobs:
           name: pidstat.txt
           path: sync/pidstat.txt
 
-      - name: Build entire image
-        uses: docker/build-push-action@v6
+
+  test-final-container:
+    runs-on: ubuntu-latest
+    needs: build-container
+    steps:
+      - name: Download final image
+        uses: actions/download-artifact@v4
         with:
-          context: .
-          load: true # make the built image available in docker (locally)
-          file: workflow-container/Dockerfile
-          tags: ${{ steps.image-metadata.outputs.tags }}
-          labels: ${{ steps.image-metadata.outputs.labels }}
-          push: false
-          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
-          # use GitHub cache:
-          cache-from: type=gha, scope=${{ github.workflow }}
-          cache-to: type=gha, scope=${{ github.workflow }}
+          name: ${{ env.FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp
+
+      - name: Load image
+        run: docker load --input /tmp/${{ env.FINAL_IMAGE_FILENAME }}
 
       - name: Test final container by verifying a file
         run: |
           docker run \
-            ${{ env.IMAGE_TAG }} \
+            ${{ needs.build-container.outputs.IMAGE_TAG }} \
             -i tutorial-examples/basic-annotations.gobra
 
+
+  deploy-container:
+    runs-on: ubuntu-latest
+    needs: [build-container, run-all-tests, test-final-container]
+    steps:
       - name: Decide whether image should be deployed or not
         run: |
           # note that these GitHub expressions return the value '1' for 'true' (as opposed to bash)
@@ -226,6 +286,17 @@ jobs:
           fi
           echo "SHOULD_DEPLOY=$SHOULD_DEPLOY" >> $GITHUB_ENV
 
+      - name: Download final image
+        if: env.SHOULD_DEPLOY == 'true'
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ env.FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp
+
+      - name: Load image
+        if: env.SHOULD_DEPLOY == 'true'
+        run: docker load --input /tmp/${{ env.FINAL_IMAGE_FILENAME }}
+
       - name: Login to Github Packages
         if: env.SHOULD_DEPLOY == 'true'
         uses: docker/login-action@v3
@@ -234,16 +305,5 @@ jobs:
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
-      - name: Push entire image
-        if: env.SHOULD_DEPLOY == 'true'
-        uses: docker/build-push-action@v6
-        with:
-          context: .
-          file: workflow-container/Dockerfile
-          tags: ${{ steps.image-metadata.outputs.tags }}
-          labels: ${{ steps.image-metadata.outputs.labels }}
-          push: true
-          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
-          # use GitHub cache:
-          cache-from: type=gha, scope=${{ github.workflow }}
-          cache-to: type=gha, scope=${{ github.workflow }}
+      - name: Push image
+        run: docker push ${{ needs.build-container.outputs.IMAGE_TAG }}

From 00b6c4f4f6b04c1ab67e73757b585af49fdbc777 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 10:08:44 +0100
Subject: [PATCH 02/38] fixes IMAGE_TAG to be a single one instead of a
 newline-separated list of tags

---
 .github/workflows/test.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index f2b5496a3..37b6c8197 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -69,9 +69,6 @@ jobs:
             # use latest tag for default branch and with highest priority (1000 is the highest default priority for the other types):
             type=raw,value=latest,priority=1100,enable={{is_default_branch}}
 
-      - name: Get first tag
-        run: echo "IMAGE_TAG=$(echo "${{ steps.image-metadata.outputs.tags }}" | head -1)" >> $GITHUB_ENV
-
       - name: Build image up to including stage 'build'
         id: image-build
         # note that the action's name is misleading: this step does NOT push
@@ -119,9 +116,12 @@ jobs:
           path: /tmp/${{ env.FINAL_IMAGE_FILENAME }}
           retention-days: 1
 
+      - name: Get first tag
+        run: echo "IMAGE_TAG=$(echo "${{ steps.image-metadata.outputs.tags }}" | head -1)" >> $GITHUB_ENV
+
       - name: Set job output
         id: output_step
-        run: echo "IMAGE_TAG=${{ steps.image-metadata.outputs.tags }}" >> $GITHUB_OUTPUT
+        run: echo "IMAGE_TAG=${{ env.IMAGE_TAG }}" >> $GITHUB_OUTPUT
 
 
   run-all-tests:

From 9b249c1777f38798b9d65c877d6fd02fb587c104 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 10:14:21 +0100
Subject: [PATCH 03/38] fixes propagation of IMAGE_TAG to later jobs in CI
 workflow

---
 .github/workflows/test.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 37b6c8197..1bdf69194 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -20,6 +20,8 @@ env:
 jobs:
   build-container:
     runs-on: ubuntu-latest
+    outputs:
+      IMAGE_TAG: ${{ steps.output_step.outputs.IMAGE_TAG }}
     env:
       IMAGE_ID: ghcr.io/${{ github.repository_owner }}/gobra
       # image labels are new-line separated key value pairs (according to https://specs.opencontainers.org/image-spec/annotations/):

From 740b0a8de074871a048d9ce2f1abf02bc16f3338 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 10:22:31 +0100
Subject: [PATCH 04/38] fixes execution of tests in CI

---
 .github/workflows/test.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 1bdf69194..16d5108e8 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -138,6 +138,10 @@ jobs:
       WARNING_LEVEL: "warning"
       FAILURE_LEVEL: "error"
     steps:
+      # we only need .github/test-and-measure-ram.sh. Thus, we do not checkout the submodules
+      - name: Checkout Gobra
+        uses: actions/checkout@v4
+
       - name: Download build image
         uses: actions/download-artifact@v4
         with:
@@ -308,4 +312,5 @@ jobs:
           password: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Push image
+        if: env.SHOULD_DEPLOY == 'true'
         run: docker push ${{ needs.build-container.outputs.IMAGE_TAG }}

From e38594fd3ab5941a00190784c9aff3d1c351969f Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 10:26:37 +0100
Subject: [PATCH 05/38] create '.gobra' directory in docker image

---
 workflow-container/Dockerfile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/workflow-container/Dockerfile b/workflow-container/Dockerfile
index 988437ecb..245459468 100644
--- a/workflow-container/Dockerfile
+++ b/workflow-container/Dockerfile
@@ -98,4 +98,7 @@ COPY --from=build /build/gobra/target/scala-2.13/gobra.jar .
 COPY src/test/resources/regressions/examples/evaluation ./evaluation
 COPY src/test/resources/regressions/examples/tutorial-examples ./tutorial-examples
 
+# create the directory that Gobra uses to write its stats to:
+RUN mkdir -p .gobra
+
 ENTRYPOINT ["java", "-Xss128m", "-jar", "gobra.jar"]

From e6b22db025e4c0ef7dce522173cfe70b4b2f0734 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:02:40 +0100
Subject: [PATCH 06/38] first attempt to split up GobraTests

---
 .github/test-and-measure-ram.sh               |  5 ++--
 .github/workflows/test.yml                    | 23 ++++++++++++++++++-
 src/test/scala/viper/gobra/GobraTests.scala   | 10 ++++++++
 .../gobra/parsing/GobraParserTests.scala      |  5 +---
 4 files changed, 36 insertions(+), 7 deletions(-)

diff --git a/.github/test-and-measure-ram.sh b/.github/test-and-measure-ram.sh
index 0b7a6afc6..c889d16ac 100755
--- a/.github/test-and-measure-ram.sh
+++ b/.github/test-and-measure-ram.sh
@@ -5,10 +5,11 @@
 # start pidstats and write output to synced folder /build/gobra/sync
 pidstat 1 -r -H -p ALL > /build/gobra/sync/pidstat.txt & PIDSTAT_PID=$!
 
-# execute sbt test and stop pidstat independent of outcome
+# execute sbt with the provided $SBTCOMMAND or 'test' and stop pidstat independent of outcome
 # set `-Dsbt.color=always` such that sbt displays warnings in yellow, passed test cases in green and failed ones in red.
 # it seems that sbt on it's own thinks that colors cannot be displayed when run in docker and thus turns them off by default.
-sbt -Dsbt.color=always test
+COMMAND="${SBTCOMMAND:-test}"
+sbt -Dsbt.color=always $COMMAND
 TEST_RES=$?
 kill -INT $PIDSTAT_PID
 
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 16d5108e8..a1d8a59da 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -127,6 +127,7 @@ jobs:
 
 
   run-all-tests:
+    name: $${{ matrix.name }}
     runs-on: ubuntu-latest
     needs: build-container
     env:
@@ -137,6 +138,26 @@ jobs:
       NOTICE_LEVEL: "info"
       WARNING_LEVEL: "warning"
       FAILURE_LEVEL: "error"
+    strategy:
+      # tests should not be stopped when they fail on one of the OSes:
+      fail-fast: false
+      matrix:
+        name:
+          [
+            "GobraTests - regressions/examples",
+            "GobraTests - regressions/features",
+            "GobraTests - regressions/issues",
+            "All other tests"
+          ]
+        include:
+          - name: "GobraTests - regressions/examples"
+            sbt-command: 'set javaOptions += "-DGOBRATESTS_REGRESSIONS_DIR=regressions/examples";  testOnly * -- -n viper.gobra.GobraTestsTag'
+          - name: "GobraTests - regressions/features"
+            sbt-command: 'set javaOptions += "-DGOBRATESTS_REGRESSIONS_DIR=regressions/features";  testOnly * -- -n viper.gobra.GobraTestsTag'
+          - name: "GobraTests - regressions/issues"
+            sbt-command: 'set javaOptions += "-DGOBRATESTS_REGRESSIONS_DIR=regressions/issues";  testOnly * -- -n viper.gobra.GobraTestsTag'
+          - name: "All other tests"
+            sbt-command: 'testOnly * -- -l viper.gobra.GobraTestsTag'
     steps:
       # we only need .github/test-and-measure-ram.sh. Thus, we do not checkout the submodules
       - name: Checkout Gobra
@@ -158,7 +179,7 @@ jobs:
           docker run \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
-            /bin/sh -c "$(cat .github/test-and-measure-ram.sh)"
+            /bin/sh -c "SBTCOMMAND=${{ matrix.sbt-command }}; $(cat .github/test-and-measure-ram.sh)"
 
       - name: Get max RAM usage by Java and Z3
         if: ${{ always() }}
diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
index d528cced7..5e14ac59a 100644
--- a/src/test/scala/viper/gobra/GobraTests.scala
+++ b/src/test/scala/viper/gobra/GobraTests.scala
@@ -22,9 +22,19 @@ import viper.silver.testing.{AbstractOutput, AnnotatedTestInput, ProjectInfo, Sy
 import viper.silver.utility.TimingUtils
 import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 
+import java.lang.annotation.{ElementType, Retention, RetentionPolicy, Target}
+import scala.annotation.StaticAnnotation
 import scala.concurrent.{Await, Future}
 import scala.concurrent.duration.Duration
 
+@org.scalatest.TagAnnotation
+@Retention(RetentionPolicy.RUNTIME)
+@Target(Array(ElementType.METHOD, ElementType.TYPE))
+class GobraTestsTag extends StaticAnnotation
+
+// tag this class with `GobraTestsTag` such that we can run all except this test class
+// (if necessary) by executing `sbt "testOnly * -- -l viper.gobra.GobraTestsTag"`
+@GobraTestsTag
 class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
 
   val regressionsPropertyName = "GOBRATESTS_REGRESSIONS_DIR"
diff --git a/src/test/scala/viper/gobra/parsing/GobraParserTests.scala b/src/test/scala/viper/gobra/parsing/GobraParserTests.scala
index 66e338af3..63ddd266e 100644
--- a/src/test/scala/viper/gobra/parsing/GobraParserTests.scala
+++ b/src/test/scala/viper/gobra/parsing/GobraParserTests.scala
@@ -23,10 +23,7 @@ import scala.concurrent.duration.Duration
 
 class GobraParserTests extends AbstractGobraTests with BeforeAndAfterAll {
 
-  val regressionsPropertyName = "GOBRATESTS_REGRESSIONS_DIR"
-
-  val regressionsDir: String = System.getProperty(regressionsPropertyName, "better_errors")
-  val testDirectories: Seq[String] = Vector(regressionsDir)
+  val testDirectories: Seq[String] = Vector("better_errors")
   override val defaultTestPattern: String = PackageResolver.inputFilePattern
 
   var gobraInstance: Gobra = _

From c30f9e4a7291f9968a46af99ca06f470585dd479 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:19:39 +0100
Subject: [PATCH 07/38] tries to fix CI by escaping commands

---
 .github/test-and-measure-ram.sh | 2 +-
 .github/workflows/test.yml      | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/test-and-measure-ram.sh b/.github/test-and-measure-ram.sh
index c889d16ac..524417f39 100755
--- a/.github/test-and-measure-ram.sh
+++ b/.github/test-and-measure-ram.sh
@@ -9,7 +9,7 @@ pidstat 1 -r -H -p ALL > /build/gobra/sync/pidstat.txt & PIDSTAT_PID=$!
 # set `-Dsbt.color=always` such that sbt displays warnings in yellow, passed test cases in green and failed ones in red.
 # it seems that sbt on it's own thinks that colors cannot be displayed when run in docker and thus turns them off by default.
 COMMAND="${SBTCOMMAND:-test}"
-sbt -Dsbt.color=always $COMMAND
+sbt -Dsbt.color=always "$COMMAND"
 TEST_RES=$?
 kill -INT $PIDSTAT_PID
 
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index a1d8a59da..842ef1db7 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -127,7 +127,7 @@ jobs:
 
 
   run-all-tests:
-    name: $${{ matrix.name }}
+    name: ${{ matrix.name }}
     runs-on: ubuntu-latest
     needs: build-container
     env:
@@ -179,7 +179,7 @@ jobs:
           docker run \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
-            /bin/sh -c "SBTCOMMAND=${{ matrix.sbt-command }}; $(cat .github/test-and-measure-ram.sh)"
+            /bin/sh -c "SBTCOMMAND='${{ matrix.sbt-command }}'; $(cat .github/test-and-measure-ram.sh)"
 
       - name: Get max RAM usage by Java and Z3
         if: ${{ always() }}

From 30d15146054c71d14fa5ab1a7a4bd792716f616d Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:25:18 +0100
Subject: [PATCH 08/38] adds more escaping

---
 .github/workflows/test.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 842ef1db7..ce8cdae80 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -151,11 +151,11 @@ jobs:
           ]
         include:
           - name: "GobraTests - regressions/examples"
-            sbt-command: 'set javaOptions += "-DGOBRATESTS_REGRESSIONS_DIR=regressions/examples";  testOnly * -- -n viper.gobra.GobraTestsTag'
+            sbt-command: 'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/examples\";  testOnly * -- -n viper.gobra.GobraTestsTag'
           - name: "GobraTests - regressions/features"
-            sbt-command: 'set javaOptions += "-DGOBRATESTS_REGRESSIONS_DIR=regressions/features";  testOnly * -- -n viper.gobra.GobraTestsTag'
+            sbt-command: 'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/features\";  testOnly * -- -n viper.gobra.GobraTestsTag'
           - name: "GobraTests - regressions/issues"
-            sbt-command: 'set javaOptions += "-DGOBRATESTS_REGRESSIONS_DIR=regressions/issues";  testOnly * -- -n viper.gobra.GobraTestsTag'
+            sbt-command: 'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/issues\";  testOnly * -- -n viper.gobra.GobraTestsTag'
           - name: "All other tests"
             sbt-command: 'testOnly * -- -l viper.gobra.GobraTestsTag'
     steps:

From e0b5a01c29b6d04cee750bbf837949ebfa3a7cf7 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:40:47 +0100
Subject: [PATCH 09/38] switches to dynamically created matrix

---
 .github/workflows/test.yml | 42 +++++++++++++++++++++++---------------
 1 file changed, 25 insertions(+), 17 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index ce8cdae80..dc117ecd7 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -126,6 +126,30 @@ jobs:
         run: echo "IMAGE_TAG=${{ env.IMAGE_TAG }}" >> $GITHUB_OUTPUT
 
 
+  prepare-matrix:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - name: Checkout Gobra
+        uses: actions/checkout@v4
+        # we do not need any submodules here as we need the folders containing our test cases
+
+      - id: set-matrix
+        run: |
+          # find subfolders of `regressions` and use those as a natural split of the GobraTests
+          # store these subfolders as a JSON array:
+          REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions | jq -R . | jq -s --compact-output)
+          MATRIX_ENTRIES=''
+          for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.GobraTestsTag\"},"
+          done
+          # add an entry for all other non-GobraTests tests:
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.GobraTestsTag\"},"
+          echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
+        working-directory: gobra-ide/client
+
+
   run-all-tests:
     name: ${{ matrix.name }}
     runs-on: ubuntu-latest
@@ -141,23 +165,7 @@ jobs:
     strategy:
       # tests should not be stopped when they fail on one of the OSes:
       fail-fast: false
-      matrix:
-        name:
-          [
-            "GobraTests - regressions/examples",
-            "GobraTests - regressions/features",
-            "GobraTests - regressions/issues",
-            "All other tests"
-          ]
-        include:
-          - name: "GobraTests - regressions/examples"
-            sbt-command: 'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/examples\";  testOnly * -- -n viper.gobra.GobraTestsTag'
-          - name: "GobraTests - regressions/features"
-            sbt-command: 'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/features\";  testOnly * -- -n viper.gobra.GobraTestsTag'
-          - name: "GobraTests - regressions/issues"
-            sbt-command: 'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/issues\";  testOnly * -- -n viper.gobra.GobraTestsTag'
-          - name: "All other tests"
-            sbt-command: 'testOnly * -- -l viper.gobra.GobraTestsTag'
+      matrix: ${{ fromJson(needs.prepare-matrix.outputs.matrix) }}
     steps:
       # we only need .github/test-and-measure-ram.sh. Thus, we do not checkout the submodules
       - name: Checkout Gobra

From 78ef69dac30bcc302fab0101f4be6d117b9473fc Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:42:25 +0100
Subject: [PATCH 10/38] prints SBT command

---
 .github/test-and-measure-ram.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/test-and-measure-ram.sh b/.github/test-and-measure-ram.sh
index 524417f39..afa26cd55 100755
--- a/.github/test-and-measure-ram.sh
+++ b/.github/test-and-measure-ram.sh
@@ -9,6 +9,7 @@ pidstat 1 -r -H -p ALL > /build/gobra/sync/pidstat.txt & PIDSTAT_PID=$!
 # set `-Dsbt.color=always` such that sbt displays warnings in yellow, passed test cases in green and failed ones in red.
 # it seems that sbt on it's own thinks that colors cannot be displayed when run in docker and thus turns them off by default.
 COMMAND="${SBTCOMMAND:-test}"
+echo "sbt -Dsbt.color=always \"$COMMAND\""
 sbt -Dsbt.color=always "$COMMAND"
 TEST_RES=$?
 kill -INT $PIDSTAT_PID

From 3d8e26e6aa6bb652dda69846c33c4cde5999d258 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:43:13 +0100
Subject: [PATCH 11/38] fixes path in CI

---
 .github/workflows/test.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index dc117ecd7..bf9000fe8 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -147,7 +147,6 @@ jobs:
           # add an entry for all other non-GobraTests tests:
           MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.GobraTestsTag\"},"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
-        working-directory: gobra-ide/client
 
 
   run-all-tests:

From a100df114aa5b7d26f0e84ce5a9be1e9d5f55f4c Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:43:51 +0100
Subject: [PATCH 12/38] fixes job dependency in CI

---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index bf9000fe8..ac0afdc06 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -152,7 +152,7 @@ jobs:
   run-all-tests:
     name: ${{ matrix.name }}
     runs-on: ubuntu-latest
-    needs: build-container
+    needs: [build-container, prepare-matrix]
     env:
       CONCLUSION_SUCCESS: "success"
       CONCLUSION_FAILURE: "failure"

From 13011a30a6f1572374e5e458a9f3d3e3c0ad753d Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:47:31 +0100
Subject: [PATCH 13/38] adds output to debug matrix

---
 .github/workflows/test.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index ac0afdc06..761cfd8eb 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -146,6 +146,7 @@ jobs:
           done
           # add an entry for all other non-GobraTests tests:
           MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.GobraTestsTag\"},"
+          echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 
 

From ed9a083e3eb3d32728485600a86f4d7d6b90827a Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:48:17 +0100
Subject: [PATCH 14/38] fixes matrix in CI

---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 761cfd8eb..6a4cb8fd6 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -139,7 +139,7 @@ jobs:
         run: |
           # find subfolders of `regressions` and use those as a natural split of the GobraTests
           # store these subfolders as a JSON array:
-          REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions | jq -R . | jq -s --compact-output)
+          REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
             MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.GobraTestsTag\"},"

From 644b86f88d636df53b5826ef0e590b9256bc3964 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:52:12 +0100
Subject: [PATCH 15/38] adds more escaping to commands in CI

---
 .github/workflows/test.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 6a4cb8fd6..0de05c014 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,10 +142,10 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.GobraTestsTag\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"\'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.GobraTestsTag\'\"},"
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.GobraTestsTag\"},"
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"\'testOnly * -- -l viper.gobra.GobraTestsTag\'\"},"
           echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 

From c4158b957c055ac85a8b8c9c3cee15d5184d660c Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:53:24 +0100
Subject: [PATCH 16/38] adds more testing to CI

---
 .github/workflows/test.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 0de05c014..c69d96e4c 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -149,6 +149,9 @@ jobs:
           echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 
+      - name: Test matrix
+        run: echo "${{ fromJson(steps.set-matrix.outputs.matrix) }}"
+
 
   run-all-tests:
     name: ${{ matrix.name }}

From bf7c3819649addc6adda3bb6e6d1f46d506ff768 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:54:57 +0100
Subject: [PATCH 17/38] switches to apostroph instead of escaped apostroph in
 CI

---
 .github/workflows/test.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index c69d96e4c..96d5c8fd0 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,10 +142,10 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"\'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.GobraTestsTag\'\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.GobraTestsTag'\"},"
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"\'testOnly * -- -l viper.gobra.GobraTestsTag\'\"},"
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"'testOnly * -- -l viper.gobra.GobraTestsTag'\"},"
           echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 

From 945e7e86b29acd210c388694f903be391e3ab2f1 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:57:12 +0100
Subject: [PATCH 18/38] removes apostroph in CI

---
 .github/workflows/test.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 96d5c8fd0..03ee093fc 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,10 +142,10 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"'set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.GobraTestsTag'\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += '-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\';  testOnly * -- -n viper.gobra.GobraTestsTag\"},"
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"'testOnly * -- -l viper.gobra.GobraTestsTag'\"},"
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.GobraTestsTag\"},"
           echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 

From a2c8ee6a728fbe619323aabd47f87dd10fb1069b Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 11:58:37 +0100
Subject: [PATCH 19/38] removes superfluous backslash

---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 03ee093fc..25cefecb1 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,7 +142,7 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += '-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\';  testOnly * -- -n viper.gobra.GobraTestsTag\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += '-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER';  testOnly * -- -n viper.gobra.GobraTestsTag\"},"
           done
           # add an entry for all other non-GobraTests tests:
           MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.GobraTestsTag\"},"

From dfd8af7b6770c7009f48e1b476ab5a4a75689537 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 17:59:05 +0100
Subject: [PATCH 20/38] makes 'GobraTestsTag' a Java annotation, adds quotes
 for javaOptions parameter in CI

---
 .github/workflows/test.yml                    |  4 +-
 .../java/viper/gobra/tags/GobraTestsTag.java  | 15 ++++
 src/test/scala/viper/gobra/GobraTests.scala   | 73 +++++++++++--------
 3 files changed, 61 insertions(+), 31 deletions(-)
 create mode 100644 src/test/java/viper/gobra/tags/GobraTestsTag.java

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 25cefecb1..dae68cdfa 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,10 +142,10 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += '-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER';  testOnly * -- -n viper.gobra.GobraTestsTag\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \'-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\';  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.GobraTestsTag\"},"
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\"},"
           echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 
diff --git a/src/test/java/viper/gobra/tags/GobraTestsTag.java b/src/test/java/viper/gobra/tags/GobraTestsTag.java
new file mode 100644
index 000000000..11fe99080
--- /dev/null
+++ b/src/test/java/viper/gobra/tags/GobraTestsTag.java
@@ -0,0 +1,15 @@
+package viper.gobra.tags;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+// We define a custom tag to selectively enable / disable GobraTests from SBT.
+// According to the documentation of org.scalatest.Tag, this annotation must be defined in Java
+// as Scala annotations are not available at runtime, which is confirmed by our own experiments.
+
+@org.scalatest.TagAnnotation
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.TYPE})
+public @interface GobraTestsTag {}
diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
index 5e14ac59a..d195ca613 100644
--- a/src/test/scala/viper/gobra/GobraTests.scala
+++ b/src/test/scala/viper/gobra/GobraTests.scala
@@ -9,28 +9,23 @@ package viper.gobra
 import java.nio.file.Path
 import ch.qos.logback.classic.Level
 import org.bitbucket.inkytonik.kiama.util.Source
-import org.scalatest.{Args, BeforeAndAfterAll, Status}
-import scalaz.EitherT
+import org.scalatest.{Args, BeforeAndAfterAll, Status, Tag}
 import scalaz.Scalaz.futureInstance
 import viper.gobra.frontend.PackageResolver.RegularPackage
 import viper.gobra.frontend.Source.FromFileSource
-import viper.gobra.frontend.info.Info
+import viper.gobra.frontend.info.{Info, TypeInfo}
 import viper.gobra.frontend.{Config, PackageResolver, Parser, Source}
 import viper.gobra.reporting.VerifierResult.{Failure, Success}
 import viper.gobra.reporting.{GobraMessage, GobraReporter, VerifierError}
+import viper.gobra.tags.GobraTestsTag
 import viper.silver.testing.{AbstractOutput, AnnotatedTestInput, ProjectInfo, SystemUnderTest}
 import viper.silver.utility.TimingUtils
 import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 
-import java.lang.annotation.{ElementType, Retention, RetentionPolicy, Target}
-import scala.annotation.StaticAnnotation
-import scala.concurrent.{Await, Future}
+import java.util.concurrent.atomic.AtomicReference
+import scala.concurrent.{Await, Future, Promise}
 import scala.concurrent.duration.Duration
 
-@org.scalatest.TagAnnotation
-@Retention(RetentionPolicy.RUNTIME)
-@Target(Array(ElementType.METHOD, ElementType.TYPE))
-class GobraTestsTag extends StaticAnnotation
 
 // tag this class with `GobraTestsTag` such that we can run all except this test class
 // (if necessary) by executing `sbt "testOnly * -- -l viper.gobra.GobraTestsTag"`
@@ -46,7 +41,8 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
   var gobraInstance: Gobra = _
   var executor: GobraExecutionContext = _
   var inputs: Vector[Source] = Vector.empty
-  val cacheParserAndTypeChecker = true
+  val shouldPreParseAndTypeCheck = true
+  val preParseAndTypeCheckResult: AtomicReference[Option[Future[Vector[Either[Vector[VerifierError], TypeInfo]]]]] = new AtomicReference(None)
 
   override def beforeAll(): Unit = {
     executor = new DefaultGobraExecutionContext()
@@ -65,31 +61,50 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
       reporter = StringifyReporter,
       packageInfoInputMap = Map(Source.getPackageInfoOrCrash(source, Path.of("")) -> Vector(source)),
       checkConsistency = true,
-      cacheParserAndTypeChecker = cacheParserAndTypeChecker,
+      cacheParserAndTypeChecker = shouldPreParseAndTypeCheck,
       z3Exe = z3Exe,
       // termination checks in functions are currently disabled in the tests. This can be enabled in the future,
       // but requires some work to add termination measures all over the test suite.
       disableCheckTerminationPureFns = true,
     )
 
-  override def runTests(testName: Option[String], args: Args): Status = {
-    if (cacheParserAndTypeChecker) {
-      implicit val execContext: GobraExecutionContext = executor
-      val futs = inputs.map(source => {
-        val config = getConfig(source)
-        val pkgInfo = config.packageInfoInputMap.keys.head
-        val fut = for {
-          finalConfig <- EitherT.fromEither(Future.successful(gobraInstance.getAndMergeInFileConfig(config, pkgInfo)))
-          parseResult <- Parser.parse(finalConfig, pkgInfo)
-          pkg = RegularPackage(pkgInfo.id)
-          typeCheckResult <- Info.check(finalConfig, pkg, parseResult)
-        } yield typeCheckResult
-        fut.toEither
-      })
-      Await.result(Future.sequence(futs), Duration.Inf)
-      println("pre-parsing and pre-typeChecking completed")
+  // The testing framework calls first `runTests` once, followed by multiple calls to `runTest`.
+  // Even if we skip `GobraTests` by instructing ScalaTest to ignore a certain tag, `runTests` is still called.
+  // Thus, we start the pre-parsing and pre-typeChecking at the first invocation of `runTest`.
+  override def runTest(testName: String, args: Args): Status = {
+    if (shouldPreParseAndTypeCheck) {
+      val result: Promise[Vector[Either[Vector[VerifierError], TypeInfo]]] = Promise()
+      val prevValue = preParseAndTypeCheckResult.getAndUpdate {
+        case None => Some(result.future)
+        case v => v // leave unchanged
+      }
+      // We start the pre-parsing and pre-typechecking only if we just updated the atomic reference, i.e., the
+      // previous value was `None`.
+      val fut = prevValue match {
+        case Some(f) => f // atomic reference was already set by another thread
+        case None =>
+          implicit val execContext: GobraExecutionContext = executor
+          val futs = inputs.map(source => {
+            val config = getConfig(source)
+            val pkgInfo = config.packageInfoInputMap.keys.head
+            val fut = for {
+              parseResult <- Parser.parse(config, pkgInfo)
+              pkg = RegularPackage(pkgInfo.id)
+              typeCheckResult <- Info.check(config, pkg, parseResult)
+            } yield typeCheckResult
+            fut.toEither
+          })
+          Future.sequence(futs)
+            .andThen(res => {
+              result.complete(res) // set the result to the promise
+            })
+          result.future // return the promise's future
+      }
+      // block until the pre-parsing and pre-typechecking is completed:
+      Await.result(fut, Duration.Inf)
     }
-    super.runTests(testName, args)
+
+    super.runTest(testName, args)
   }
 
   override def afterAll(): Unit = {

From cbd27287ff7cf6ffca244a186f0c75573e8c5619 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 18:11:02 +0100
Subject: [PATCH 21/38] switches to double quotes for the javaOptions in CI

---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index dae68cdfa..bf5b8091f 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,7 +142,7 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \'-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\';  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
           done
           # add an entry for all other non-GobraTests tests:
           MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\"},"

From dc2c88ab38d21ffdb4e46f2f6bf1bb92d2ed1a51 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 18:12:06 +0100
Subject: [PATCH 22/38] escapes the backslashes escaping the double quotes for
 the javaOptions

---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index bf5b8091f..10916ac17 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,7 +142,7 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
           done
           # add an entry for all other non-GobraTests tests:
           MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\"},"

From f9802d4092ccd92a63fb68e03ba37a13e8a6d49c Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 18:36:42 +0100
Subject: [PATCH 23/38] yet another attempt at correct escaping

---
 .github/workflows/test.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 10916ac17..67b5c3e76 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,10 +142,10 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
+            MATRIX_ENTRIES=$'$MATRIX_ENTRIES {"name": "GobraTests - regressions/$SUBFOLDER", "sbt-command": "set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag"},'
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\"},"
+          MATRIX_ENTRIES=$'$MATRIX_ENTRIES {"name": "All other tests", "sbt-command": "testOnly * -- -l viper.gobra.tags.GobraTestsTag"},'
           echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 
@@ -190,7 +190,7 @@ jobs:
           docker run \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
-            /bin/sh -c "SBTCOMMAND='${{ matrix.sbt-command }}'; $(cat .github/test-and-measure-ram.sh)"
+            /bin/sh -c $'SBTCOMMAND=\'${{ matrix.sbt-command }}\'; $(cat .github/test-and-measure-ram.sh)'
 
       - name: Get max RAM usage by Java and Z3
         if: ${{ always() }}

From 375226454cb8a8ad476f924554b95a45506c4eca Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 18:40:00 +0100
Subject: [PATCH 24/38] yet another try

---
 .github/workflows/test.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 67b5c3e76..9691cb5ec 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,10 +142,10 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES=$'$MATRIX_ENTRIES {"name": "GobraTests - regressions/$SUBFOLDER", "sbt-command": "set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag"},'
+            MATRIX_ENTRIES="$MATRIX_ENTRIES "$'{"name": "GobraTests - regressions/$SUBFOLDER", "sbt-command": "set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag"},'
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES=$'$MATRIX_ENTRIES {"name": "All other tests", "sbt-command": "testOnly * -- -l viper.gobra.tags.GobraTestsTag"},'
+          MATRIX_ENTRIES="$MATRIX_ENTRIES "$'{"name": "All other tests", "sbt-command": "testOnly * -- -l viper.gobra.tags.GobraTestsTag"},'
           echo "$MATRIX_ENTRIES"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 

From 02e82abafe59a0c1f7d2cdc51551a60be584b328 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 18:45:19 +0100
Subject: [PATCH 25/38] one more try

---
 .github/workflows/test.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 9691cb5ec..92ba978a8 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,11 +142,11 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES "$'{"name": "GobraTests - regressions/$SUBFOLDER", "sbt-command": "set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag"},'
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES="$MATRIX_ENTRIES "$'{"name": "All other tests", "sbt-command": "testOnly * -- -l viper.gobra.tags.GobraTestsTag"},'
-          echo "$MATRIX_ENTRIES"
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\"},"
+          echo "matrix={\"include\": [$MATRIX_ENTRIES]}"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 
       - name: Test matrix

From e9202748b917c68bf0a07a4500dc8f6d15e8833f Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 18:53:39 +0100
Subject: [PATCH 26/38] adds more log output

---
 .github/workflows/test.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 92ba978a8..6fdb1cc8d 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -187,6 +187,8 @@ jobs:
         run: |
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
+          echo ${{ matrix.sbt-command }}
+          echo ${{ needs.prepare-matrix.outputs.matrix }}
           docker run \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \

From e71629807f5104a82398be3d9f1a11ea6cf42177 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 19:04:06 +0100
Subject: [PATCH 27/38] another try

---
 .github/workflows/test.yml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 6fdb1cc8d..7766c64a1 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -165,6 +165,8 @@ jobs:
       NOTICE_LEVEL: "info"
       WARNING_LEVEL: "warning"
       FAILURE_LEVEL: "error"
+      # we do the context expansion here to avoid escaping problems below as explained in https://stackoverflow.com/a/77924154/1990080
+      SBT_COMMAND: ${{ matrix.sbt-command }}
     strategy:
       # tests should not be stopped when they fail on one of the OSes:
       fail-fast: false
@@ -187,12 +189,13 @@ jobs:
         run: |
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
-          echo ${{ matrix.sbt-command }}
-          echo ${{ needs.prepare-matrix.outputs.matrix }}
+          echo "${{ matrix.sbt-command }}"
+          echo "$SBT_COMMAND"
+          echo "${{ needs.prepare-matrix.outputs.matrix }}"
           docker run \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
-            /bin/sh -c $'SBTCOMMAND=\'${{ matrix.sbt-command }}\'; $(cat .github/test-and-measure-ram.sh)'
+            /bin/sh -c $'SBTCOMMAND=\'$SBT_COMMAND\'; $(cat .github/test-and-measure-ram.sh)'
 
       - name: Get max RAM usage by Java and Z3
         if: ${{ always() }}

From b73c94ad14f040831130d006875e316063e3d157 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Wed, 12 Mar 2025 19:31:52 +0100
Subject: [PATCH 28/38] changes the way we pass environment variables to the
 script running within the docker container

---
 .github/workflows/test.yml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 7766c64a1..7157ecad2 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -193,9 +193,10 @@ jobs:
           echo "$SBT_COMMAND"
           echo "${{ needs.prepare-matrix.outputs.matrix }}"
           docker run \
+            -e SBTCOMMAND="$SBT_COMMAND" \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
-            /bin/sh -c $'SBTCOMMAND=\'$SBT_COMMAND\'; $(cat .github/test-and-measure-ram.sh)'
+            /bin/sh -c '$(cat .github/test-and-measure-ram.sh)'
 
       - name: Get max RAM usage by Java and Z3
         if: ${{ always() }}

From 4febf677eb368186e013011411a00f0b31394728 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 00:46:12 +0100
Subject: [PATCH 29/38] yet another attempt to fix quotes

---
 .github/workflows/test.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 7157ecad2..c178df70a 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -189,14 +189,14 @@ jobs:
         run: |
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
-          echo "${{ matrix.sbt-command }}"
-          echo "$SBT_COMMAND"
-          echo "${{ needs.prepare-matrix.outputs.matrix }}"
+          # echo "${{ matrix.sbt-command }}"
+          # echo "$SBT_COMMAND"
+          # echo "${{ needs.prepare-matrix.outputs.matrix }}"
           docker run \
             -e SBTCOMMAND="$SBT_COMMAND" \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
-            /bin/sh -c '$(cat .github/test-and-measure-ram.sh)'
+            /bin/sh -c "$(cat .github/test-and-measure-ram.sh)"
 
       - name: Get max RAM usage by Java and Z3
         if: ${{ always() }}

From 01e6179b4c8486afa7be1ddc81812d51734e14e8 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 00:57:54 +0100
Subject: [PATCH 30/38] makes pidstat filenames unique

---
 .github/test-and-measure-ram.sh |  1 -
 .github/workflows/test.yml      | 12 +++---------
 2 files changed, 3 insertions(+), 10 deletions(-)

diff --git a/.github/test-and-measure-ram.sh b/.github/test-and-measure-ram.sh
index afa26cd55..524417f39 100755
--- a/.github/test-and-measure-ram.sh
+++ b/.github/test-and-measure-ram.sh
@@ -9,7 +9,6 @@ pidstat 1 -r -H -p ALL > /build/gobra/sync/pidstat.txt & PIDSTAT_PID=$!
 # set `-Dsbt.color=always` such that sbt displays warnings in yellow, passed test cases in green and failed ones in red.
 # it seems that sbt on it's own thinks that colors cannot be displayed when run in docker and thus turns them off by default.
 COMMAND="${SBTCOMMAND:-test}"
-echo "sbt -Dsbt.color=always \"$COMMAND\""
 sbt -Dsbt.color=always "$COMMAND"
 TEST_RES=$?
 kill -INT $PIDSTAT_PID
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index c178df70a..2350343d5 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,16 +142,13 @@ jobs:
           REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
           MATRIX_ENTRIES=''
           for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
-            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\"},"
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\", \"pidstat-filename\": \"pidstat-GobraTests-$SUBFOLDER.txt\"},"
           done
           # add an entry for all other non-GobraTests tests:
-          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\"},"
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\", \"pidstat-filename\": \"pidstat-OtherTests.txt\"},"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 
-      - name: Test matrix
-        run: echo "${{ fromJson(steps.set-matrix.outputs.matrix) }}"
-
 
   run-all-tests:
     name: ${{ matrix.name }}
@@ -189,9 +186,6 @@ jobs:
         run: |
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
-          # echo "${{ matrix.sbt-command }}"
-          # echo "$SBT_COMMAND"
-          # echo "${{ needs.prepare-matrix.outputs.matrix }}"
           docker run \
             -e SBTCOMMAND="$SBT_COMMAND" \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
@@ -286,7 +280,7 @@ jobs:
         if: ${{ always() }}
         uses: actions/upload-artifact@v6
         with:
-          name: pidstat.txt
+          name: ${{ matrix.pidstat-filename }}
           path: sync/pidstat.txt
 
 

From 492920e49631e8cf5a03ed549c6f8384483a0446 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 00:59:32 +0100
Subject: [PATCH 31/38] tests whether detour via env variable is necessary

---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 2350343d5..bbbc490c9 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -187,7 +187,7 @@ jobs:
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
           docker run \
-            -e SBTCOMMAND="$SBT_COMMAND" \
+            -e SBTCOMMAND="${{ matrix.sbt-command }}" \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
             /bin/sh -c "$(cat .github/test-and-measure-ram.sh)"

From bda1eda0333a17f1cb5f3ccac7e73e8bcb8b191f Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 01:03:10 +0100
Subject: [PATCH 32/38] Reverts "tests whether detour via env variable is
 necessary"

This reverts commit 5a7fcbd9ad41bf92f9698faabbd0ec319c2941fb.
---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index bbbc490c9..2350343d5 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -187,7 +187,7 @@ jobs:
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
           docker run \
-            -e SBTCOMMAND="${{ matrix.sbt-command }}" \
+            -e SBTCOMMAND="$SBT_COMMAND" \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
             /bin/sh -c "$(cat .github/test-and-measure-ram.sh)"

From b495d85c7a35af567de326d7c34e1eeac15fe179 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 01:04:17 +0100
Subject: [PATCH 33/38] adds some documentation

---
 .github/workflows/test.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 2350343d5..3b47df157 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -146,6 +146,7 @@ jobs:
           done
           # add an entry for all other non-GobraTests tests:
           MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\", \"pidstat-filename\": \"pidstat-OtherTests.txt\"},"
+          # print matrix for debugging purposes:
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}"
           echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
 

From 6b5df5bdddf4e4772684def022cfc8d18a3e26cb Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 01:04:35 +0100
Subject: [PATCH 34/38] fixes a compiler warning

---
 src/test/scala/viper/gobra/GobraTests.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
index d195ca613..b14ca05fa 100644
--- a/src/test/scala/viper/gobra/GobraTests.scala
+++ b/src/test/scala/viper/gobra/GobraTests.scala
@@ -9,7 +9,7 @@ package viper.gobra
 import java.nio.file.Path
 import ch.qos.logback.classic.Level
 import org.bitbucket.inkytonik.kiama.util.Source
-import org.scalatest.{Args, BeforeAndAfterAll, Status, Tag}
+import org.scalatest.{Args, BeforeAndAfterAll, Status}
 import scalaz.Scalaz.futureInstance
 import viper.gobra.frontend.PackageResolver.RegularPackage
 import viper.gobra.frontend.Source.FromFileSource

From 905fe7d72e9a71d7458e840da7433362d476c4ad Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 01:08:31 +0100
Subject: [PATCH 35/38] merges final image testing and deployment jobs

---
 .github/workflows/test.yml | 22 +++-------------------
 1 file changed, 3 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 3b47df157..21ab3f160 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -183,7 +183,7 @@ jobs:
       - name: Load image
         run: docker load --input /tmp/${{ env.BUILD_IMAGE_FILENAME }}
 
-      - name: Execute all tests
+      - name: Execute tests
         run: |
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
@@ -285,9 +285,9 @@ jobs:
           path: sync/pidstat.txt
 
 
-  test-final-container:
+  test-final-container-and-deploy:
     runs-on: ubuntu-latest
-    needs: build-container
+    needs: [build-container, run-all-tests]
     steps:
       - name: Download final image
         uses: actions/download-artifact@v4
@@ -304,11 +304,6 @@ jobs:
             ${{ needs.build-container.outputs.IMAGE_TAG }} \
             -i tutorial-examples/basic-annotations.gobra
 
-
-  deploy-container:
-    runs-on: ubuntu-latest
-    needs: [build-container, run-all-tests, test-final-container]
-    steps:
       - name: Decide whether image should be deployed or not
         run: |
           # note that these GitHub expressions return the value '1' for 'true' (as opposed to bash)
@@ -325,17 +320,6 @@ jobs:
           fi
           echo "SHOULD_DEPLOY=$SHOULD_DEPLOY" >> $GITHUB_ENV
 
-      - name: Download final image
-        if: env.SHOULD_DEPLOY == 'true'
-        uses: actions/download-artifact@v4
-        with:
-          name: ${{ env.FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME }}
-          path: /tmp
-
-      - name: Load image
-        if: env.SHOULD_DEPLOY == 'true'
-        run: docker load --input /tmp/${{ env.FINAL_IMAGE_FILENAME }}
-
       - name: Login to Github Packages
         if: env.SHOULD_DEPLOY == 'true'
         uses: docker/login-action@v3

From 3c43cc9d3cc61598c076179eeefe56825b0d285e Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 13 Mar 2025 10:03:56 +0100
Subject: [PATCH 36/38] fixes license header

---
 .github/license-check/config.json                 | 3 ++-
 src/test/java/viper/gobra/tags/GobraTestsTag.java | 6 ++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/.github/license-check/config.json b/.github/license-check/config.json
index 9582adef6..0b939ac2c 100644
--- a/.github/license-check/config.json
+++ b/.github/license-check/config.json
@@ -6,7 +6,8 @@
       "**/*.go",
       "build.sbt",
       "src/main/resources/stubs/github.com/**/*.gobra",
-      "**/Gobra*.g4"
+      "**/Gobra*.g4",
+      "src/test/java/**/*.java"
     ],
     "exclude": [
       "carbon/**",
diff --git a/src/test/java/viper/gobra/tags/GobraTestsTag.java b/src/test/java/viper/gobra/tags/GobraTestsTag.java
index 11fe99080..c8ec04a8d 100644
--- a/src/test/java/viper/gobra/tags/GobraTestsTag.java
+++ b/src/test/java/viper/gobra/tags/GobraTestsTag.java
@@ -1,3 +1,9 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2025 ETH Zurich.
+
 package viper.gobra.tags;
 
 import java.lang.annotation.ElementType;

From e59c4ea87450f49f35b7f62d8864491160a33b68 Mon Sep 17 00:00:00 2001
From: Linard Arquint <arquintl@nus.edu.sg>
Date: Wed, 25 Feb 2026 12:29:48 +0800
Subject: [PATCH 37/38] adds compilation of test classes to the Docker image's
 build phase

---
 workflow-container/Dockerfile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/workflow-container/Dockerfile b/workflow-container/Dockerfile
index 245459468..d82852d7b 100644
--- a/workflow-container/Dockerfile
+++ b/workflow-container/Dockerfile
@@ -65,6 +65,9 @@ COPY viperserver /build/gobra/viperserver
 
 RUN sbt assembly
 
+# force compilation of test classes:
+RUN sbt "test:compile"
+
 
 # a second build stage starts here that is based of a fresh image.
 # note that only stuff explicitly copied from "build" will be present.

From cde184ddab106ec384c14ddad489449c6e4637f7 Mon Sep 17 00:00:00 2001
From: Linard Arquint <arquintl@nus.edu.sg>
Date: Wed, 25 Feb 2026 12:38:10 +0800
Subject: [PATCH 38/38] fixes merge bug by reapplying the changes from commit
 '74462f9179335fd05fd5ec008bb27442e2accb22'

---
 src/test/scala/viper/gobra/GobraTests.scala | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
index b14ca05fa..ee269dd21 100644
--- a/src/test/scala/viper/gobra/GobraTests.scala
+++ b/src/test/scala/viper/gobra/GobraTests.scala
@@ -10,6 +10,7 @@ import java.nio.file.Path
 import ch.qos.logback.classic.Level
 import org.bitbucket.inkytonik.kiama.util.Source
 import org.scalatest.{Args, BeforeAndAfterAll, Status}
+import scalaz.EitherT
 import scalaz.Scalaz.futureInstance
 import viper.gobra.frontend.PackageResolver.RegularPackage
 import viper.gobra.frontend.Source.FromFileSource
@@ -88,9 +89,10 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
             val config = getConfig(source)
             val pkgInfo = config.packageInfoInputMap.keys.head
             val fut = for {
-              parseResult <- Parser.parse(config, pkgInfo)
+              finalConfig <- EitherT.fromEither(Future.successful(gobraInstance.getAndMergeInFileConfig(config, pkgInfo)))
+              parseResult <- Parser.parse(finalConfig, pkgInfo)
               pkg = RegularPackage(pkgInfo.id)
-              typeCheckResult <- Info.check(config, pkg, parseResult)
+              typeCheckResult <- Info.check(finalConfig, pkg, parseResult)
             } yield typeCheckResult
             fut.toEither
           })