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/dafny3/CachedContainer.dfy               | 3 +++
 Test/dafny3/CachedContainer.dfy.expect        | 2 ++
 Test/dafny3/CalcExample.dfy                   | 3 +++
 Test/dafny3/CalcExample.dfy.expect            | 2 ++
 Test/dafny3/Dijkstra.dfy                      | 3 +++
 Test/dafny3/Dijkstra.dfy.expect               | 2 ++
 Test/dafny3/Filter.dfy                        | 3 +++
 Test/dafny3/Filter.dfy.expect                 | 2 ++
 Test/dafny3/GenericSort.dfy                   | 3 +++
 Test/dafny3/GenericSort.dfy.expect            | 2 ++
 Test/dafny3/InductionVsCoinduction.dfy        | 3 +++
 Test/dafny3/InductionVsCoinduction.dfy.expect | 2 ++
 Test/dafny3/InfiniteTrees.dfy                 | 3 +++
 Test/dafny3/InfiniteTrees.dfy.expect          | 2 ++
 Test/dafny3/Iter.dfy                          | 3 +++
 Test/dafny3/Iter.dfy.expect                   | 2 ++
 Test/dafny3/OpaqueTrees.dfy                   | 3 +++
 Test/dafny3/OpaqueTrees.dfy.expect            | 2 ++
 Test/dafny3/Paulson.dfy                       | 3 +++
 Test/dafny3/Paulson.dfy.expect                | 2 ++
 Test/dafny3/SetIterations.dfy                 | 3 +++
 Test/dafny3/SetIterations.dfy.expect          | 2 ++
 Test/dafny3/SimpleCoinduction.dfy             | 3 +++
 Test/dafny3/SimpleCoinduction.dfy.expect      | 2 ++
 Test/dafny3/SimpleInduction.dfy               | 3 +++
 Test/dafny3/SimpleInduction.dfy.expect        | 2 ++
 Test/dafny3/Streams.dfy                       | 3 +++
 Test/dafny3/Streams.dfy.expect                | 2 ++
 Test/dafny3/WideTrees.dfy                     | 3 +++
 Test/dafny3/WideTrees.dfy.expect              | 2 ++
 Test/dafny3/Zip.dfy                           | 3 +++
 Test/dafny3/Zip.dfy.expect                    | 2 ++
 32 files changed, 80 insertions(+)
 create mode 100644 Test/dafny3/CachedContainer.dfy.expect
 create mode 100644 Test/dafny3/CalcExample.dfy.expect
 create mode 100644 Test/dafny3/Dijkstra.dfy.expect
 create mode 100644 Test/dafny3/Filter.dfy.expect
 create mode 100644 Test/dafny3/GenericSort.dfy.expect
 create mode 100644 Test/dafny3/InductionVsCoinduction.dfy.expect
 create mode 100644 Test/dafny3/InfiniteTrees.dfy.expect
 create mode 100644 Test/dafny3/Iter.dfy.expect
 create mode 100644 Test/dafny3/OpaqueTrees.dfy.expect
 create mode 100644 Test/dafny3/Paulson.dfy.expect
 create mode 100644 Test/dafny3/SetIterations.dfy.expect
 create mode 100644 Test/dafny3/SimpleCoinduction.dfy.expect
 create mode 100644 Test/dafny3/SimpleInduction.dfy.expect
 create mode 100644 Test/dafny3/Streams.dfy.expect
 create mode 100644 Test/dafny3/WideTrees.dfy.expect
 create mode 100644 Test/dafny3/Zip.dfy.expect

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy
index 6ac5ff2f..18c12862 100644
--- a/Test/dafny3/CachedContainer.dfy
+++ b/Test/dafny3/CachedContainer.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // give the method signatures and specs
 abstract module M0 {
   class {:autocontracts} Container<T(==)> {
diff --git a/Test/dafny3/CachedContainer.dfy.expect b/Test/dafny3/CachedContainer.dfy.expect
new file mode 100644
index 00000000..c6c90498
--- /dev/null
+++ b/Test/dafny3/CachedContainer.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 47 verified, 0 errors
diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index dcd41077..2782d049 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 function f(x: int, y: int): int
 
 ghost method Associativity(x: int, y: int, z: int)
diff --git a/Test/dafny3/CalcExample.dfy.expect b/Test/dafny3/CalcExample.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/dafny3/CalcExample.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index ef94f291..e90687e0 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // Example taken from:
 // Edsger W. Dijkstra: Heuristics for a Calculational Proof. Inf. Process. Lett. (IPL) 53(3):141-143 (1995)
 // Transcribed into Dafny by Valentin Wüstholz and Nadia Polikarpova.
diff --git a/Test/dafny3/Dijkstra.dfy.expect b/Test/dafny3/Dijkstra.dfy.expect
new file mode 100644
index 00000000..b9a9bc89
--- /dev/null
+++ b/Test/dafny3/Dijkstra.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 12 verified, 0 errors
diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 4b39876a..0d9a7231 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 codatatype Stream<T> = Cons(head: T, tail: Stream);
 
 function Tail(s: Stream, n: nat): Stream
diff --git a/Test/dafny3/Filter.dfy.expect b/Test/dafny3/Filter.dfy.expect
new file mode 100644
index 00000000..91aa9b47
--- /dev/null
+++ b/Test/dafny3/Filter.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 43 verified, 0 errors
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index 10589e5a..53d98bc2 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 abstract module TotalOrder {
   type T // the type to be compared
   static predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
diff --git a/Test/dafny3/GenericSort.dfy.expect b/Test/dafny3/GenericSort.dfy.expect
new file mode 100644
index 00000000..f5e3b3dc
--- /dev/null
+++ b/Test/dafny3/GenericSort.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 36 verified, 0 errors
diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 5c5c0412..47754036 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // A definition of a co-inductive datatype Stream, whose values are possibly
 // infinite lists.
 codatatype Stream<T> = SNil | SCons(head: T, tail: Stream<T>);
diff --git a/Test/dafny3/InductionVsCoinduction.dfy.expect b/Test/dafny3/InductionVsCoinduction.dfy.expect
new file mode 100644
index 00000000..c192e07c
--- /dev/null
+++ b/Test/dafny3/InductionVsCoinduction.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 20 verified, 0 errors
diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy
index 32a868bb..030443c0 100644
--- a/Test/dafny3/InfiniteTrees.dfy
+++ b/Test/dafny3/InfiniteTrees.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // Here is the usual definition of possibly infinite lists, along with a function Tail(s, n), which drops
 // n heads from s, and two lemmas that prove properties of Tail.
 
diff --git a/Test/dafny3/InfiniteTrees.dfy.expect b/Test/dafny3/InfiniteTrees.dfy.expect
new file mode 100644
index 00000000..79f8263d
--- /dev/null
+++ b/Test/dafny3/InfiniteTrees.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 88 verified, 0 errors
diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy
index c5e8f3a3..5ada6f5b 100644
--- a/Test/dafny3/Iter.dfy
+++ b/Test/dafny3/Iter.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 class List<T> {
   ghost var Contents: seq<T>;
   ghost var Repr: set<object>;
diff --git a/Test/dafny3/Iter.dfy.expect b/Test/dafny3/Iter.dfy.expect
new file mode 100644
index 00000000..b06ff8fc
--- /dev/null
+++ b/Test/dafny3/Iter.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 15 verified, 0 errors
diff --git a/Test/dafny3/OpaqueTrees.dfy b/Test/dafny3/OpaqueTrees.dfy
index a08d0b68..53540c1d 100644
--- a/Test/dafny3/OpaqueTrees.dfy
+++ b/Test/dafny3/OpaqueTrees.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 datatype Tree<T> = Leaf(T) | Node(Tree, Tree)
 
 function {:opaque} size(t: Tree): nat
diff --git a/Test/dafny3/OpaqueTrees.dfy.expect b/Test/dafny3/OpaqueTrees.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/dafny3/OpaqueTrees.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index 37586ec7..735963a5 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // The following are Dafny versions from Section 8 of
 // "Mechanizing Coinduction and Corecursion in Higher-order Logic"
 // by Lawrence C. Paulson, 1996.
diff --git a/Test/dafny3/Paulson.dfy.expect b/Test/dafny3/Paulson.dfy.expect
new file mode 100644
index 00000000..ab18d98e
--- /dev/null
+++ b/Test/dafny3/Paulson.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 28 verified, 0 errors
diff --git a/Test/dafny3/SetIterations.dfy b/Test/dafny3/SetIterations.dfy
index 8b095b5f..2319078a 100644
--- a/Test/dafny3/SetIterations.dfy
+++ b/Test/dafny3/SetIterations.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 function Count<T>(s: set<T>): int
 {
   if s == {} then 0 else
diff --git a/Test/dafny3/SetIterations.dfy.expect b/Test/dafny3/SetIterations.dfy.expect
new file mode 100644
index 00000000..aeb37948
--- /dev/null
+++ b/Test/dafny3/SetIterations.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 13 verified, 0 errors
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index b5b0c8bf..5be5c569 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 codatatype Stream<T> = Cons(head: T, tail: Stream);
 codatatype IList<T> = Nil | ICons(head: T, tail: IList);
 
diff --git a/Test/dafny3/SimpleCoinduction.dfy.expect b/Test/dafny3/SimpleCoinduction.dfy.expect
new file mode 100644
index 00000000..58598e51
--- /dev/null
+++ b/Test/dafny3/SimpleCoinduction.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 31 verified, 0 errors
diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 700b531c..29660099 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 /*
   The well-known Fibonacci function defined in Dafny.  The postcondition of
   method FibLemma states a property about Fib, and the body of the method is
diff --git a/Test/dafny3/SimpleInduction.dfy.expect b/Test/dafny3/SimpleInduction.dfy.expect
new file mode 100644
index 00000000..b9a9bc89
--- /dev/null
+++ b/Test/dafny3/SimpleInduction.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 12 verified, 0 errors
diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index 1d566545..c51f30d4 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // ----- Stream
 
 codatatype Stream<T> = Nil | Cons(head: T, tail: Stream);
diff --git a/Test/dafny3/Streams.dfy.expect b/Test/dafny3/Streams.dfy.expect
new file mode 100644
index 00000000..c90560b0
--- /dev/null
+++ b/Test/dafny3/Streams.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 52 verified, 0 errors
diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy
index 3fa99256..0245ef9f 100644
--- a/Test/dafny3/WideTrees.dfy
+++ b/Test/dafny3/WideTrees.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 codatatype Stream<T> = SNil | SCons(head: T, tail: Stream)
 datatype Tree = Node(children: Stream<Tree>)
 
diff --git a/Test/dafny3/WideTrees.dfy.expect b/Test/dafny3/WideTrees.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/dafny3/WideTrees.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 629861f9..9b1d3671 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 /*
 Here, we define infinite streams with some functions and prove a few
 properties, drawing from:
diff --git a/Test/dafny3/Zip.dfy.expect b/Test/dafny3/Zip.dfy.expect
new file mode 100644
index 00000000..acae4413
--- /dev/null
+++ b/Test/dafny3/Zip.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 24 verified, 0 errors
-- 
cgit v1.2.3