Set up the same test infrastructure as in Boogie.

12 files changed, 30 insertions, 0 deletions

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