Set up the same test infrastructure as in Boogie.

10 files changed, 25 insertions, 0 deletions

diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy
index 3db9bf72..d7989539 100644
--- a/Test/VSComp2010/Problem1-SumMax.dfy
+++ b/Test/VSComp2010/Problem1-SumMax.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // VSComp 2010, problem 1, compute the sum and max of the elements of an array and prove

 // that 'sum <= N * max'.

 // Rustan Leino, 18 August 2010.

diff --git a/Test/VSComp2010/Problem1-SumMax.dfy.expect b/Test/VSComp2010/Problem1-SumMax.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/VSComp2010/Problem1-SumMax.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors

diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index 327703e7..23c25733 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // VSComp 2010, problem 2, compute the inverse 'B' of a permutation 'A' and prove that 'B' is

 // indeed an inverse of 'A' (or at least prove that 'B' is injective).

 // Rustan Leino, 31 August 2010.

diff --git a/Test/VSComp2010/Problem2-Invert.dfy.expect b/Test/VSComp2010/Problem2-Invert.dfy.expect
new file mode 100644
index 00000000..76f19e0d
--- /dev/null
+++ b/Test/VSComp2010/Problem2-Invert.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy
index 3d24255d..61bb2e3a 100644
--- a/Test/VSComp2010/Problem3-FindZero.dfy
+++ b/Test/VSComp2010/Problem3-FindZero.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // VSComp 2010, problem 3, find a 0 in a linked list and return how many nodes were skipped

 // until the first 0 (or end-of-list) was found.

 // Rustan Leino, 18 August 2010.

diff --git a/Test/VSComp2010/Problem3-FindZero.dfy.expect b/Test/VSComp2010/Problem3-FindZero.dfy.expect
new file mode 100644
index 00000000..76f19e0d
--- /dev/null
+++ b/Test/VSComp2010/Problem3-FindZero.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index 2d4111db..21fcc053 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // VSComp 2010, problem 4, N queens

 // Rustan Leino, 31 August 2010, updated 24 March 2011.

 //

diff --git a/Test/VSComp2010/Problem4-Queens.dfy.expect b/Test/VSComp2010/Problem4-Queens.dfy.expect
new file mode 100644
index 00000000..249e77e5
--- /dev/null
+++ b/Test/VSComp2010/Problem4-Queens.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 9 verified, 0 errors

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index 0e141927..930758a5 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // VSComp 2010, problem 5, double-ended queue.

 // Rustan Leino, 18 August 2010.

 //

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect
new file mode 100644
index 00000000..73727958
--- /dev/null
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 21 verified, 0 errors