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/dafny2/COST-verif-comp-2011-1-MaxArray.dfy                | 3 +++
 Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy.expect         | 2 ++
 Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy           | 3 +++
 Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect    | 2 ++
 Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy        | 3 +++
 Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy.expect | 2 ++
 Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy           | 3 +++
 Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy.expect    | 2 ++
 Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy        | 3 +++
 Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect | 2 ++
 Test/dafny2/Calculations.dfy                                   | 3 +++
 Test/dafny2/Calculations.dfy.expect                            | 2 ++
 Test/dafny2/Classics.dfy                                       | 3 +++
 Test/dafny2/Classics.dfy.expect                                | 2 ++
 Test/dafny2/Intervals.dfy                                      | 3 +++
 Test/dafny2/Intervals.dfy.expect                               | 2 ++
 Test/dafny2/MajorityVote.dfy                                   | 3 +++
 Test/dafny2/MajorityVote.dfy.expect                            | 2 ++
 Test/dafny2/MonotonicHeapstate.dfy                             | 3 +++
 Test/dafny2/MonotonicHeapstate.dfy.expect                      | 2 ++
 Test/dafny2/SegmentSum.dfy                                     | 3 +++
 Test/dafny2/SegmentSum.dfy.expect                              | 2 ++
 Test/dafny2/StoreAndRetrieve.dfy                               | 3 +++
 Test/dafny2/StoreAndRetrieve.dfy.expect                        | 2 ++
 Test/dafny2/TreeBarrier.dfy                                    | 3 +++
 Test/dafny2/TreeBarrier.dfy.expect                             | 2 ++
 Test/dafny2/TreeFill.dfy                                       | 3 +++
 Test/dafny2/TreeFill.dfy.expect                                | 2 ++
 Test/dafny2/TuringFactorial.dfy                                | 3 +++
 Test/dafny2/TuringFactorial.dfy.expect                         | 2 ++
 30 files changed, 75 insertions(+)
 create mode 100644 Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy.expect
 create mode 100644 Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
 create mode 100644 Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy.expect
 create mode 100644 Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy.expect
 create mode 100644 Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect
 create mode 100644 Test/dafny2/Calculations.dfy.expect
 create mode 100644 Test/dafny2/Classics.dfy.expect
 create mode 100644 Test/dafny2/Intervals.dfy.expect
 create mode 100644 Test/dafny2/MajorityVote.dfy.expect
 create mode 100644 Test/dafny2/MonotonicHeapstate.dfy.expect
 create mode 100644 Test/dafny2/SegmentSum.dfy.expect
 create mode 100644 Test/dafny2/StoreAndRetrieve.dfy.expect
 create mode 100644 Test/dafny2/TreeBarrier.dfy.expect
 create mode 100644 Test/dafny2/TreeFill.dfy.expect
 create mode 100644 Test/dafny2/TuringFactorial.dfy.expect

(limited to 'Test/dafny2')

diff --git a/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
index f67d7870..1a2b1f76 100644
--- a/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 /*
 Rustan Leino, 5 Oct 2011
 
diff --git a/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy.expect b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
index 1c01eefc..75a7822e 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 /*
 Rustan Leino, 5 Oct 2011
 
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
new file mode 100644
index 00000000..42fd56a5
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
index 8dd7bd2d..24cd541c 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // This Dafny program was inspired by Claude Marche's Why3ML program that solves
 // Challenge 2 of the COST Verification Competition.  It particular, it uses an
 // inductive datatype for the Tree data structure, and it uses a Contains function
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy.expect b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy.expect
new file mode 100644
index 00000000..790f6509
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
index 069baa61..72a22cfd 100644
--- a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 /*
 Rustan Leino, 5 Oct 2011
 
diff --git a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy.expect b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 30031e45..56f689da 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 /*
 Rustan Leino, 6 Oct 2011
 
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect
new file mode 100644
index 00000000..9d7e625f
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 25 verified, 0 errors
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index bbfab50d..10004332 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 /* Lists */
 // Here are some standard definitions of List and functions on Lists
 
diff --git a/Test/dafny2/Calculations.dfy.expect b/Test/dafny2/Calculations.dfy.expect
new file mode 100644
index 00000000..58598e51
--- /dev/null
+++ b/Test/dafny2/Calculations.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 31 verified, 0 errors
diff --git a/Test/dafny2/Classics.dfy b/Test/dafny2/Classics.dfy
index 68d9bf79..ddb7ccbe 100644
--- a/Test/dafny2/Classics.dfy
+++ b/Test/dafny2/Classics.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // A version of Turing's additive factorial program [Dr. A. Turing, "Checking a large routine",
 // In "Report of a Conference of High Speed Automatic Calculating Machines", pp. 67-69, 1949].
 
diff --git a/Test/dafny2/Classics.dfy.expect b/Test/dafny2/Classics.dfy.expect
new file mode 100644
index 00000000..790f6509
--- /dev/null
+++ b/Test/dafny2/Classics.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny2/Intervals.dfy b/Test/dafny2/Intervals.dfy
index f04f6411..df14c1e9 100644
--- a/Test/dafny2/Intervals.dfy
+++ b/Test/dafny2/Intervals.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // The RoundDown and RoundUp methods in this file are the ones in the Boogie
 // implementation Source/AbsInt/IntervalDomain.cs.
 
diff --git a/Test/dafny2/Intervals.dfy.expect b/Test/dafny2/Intervals.dfy.expect
new file mode 100644
index 00000000..790f6509
--- /dev/null
+++ b/Test/dafny2/Intervals.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index eb7ae766..51e5b968 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 // Rustan Leino, June 2012.
 // This file verifies an algorithm, due to Boyer and Moore, that finds the majority choice
 // among a sequence of votes, see http://www.cs.utexas.edu/~moore/best-ideas/mjrty/.
diff --git a/Test/dafny2/MajorityVote.dfy.expect b/Test/dafny2/MajorityVote.dfy.expect
new file mode 100644
index 00000000..d903c7c5
--- /dev/null
+++ b/Test/dafny2/MajorityVote.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 16 verified, 0 errors
diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy
index 4844086e..12e86018 100644
--- a/Test/dafny2/MonotonicHeapstate.dfy
+++ b/Test/dafny2/MonotonicHeapstate.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 module M0 {
   datatype Kind = Constant | Ident | Binary;
 
diff --git a/Test/dafny2/MonotonicHeapstate.dfy.expect b/Test/dafny2/MonotonicHeapstate.dfy.expect
new file mode 100644
index 00000000..f5e3b3dc
--- /dev/null
+++ b/Test/dafny2/MonotonicHeapstate.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 36 verified, 0 errors
diff --git a/Test/dafny2/SegmentSum.dfy b/Test/dafny2/SegmentSum.dfy
index dc67162b..ec2ad8b3 100644
--- a/Test/dafny2/SegmentSum.dfy
+++ b/Test/dafny2/SegmentSum.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 function Sum(a: seq<int>, s: int, t: int): int
   requires 0 <= s <= t <= |a|;
 {
diff --git a/Test/dafny2/SegmentSum.dfy.expect b/Test/dafny2/SegmentSum.dfy.expect
new file mode 100644
index 00000000..52595bf9
--- /dev/null
+++ b/Test/dafny2/SegmentSum.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 1cc906f3..6255ee96 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 abstract module A {
   import L = Library;
   class {:autocontracts} StoreAndRetrieve<Thing(==)> {
diff --git a/Test/dafny2/StoreAndRetrieve.dfy.expect b/Test/dafny2/StoreAndRetrieve.dfy.expect
new file mode 100644
index 00000000..39123c41
--- /dev/null
+++ b/Test/dafny2/StoreAndRetrieve.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny2/TreeBarrier.dfy b/Test/dafny2/TreeBarrier.dfy
index f4cc25d2..ffc75745 100644
--- a/Test/dafny2/TreeBarrier.dfy
+++ b/Test/dafny2/TreeBarrier.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 class Node {
   var left: Node;
   var right: Node;
diff --git a/Test/dafny2/TreeBarrier.dfy.expect b/Test/dafny2/TreeBarrier.dfy.expect
new file mode 100644
index 00000000..42fd56a5
--- /dev/null
+++ b/Test/dafny2/TreeBarrier.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
index 3328aca9..fdd73a1a 100644
--- a/Test/dafny2/TreeFill.dfy
+++ b/Test/dafny2/TreeFill.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 datatype Tree<T> = Leaf | Node(Tree, T, Tree)
 
 function Contains<T>(t: Tree, v: T): bool
diff --git a/Test/dafny2/TreeFill.dfy.expect b/Test/dafny2/TreeFill.dfy.expect
new file mode 100644
index 00000000..52595bf9
--- /dev/null
+++ b/Test/dafny2/TreeFill.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy
index 585c998e..9fb5e0ea 100644
--- a/Test/dafny2/TuringFactorial.dfy
+++ b/Test/dafny2/TuringFactorial.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
 function Factorial(n: nat): nat
 {
   if n == 0 then 1 else n * Factorial(n-1)
diff --git a/Test/dafny2/TuringFactorial.dfy.expect b/Test/dafny2/TuringFactorial.dfy.expect
new file mode 100644
index 00000000..52595bf9
--- /dev/null
+++ b/Test/dafny2/TuringFactorial.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
-- 
cgit v1.2.3