dafny-lang · robin-aws · Mar 11, 2022 · Sep 2, 2021 · Sep 3, 2021 · Sep 3, 2021
diff --git a/.github/workflows/generate-test-report.yml b/.github/workflows/generate-test-report.yml
@@ -0,0 +1,16 @@
+name: 'Generate Test Report'
+on:
+  workflow_run:
+    workflows: ['tests']                     # runs after CI workflow
+    types:
+      - completed
+jobs:
+  report:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: dorny/test-reporter@v1
+      with:
+        artifact: verification-results
+        name: Verification Results
+        path: '*.trx'
+        reporter: dotnet-trx
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -18,10 +18,21 @@ jobs:
         with:
           dafny-version: "3.4.2"
 
-      - uses: actions/setup-python@v1
+      - name: Install Dafny report generator
+        run: dotnet tool install --global dafny-reportgenerator
 
       - name: Install lit 
         run: pip install lit OutputCheck
 
-      - name: Verify/Test Dafny code
-        run: lit --time-tests -v .
+      - name: Verify Dafny Code
+        run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' .
+
+      - name: Generate Report
+        run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-duration-seconds 10
+
+      - uses: actions/upload-artifact@v2  # upload test results
+        if: success() || failure()        # run this step even if previous step failed
+        with:
+          name: verification-results
+          path: '**/TestResults/*.trx'
+          if-no-files-found: error
diff --git a/.gitignore b/.gitignore
@@ -1 +1,2 @@
 **/Output/
+**/TestResults/
diff --git a/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy b/examples/LittleEndianNat/LittleEndianNatCustomExample.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:3 /noNLarith "%s"
 
 /*******************************************************************************
 *  Copyright by the contributors to the Dafny Project

diff --git a/examples/LittleEndianNat/LittleEndianNatExample.dfy b/examples/LittleEndianNat/LittleEndianNatExample.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:3 /noNLarith "%s"
 
 /*******************************************************************************
 *  Copyright by the contributors to the Dafny Project

diff --git a/examples/Wrappers.dfy b/examples/Wrappers.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:3 "%s"
 
 include "../src/Wrappers.dfy"
 

diff --git a/lit.site.cfg b/lit.site.cfg
@@ -120,9 +120,6 @@ dafnyExecutable += ' -useBaseNameForFileName'
 
 dafnyExecutable += ' -timeLimit:30'
 
-# The following option adjusts the exit codes of the Dafny executable
-dafnyExecutable += ' -countVerificationErrors:0'
-
 # We do not want output such as "Compiled program written to Foo.cs"
 # from the compilers, since that changes with the target language
 dafnyExecutable += ' -compileVerbose:0'

diff --git a/src/BoundedInts.dfy b/src/BoundedInts.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 module BoundedInts {
   const TWO_TO_THE_0:   int := 1

diff --git a/src/BoundedInts.dfy.expect b/src/BoundedInts.dfy.expect
diff --git a/src/Collections/Maps/Imaps.dfy b/src/Collections/Maps/Imaps.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, 

diff --git a/src/Collections/Maps/Imaps.dfy.expect b/src/Collections/Maps/Imaps.dfy.expect
diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, 

diff --git a/src/Collections/Maps/Maps.dfy.expect b/src/Collections/Maps/Maps.dfy.expect
diff --git a/src/Collections/Sequences/LittleEndianNat.dfy b/src/Collections/Sequences/LittleEndianNat.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) 2020 Secure Foundations Lab

diff --git a/src/Collections/Sequences/LittleEndianNat.dfy.expect b/src/Collections/Sequences/LittleEndianNat.dfy.expect
diff --git a/src/Collections/Sequences/LittleEndianNatConversions.dfy b/src/Collections/Sequences/LittleEndianNatConversions.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Copyright by the contributors to the Dafny Project

diff --git a/src/Collections/Sequences/LittleEndianNatConversions.dfy.expect b/src/Collections/Sequences/LittleEndianNatConversions.dfy.expect
diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original Copyright under the following: 

diff --git a/src/Collections/Sequences/Seq.dfy.expect b/src/Collections/Sequences/Seq.dfy.expect
diff --git a/src/Collections/Sets/Isets.dfy b/src/Collections/Sets/Isets.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original Copyright under the following: 

diff --git a/src/Collections/Sets/Isets.dfy.expect b/src/Collections/Sets/Isets.dfy.expect
diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original Copyright under the following: 

diff --git a/src/Collections/Sets/Sets.dfy.expect b/src/Collections/Sets/Sets.dfy.expect
diff --git a/src/Functions.dfy b/src/Functions.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original Copyright under the following: 

diff --git a/src/Functions.dfy.expect b/src/Functions.dfy.expect
diff --git a/src/Math.dfy b/src/Math.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Copyright by the contributors to the Dafny Project

diff --git a/src/Math.dfy.expect b/src/Math.dfy.expect
diff --git a/src/NonlinearArithmetic/DivMod.dfy b/src/NonlinearArithmetic/DivMod.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/DivMod.dfy.expect b/src/NonlinearArithmetic/DivMod.dfy.expect
diff --git a/src/NonlinearArithmetic/Internals/DivInternals.dfy b/src/NonlinearArithmetic/Internals/DivInternals.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Internals/DivInternals.dfy.expect b/src/NonlinearArithmetic/Internals/DivInternals.dfy.expect
diff --git a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy.expect b/src/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy.expect
diff --git a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy b/src/NonlinearArithmetic/Internals/GeneralInternals.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Internals/GeneralInternals.dfy.expect b/src/NonlinearArithmetic/Internals/GeneralInternals.dfy.expect
diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy b/src/NonlinearArithmetic/Internals/ModInternals.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy.expect b/src/NonlinearArithmetic/Internals/ModInternals.dfy.expect
diff --git a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy.expect b/src/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy.expect
diff --git a/src/NonlinearArithmetic/Internals/MulInternals.dfy b/src/NonlinearArithmetic/Internals/MulInternals.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Internals/MulInternals.dfy.expect b/src/NonlinearArithmetic/Internals/MulInternals.dfy.expect
diff --git a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy b/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy.expect b/src/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy.expect
diff --git a/src/NonlinearArithmetic/Mul.dfy b/src/NonlinearArithmetic/Mul.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Mul.dfy.expect b/src/NonlinearArithmetic/Mul.dfy.expect
diff --git a/src/NonlinearArithmetic/Power.dfy b/src/NonlinearArithmetic/Power.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Power.dfy.expect b/src/NonlinearArithmetic/Power.dfy.expect
diff --git a/src/NonlinearArithmetic/Power2.dfy b/src/NonlinearArithmetic/Power2.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 /noNLarith "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 /noNLarith "%s"
 
 /*******************************************************************************
 *  Original: Copyright (c) Microsoft Corporation

diff --git a/src/NonlinearArithmetic/Power2.dfy.expect b/src/NonlinearArithmetic/Power2.dfy.expect
diff --git a/src/Wrappers.dfy b/src/Wrappers.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %dafny /compile:0 "%s"
 
 /*******************************************************************************
 *  Copyright by the contributors to the Dafny Project

diff --git a/src/Wrappers.dfy.expect b/src/Wrappers.dfy.expect