Convert all tests

robin-aws · Jun 10, 2023 · 3ab861b · 3ab861b
1 parent 42255ac
commit 3ab861b
Show file tree

Hide file tree

Showing 469 changed files with 2,165 additions and 8,689 deletions.
diff --git a/Test/VerifyThis2015/Problem1.dfy b/Test/VerifyThis2015/Problem1.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment
 
 // Rustan Leino
 // 12 April 2015

diff --git a/Test/VerifyThis2015/Problem1.dfy.expect b/Test/VerifyThis2015/Problem1.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 18 verified, 0 errors
 true
 true
 false
diff --git a/Test/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment
 
 // Rustan Leino
 // 13 April 2015, and many subsequent enhancements and revisions

diff --git a/Test/VerifyThis2015/Problem2.dfy.expect b/Test/VerifyThis2015/Problem2.dfy.expect
@@ -1,2 +0,0 @@
-
-Dafny program verifier finished with 32 verified, 0 errors

diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment
 // Rustan Leino
 // 12 April 2015
 // VerifyThis 2015

diff --git a/Test/VerifyThis2015/Problem3.dfy.expect b/Test/VerifyThis2015/Problem3.dfy.expect
@@ -1,2 +0,0 @@
-
-Dafny program verifier finished with 18 verified, 0 errors

diff --git a/Test/c++/arrays.dfy b/Test/c++/arrays.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

diff --git a/Test/c++/arrays.dfy.expect b/Test/c++/arrays.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 9 verified, 0 errors
 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 
 17
 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22]

diff --git a/Test/c++/bit-vectors.dfy b/Test/c++/bit-vectors.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint64 = i:int | 0 <= i < 0x10000000000000000
 

diff --git a/Test/c++/bit-vectors.dfy.expect b/Test/c++/bit-vectors.dfy.expect
@@ -1,3 +1 @@
-
-Dafny program verifier finished with 6 verified, 0 errors
 084841024
diff --git a/Test/c++/class.dfy b/Test/c++/class.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

diff --git a/Test/c++/class.dfy.expect b/Test/c++/class.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 16 verified, 0 errors
 true true false
 103 102 102 106 105 105
 203 17 0 18 8 9 69 70

diff --git a/Test/c++/const.dfy b/Test/c++/const.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 module Holder {
  const x:bool := false

diff --git a/Test/c++/const.dfy.expect b/Test/c++/const.dfy.expect
@@ -1,2 +0,0 @@
-
-Dafny program verifier finished with 1 verified, 0 errors

diff --git a/Test/c++/datatypes.dfy b/Test/c++/datatypes.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

diff --git a/Test/c++/datatypes.dfy.expect b/Test/c++/datatypes.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 12 verified, 0 errors
 Case A: 42
 Case B: true
 This is expected

diff --git a/Test/c++/generic.dfy b/Test/c++/generic.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 class Test<T> {
  var t:T

diff --git a/Test/c++/generic.dfy.expect b/Test/c++/generic.dfy.expect
@@ -1,2 +0,0 @@
-
-Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/c++/hello.dfy b/Test/c++/hello.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 method Main() {
  print "Hello world\n";

diff --git a/Test/c++/hello.dfy.expect b/Test/c++/hello.dfy.expect
@@ -1,3 +1 @@
-
-Dafny program verifier finished with 0 verified, 0 errors
 Hello world
diff --git a/Test/c++/ints.dfy b/Test/c++/ints.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype sbyte = i:int | -0x80 <= i < 0x80
 newtype byte = i:int | 0 <= i < 0x100

diff --git a/Test/c++/ints.dfy.expect b/Test/c++/ints.dfy.expect
@@ -1,3 +1 @@
-
-Dafny program verifier finished with 15 verified, 0 errors
 Result is z = 42
diff --git a/Test/c++/recursion.dfy b/Test/c++/recursion.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

diff --git a/Test/c++/recursion.dfy.expect b/Test/c++/recursion.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 5 verified, 0 errors
 x
 !y
 3

diff --git a/Test/c++/returns.dfy b/Test/c++/returns.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint64 = i:int | 0 <= i < 0x10000000000000000
 

diff --git a/Test/c++/returns.dfy.expect b/Test/c++/returns.dfy.expect
@@ -1,3 +1 @@
-
-Dafny program verifier finished with 3 verified, 0 errors
 12
diff --git a/Test/c++/seqs.dfy b/Test/c++/seqs.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint8 = i:int | 0 <= i < 0x100
 newtype uint32 = i:int | 0 <= i < 0x100000000

diff --git a/Test/c++/seqs.dfy.expect b/Test/c++/seqs.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 11 verified, 0 errors
 Head second:2
 Trunc first:2
 Head trunc: This is expected

diff --git a/Test/c++/sets.dfy b/Test/c++/sets.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

diff --git a/Test/c++/sets.dfy.expect b/Test/c++/sets.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 8 verified, 0 errors
 Identity: This is expected
 ValuesIdentity: This is expected
 DiffIdentity: This is expected

diff --git a/Test/c++/while.dfy b/Test/c++/while.dfy
@@ -1,5 +1,4 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
 
 newtype uint32 = i:int | 0 <= i < 0x100000000
 

diff --git a/Test/c++/while.dfy.expect b/Test/c++/while.dfy.expect
@@ -1,5 +1,3 @@
-
-Dafny program verifier finished with 2 verified, 0 errors
 0
 1
 2

diff --git a/Test/comp/Arrays.dfy b/Test/comp/Arrays.dfy
@@ -1,10 +1,5 @@
-// RUN: %baredafny verify %args --relax-definite-assignment "%s" > "%t"
-// RUN: %baredafny run --unicode-char:false --no-verify --target=cs %args "%s" >> "%t"
-// RUN: %baredafny run --unicode-char:false --no-verify --target=js %args "%s" >> "%t"
-// RUN: %baredafny run --unicode-char:false --no-verify --target=go %args "%s" >> "%t"
-// RUN: %baredafny run --unicode-char:false --no-verify --target=java %args "%s" >> "%t"
-// RUN: %baredafny run --unicode-char:false --no-verify --target=py %args "%s" >> "%t"
-// RUN: %diff "%s.expect" "%t"
+// NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108
+// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment --unicode-char:false
 
 method LinearSearch(a: array<int>, key: int) returns (n: nat)
  ensures 0 <= n <= a.Length