Merge branch 'master' into lsp

.github/workflows/scala.yml

@@ -324,16 +324,16 @@ jobs:
       - name: Create nightly release
         if: env.MATCHING_RELEASE != 'true'
         id: create_release
-        uses: viperproject/create-nightly-release@v1
+        uses: actions/create-release@v1
         env:
           # This token is provided by Actions, you do not need to create your own token
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         with:
           tag_name: ${{ env.TAG_NAME }}
           release_name: Nightly Release ${{ env.TAG_NAME }}
           body_path: versions.txt
-          keep_num: 1 # keep the previous nightly release such that there are always two
-          keep_tags: true
+          draft: false
+          prerelease: true
 
       - name: Upload ViperServer skinny jars
         if: env.MATCHING_RELEASE != 'true'
@@ -357,25 +357,6 @@ jobs:
           asset_name: viperserver.jar
           asset_content_type: application/octet-stream
 
-      - name: Trigger Viper-IDE CI
-        if: env.MATCHING_RELEASE != 'true'
-        run: |
-          curl --fail --request POST \
-          --user 'viper-admin:${{ secrets.VIPER_ADMIN_TOKEN }}' \
-          --header 'Accept: application/vnd.github.v3+json' \
-          --url 'https://api.github.com/repos/viperproject/viper-ide/actions/workflows/test.yml/dispatches' \
-          --data "{ \
-            \"ref\":\"master\", \
-            \"inputs\":{ \
-              \"type\":\"nightly\", \
-              \"viperserver_tag_name\":\"${{ env.TAG_NAME }}\", \
-              \"boogie_tag_name\":\"latest\", \
-              \"z3_version\":\"${{ env.Z3_VERSION }}\", \
-              \"tag_name\":\"${{ env.TAG_NAME }}\", \
-              \"release_name\":\"Nightly Release ${{ env.TAG_NAME }}\" \
-            } \
-          }"
-
 
   create-stable-release:
     needs: test

src/main/scala/viper/server/core/VerificationWorker.scala

@@ -154,6 +154,12 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend,
       val res = for {
         filteredProgram <- filter(_ast)
         innerProgram <- beforeVerify(filteredProgram)
+        stats = StatisticsReport(innerProgram.methods.size,
+          innerProgram.functions.size,
+          innerProgram.predicates.size,
+          innerProgram.domains.size,
+          innerProgram.fields.size)
+        _ = _frontend.reporter.report(stats)
         cachingResult = caching(innerProgram)
         verificationResult <- verification(cachingResult.transformedProgram)
         combinedVerificationResult = postCaching(cachingResult, verificationResult)

src/main/scala/viper/server/utility/ProgramDefinitionsProvider.scala

@@ -129,27 +129,9 @@ trait ProgramDefinitionsProvider {
     } flatten) toList
   }
 
-  private def countInstances(p: Program): Map[String, Int] = p.members.groupBy({
-    case _: Method => "method"
-    case _: Function => "function"
-    case _: Predicate => "predicate"
-    case _: Domain => "domain"
-    case _: Field => "field"
-    case _ => "other"
-  }).view.mapValues(_.size).toMap
-
   def reportProgramStats(): Unit = {
     val prog = _frontend.program.get
-    val stats = countInstances(prog)
-
     _frontend.reporter.report(ProgramOutlineReport(prog.members.toList))
-    _frontend.reporter.report(StatisticsReport(
-      stats.getOrElse("method", 0),
-      stats.getOrElse("function", 0),
-      stats.getOrElse("predicate", 0),
-      stats.getOrElse("domain", 0),
-      stats.getOrElse("field", 0)
-    ))
     _frontend.reporter.report(ProgramDefinitionsReport(collect(prog)))
   }
 }