From 607ef28aadb281ab61a2be493a637126e967a388 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Thu, 29 May 2014 21:41:00 +0200
Subject: Set up the same test infrastructure as in Boogie.

---
 Test/VSI-Benchmarks/b1.dfy        | 3 +++
 Test/VSI-Benchmarks/b1.dfy.expect | 2 ++
 Test/VSI-Benchmarks/b2.dfy        | 2 ++
 Test/VSI-Benchmarks/b2.dfy.expect | 2 ++
 Test/VSI-Benchmarks/b3.dfy        | 3 +++
 Test/VSI-Benchmarks/b3.dfy.expect | 2 ++
 Test/VSI-Benchmarks/b4.dfy        | 3 +++
 Test/VSI-Benchmarks/b4.dfy.expect | 2 ++
 Test/VSI-Benchmarks/b5.dfy        | 3 ++-
 Test/VSI-Benchmarks/b5.dfy.expect | 2 ++
 Test/VSI-Benchmarks/b6.dfy        | 2 ++
 Test/VSI-Benchmarks/b6.dfy.expect | 2 ++
 Test/VSI-Benchmarks/b7.dfy        | 3 +++
 Test/VSI-Benchmarks/b7.dfy.expect | 2 ++
 Test/VSI-Benchmarks/b8.dfy        | 3 +++
 Test/VSI-Benchmarks/b8.dfy.expect | 2 ++
 16 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 Test/VSI-Benchmarks/b1.dfy.expect
 create mode 100644 Test/VSI-Benchmarks/b2.dfy.expect
 create mode 100644 Test/VSI-Benchmarks/b3.dfy.expect
 create mode 100644 Test/VSI-Benchmarks/b4.dfy.expect
 create mode 100644 Test/VSI-Benchmarks/b5.dfy.expect
 create mode 100644 Test/VSI-Benchmarks/b6.dfy.expect
 create mode 100644 Test/VSI-Benchmarks/b7.dfy.expect
 create mode 100644 Test/VSI-Benchmarks/b8.dfy.expect

(limited to 'Test/VSI-Benchmarks')

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
-- 
cgit v1.2.3