Merge branch 'viperproject:master' into master

Author: jogasser

.github/workflows/scala.yml

@@ -36,33 +36,61 @@ on:
 # them. This job automatically runs every night.
 # - create-stable-release
 # takes the fat and skinny JARs produced by configuration `release` during `build` job and creates a draft release with
-# them.
+# them. This only works on branch `release`.
 
 env:
   Z3_VERSION: "4.8.6"
 
 jobs:
-  build:
+  prepare-matrix:
     # build is the base job on which all other jobs depend
     # we enforce here that the nightly build job only runs in the main repo:
     if: (github.event_name == 'schedule' && github.repository == 'viperproject/viperserver') || (github.event_name != 'schedule')
+    # sets up matrix for `build` job (based on https://stackoverflow.com/a/65434401/1990080)
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - id: set-matrix
+        run: |
+          # note that the values of `NAME` are also used in all other jobs and they have to match!
+          IS_RELEASE=${{ github.ref == 'refs/heads/release' }}
+          # skip 'latest' name on 'release' branch and ignore 'release' on all other branches'
+          if [[ "$IS_RELEASE" == ${{ true }} ]]
+          then
+            NAME="release"
+            SILVER_REF="v.21.07-release"
+            SILICON_REF="v.21.07-release"
+            CARBON_REF="v.21.07-release"
+          else
+            NAME="latest"
+            SILVER_REF="master"
+            SILICON_REF="master"
+            CARBON_REF="master"
+          fi
+          # creates a JSON object that looks like the key-values in the GitHub documentation on `strategy.matrix`
+          MATRIX="{ \
+            \"name\":[\"$NAME\"], \
+            \"include\": [{ \
+              \"name\":\"$NAME\", \
+              \"silver-ref\":\"$SILVER_REF\", \
+              \"silicon-ref\":\"$SILICON_REF\", \
+              \"carbon-ref\":\"$CARBON_REF\" \
+            }] \
+          }"
+          # print matrix for debugging purposes:
+          echo $MATRIX
+          # set outputs of job:
+          echo ::set-output name=matrix::$MATRIX
+
+  build:
+    needs: prepare-matrix
     runs-on: ubuntu-latest
     container: viperproject/viperserver:v3_z3_4.8.6
     strategy:
       # tests should not be stopped when they fail on one of the configurations:
       fail-fast: false
-      matrix:
-        # note that the same names are also used in all other jobs and they have to match!
-        name: [latest, release]
-        include:
-          - name: latest
-            silver-ref: "master"
-            silicon-ref: "master"
-            carbon-ref: "master"
-          - name: release
-            silver-ref: "v.21.07-release"
-            silicon-ref: "v.21.07-release"
-            carbon-ref: "v.21.07-release"
+      matrix: ${{ fromJson(needs.prepare-matrix.outputs.matrix) }}
     steps:
       - name: Checkout ViperServer
         uses: actions/checkout@v2
@@ -180,13 +208,13 @@ jobs:
 
 
   test:
-    needs: build
+    needs: [prepare-matrix, build]
     strategy:
       # tests should not be stopped when they fail on one of the OSes:
       fail-fast: false
       matrix:
         os: [macos-latest, ubuntu-latest, windows-latest]
-        name: [latest, release]
+        name: ${{ fromJson(needs.prepare-matrix.outputs.matrix).name }}
     runs-on: ${{ matrix.os }}
     steps:
       # we need to checkout the repo to have access to the test files
@@ -262,9 +290,9 @@ jobs:
 
 
   create-nightly-release:
+    needs: [prepare-matrix, test]
     # this job creates a new nightly pre-release, set viperserver.jar as artifacts, and deletes old releases
-    if: (github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'nightly') || github.event_name == 'schedule'
-    needs: test
+    if: contains(fromJson(needs.prepare-matrix.outputs.matrix).name, 'latest') && ((github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'nightly') || github.event_name == 'schedule')
     runs-on: ubuntu-latest
     env:
       # specifies that `latest` artifacts from `build` job should be used for nightly releases:
@@ -370,9 +398,9 @@ jobs:
 
 
   create-stable-release:
+    needs: [prepare-matrix, test]
     # this job creates a stable draft-release and set viperserver.jar as artifacts
-    if: github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'stable'
-    needs: test
+    if: contains(fromJson(needs.prepare-matrix.outputs.matrix).name, 'release') && github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'stable'
     runs-on: ubuntu-latest
     env:
       # specifies that `release` artifacts from `build` job should be used for stable releases:

src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala

@@ -170,13 +170,14 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
   implicit val abstractError_writer: RootJsonFormat[AbstractError] = lift(new RootJsonWriter[AbstractError] {
     override def write(obj: AbstractError): JsValue = {
       obj match {
-        case e: VerificationError if e.counterexample.isDefined =>
+        case e: VerificationError =>
+          val counterexamples: Seq[Counterexample] = e.failureContexts.flatMap(ctx => ctx.counterExample)
           JsObject(
             "tag" -> JsString(obj.fullId),
             "text" -> JsString(obj.readableMessage),
             "position" -> obj.pos.toJson,
             "cached" -> JsBoolean(obj.cached),
-            "counterexample" -> e.counterexample.get.toJson)
+            "counterexamples" -> JsArray(counterexamples.map(_.toJson).toVector))
         case _ =>
           JsObject(
             "tag" -> JsString(obj.fullId),