Set up the same test infrastructure as in Boogie.

16 files changed, 37 insertions, 1 deletions

diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index 3bd2bf43..4b1852ae 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Spec# and Boogie and Chalice:  The program will be

 // the same, except that these languages do not check

 // for any kind of termination.  Also, in Spec#, there

diff --git a/Test/VSI-Benchmarks/b1.dfy.expect b/Test/VSI-Benchmarks/b1.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/VSI-Benchmarks/b1.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index a7f1ca9a..7966d2ea 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -1,3 +1,5 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

 

 class Benchmark2 {

   method BinarySearch(a: array<int>, key: int) returns (result: int)

diff --git a/Test/VSI-Benchmarks/b2.dfy.expect b/Test/VSI-Benchmarks/b2.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/VSI-Benchmarks/b2.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 6 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 5df25612..91044397 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Note:  We used integers instead of a generic Comparable type, because

 // Dafny has no way of saying that the Comparable type's AtMost function

 // is total and transitive.

diff --git a/Test/VSI-Benchmarks/b3.dfy.expect b/Test/VSI-Benchmarks/b3.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/VSI-Benchmarks/b3.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ae5b0511..92975e11 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 /*

 	This test works with Z3 4.3 (on Win8 x64). Other versions ... who knows.

 */

diff --git a/Test/VSI-Benchmarks/b4.dfy.expect b/Test/VSI-Benchmarks/b4.dfy.expect
new file mode 100644
index 00000000..f3a9c95f
--- /dev/null
+++ b/Test/VSI-Benchmarks/b4.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 53d82207..d735e6c7 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -1,4 +1,5 @@
-

+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

 

 class Queue<T> {

   var head: Node<T>;

diff --git a/Test/VSI-Benchmarks/b5.dfy.expect b/Test/VSI-Benchmarks/b5.dfy.expect
new file mode 100644
index 00000000..39123c41
--- /dev/null
+++ b/Test/VSI-Benchmarks/b5.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index fda9ca74..660fe85c 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -1,3 +1,5 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

 

 class Collection<T> {

   ghost var footprint:set<object>;

diff --git a/Test/VSI-Benchmarks/b6.dfy.expect b/Test/VSI-Benchmarks/b6.dfy.expect
new file mode 100644
index 00000000..73727958
--- /dev/null
+++ b/Test/VSI-Benchmarks/b6.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 21 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 8d218ec9..301ef00d 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Edited B6 to include GetChar and PutChar 

 

 //This is the Queue from Benchmark 3.

diff --git a/Test/VSI-Benchmarks/b7.dfy.expect b/Test/VSI-Benchmarks/b7.dfy.expect
new file mode 100644
index 00000000..5add7af7
--- /dev/null
+++ b/Test/VSI-Benchmarks/b7.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 23 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 7608ed85..5ab75e7a 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Benchmark 8

 

 // A dictionary is a mapping between words and sequences of words

diff --git a/Test/VSI-Benchmarks/b8.dfy.expect b/Test/VSI-Benchmarks/b8.dfy.expect
new file mode 100644
index 00000000..6ba9b9bc
--- /dev/null
+++ b/Test/VSI-Benchmarks/b8.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 42 verified, 0 errors