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/vstte2012/BreadthFirstSearch.dfy        | 3 +++
 Test/vstte2012/BreadthFirstSearch.dfy.expect | 2 ++
 Test/vstte2012/Combinators.dfy               | 3 +++
 Test/vstte2012/Combinators.dfy.expect        | 2 ++
 Test/vstte2012/RingBuffer.dfy                | 3 +++
 Test/vstte2012/RingBuffer.dfy.expect         | 2 ++
 Test/vstte2012/RingBufferAuto.dfy            | 3 +++
 Test/vstte2012/RingBufferAuto.dfy.expect     | 2 ++
 Test/vstte2012/Tree.dfy                      | 3 +++
 Test/vstte2012/Tree.dfy.expect               | 2 ++
 Test/vstte2012/Two-Way-Sort.dfy              | 3 +++
 Test/vstte2012/Two-Way-Sort.dfy.expect       | 2 ++
 12 files changed, 30 insertions(+)
 create mode 100644 Test/vstte2012/BreadthFirstSearch.dfy.expect
 create mode 100644 Test/vstte2012/Combinators.dfy.expect
 create mode 100644 Test/vstte2012/RingBuffer.dfy.expect
 create mode 100644 Test/vstte2012/RingBufferAuto.dfy.expect
 create mode 100644 Test/vstte2012/Tree.dfy.expect
 create mode 100644 Test/vstte2012/Two-Way-Sort.dfy.expect

(limited to 'Test/vstte2012')

diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index f1181ed2..2d724b54 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 class BreadthFirstSearch<Vertex(==)>
 {
   // The following function is left uninterpreted (for the purpose of the 
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy.expect b/Test/vstte2012/BreadthFirstSearch.dfy.expect
new file mode 100644
index 00000000..39123c41
--- /dev/null
+++ b/Test/vstte2012/BreadthFirstSearch.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
index dcc2e22d..82bfc970 100644
--- a/Test/vstte2012/Combinators.dfy
+++ b/Test/vstte2012/Combinators.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // Problem 2 concerns an interpreter for the language of S and K combinators.
 
 // -----------------------------------------------------------------------------
diff --git a/Test/vstte2012/Combinators.dfy.expect b/Test/vstte2012/Combinators.dfy.expect
new file mode 100644
index 00000000..9d7e625f
--- /dev/null
+++ b/Test/vstte2012/Combinators.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 25 verified, 0 errors
diff --git a/Test/vstte2012/RingBuffer.dfy b/Test/vstte2012/RingBuffer.dfy
index e943b68d..4ddd7fe2 100644
--- a/Test/vstte2012/RingBuffer.dfy
+++ b/Test/vstte2012/RingBuffer.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 class RingBuffer<T>
 {
   // public view of the class:
diff --git a/Test/vstte2012/RingBuffer.dfy.expect b/Test/vstte2012/RingBuffer.dfy.expect
new file mode 100644
index 00000000..aeb37948
--- /dev/null
+++ b/Test/vstte2012/RingBuffer.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 13 verified, 0 errors
diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index aa7f171a..a9d36932 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 class {:autocontracts} RingBuffer<T>
 {
   // public view of the class:
diff --git a/Test/vstte2012/RingBufferAuto.dfy.expect b/Test/vstte2012/RingBufferAuto.dfy.expect
new file mode 100644
index 00000000..aeb37948
--- /dev/null
+++ b/Test/vstte2012/RingBufferAuto.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 13 verified, 0 errors
diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
index 1aa06408..0bfce265 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // The tree datatype
 datatype Tree = Leaf | Node(Tree, Tree);
 
diff --git a/Test/vstte2012/Tree.dfy.expect b/Test/vstte2012/Tree.dfy.expect
new file mode 100644
index 00000000..b06ff8fc
--- /dev/null
+++ b/Test/vstte2012/Tree.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 15 verified, 0 errors
diff --git a/Test/vstte2012/Two-Way-Sort.dfy b/Test/vstte2012/Two-Way-Sort.dfy
index 49ff29b4..92be95d2 100644
--- a/Test/vstte2012/Two-Way-Sort.dfy
+++ b/Test/vstte2012/Two-Way-Sort.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // This method is a slight generalization of the
 // code provided in the problem statement since it
 // is generic in the type of the array elements.
diff --git a/Test/vstte2012/Two-Way-Sort.dfy.expect b/Test/vstte2012/Two-Way-Sort.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/vstte2012/Two-Way-Sort.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 4 verified, 0 errors
-- 
cgit v1.2.3