Set up the same test infrastructure as in Boogie.

30 files changed, 75 insertions, 0 deletions

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