From 607ef28aadb281ab61a2be493a637126e967a388 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 29 May 2014 21:41:00 +0200 Subject: Set up the same test infrastructure as in Boogie. --- Test/dafny1/Answer | 16 ++++++++-------- Test/dafny1/BDD.dfy | 5 +++-- Test/dafny1/BDD.dfy.expect | 2 ++ Test/dafny1/BinaryTree.dfy | 3 +++ Test/dafny1/BinaryTree.dfy.expect | 2 ++ Test/dafny1/Celebrity.dfy | 3 +++ Test/dafny1/Celebrity.dfy.expect | 2 ++ Test/dafny1/Cubes.dfy | 3 +++ Test/dafny1/Cubes.dfy.expect | 2 ++ Test/dafny1/ExtensibleArray.dfy | 3 +++ Test/dafny1/ExtensibleArray.dfy.expect | 2 ++ Test/dafny1/ExtensibleArrayAuto.dfy | 3 +++ Test/dafny1/ExtensibleArrayAuto.dfy.expect | 2 ++ Test/dafny1/FindZero.dfy | 3 +++ Test/dafny1/FindZero.dfy.expect | 2 ++ Test/dafny1/Induction.dfy | 3 +++ Test/dafny1/Induction.dfy.expect | 2 ++ Test/dafny1/KatzManna.dfy | 3 +++ Test/dafny1/KatzManna.dfy.expect | 2 ++ Test/dafny1/ListContents.dfy | 3 +++ Test/dafny1/ListContents.dfy.expect | 2 ++ Test/dafny1/ListCopy.dfy | 3 +++ Test/dafny1/ListCopy.dfy.expect | 2 ++ Test/dafny1/ListReverse.dfy | 2 ++ Test/dafny1/ListReverse.dfy.expect | 2 ++ Test/dafny1/MatrixFun.dfy | 3 +++ Test/dafny1/MatrixFun.dfy.expect | 2 ++ Test/dafny1/MoreInduction.dfy | 3 +++ Test/dafny1/MoreInduction.dfy.expect | 18 ++++++++++++++++++ Test/dafny1/PriorityQueue.dfy | 3 +++ Test/dafny1/PriorityQueue.dfy.expect | 2 ++ Test/dafny1/Queue.dfy | 3 +++ Test/dafny1/Queue.dfy.expect | 2 ++ Test/dafny1/Rippling.dfy | 3 +++ Test/dafny1/Rippling.dfy.expect | 2 ++ Test/dafny1/SchorrWaite-stages.dfy | 3 +++ Test/dafny1/SchorrWaite-stages.dfy.expect | 2 ++ Test/dafny1/SchorrWaite.dfy | 3 +++ Test/dafny1/SchorrWaite.dfy.expect | 2 ++ Test/dafny1/SeparationLogicList.dfy | 3 +++ Test/dafny1/SeparationLogicList.dfy.expect | 2 ++ Test/dafny1/Substitution.dfy | 3 +++ Test/dafny1/Substitution.dfy.expect | 2 ++ Test/dafny1/SumOfCubes.dfy | 3 +++ Test/dafny1/SumOfCubes.dfy.expect | 2 ++ Test/dafny1/TerminationDemos.dfy | 3 +++ Test/dafny1/TerminationDemos.dfy.expect | 2 ++ Test/dafny1/TreeDatatype.dfy | 3 +++ Test/dafny1/TreeDatatype.dfy.expect | 2 ++ Test/dafny1/UltraFilter.dfy | 3 +++ Test/dafny1/UltraFilter.dfy.expect | 2 ++ Test/dafny1/UnboundedStack.dfy | 3 +++ Test/dafny1/UnboundedStack.dfy.expect | 2 ++ Test/dafny1/pow2.dfy | 3 +++ Test/dafny1/pow2.dfy.expect | 2 ++ 55 files changed, 158 insertions(+), 10 deletions(-) create mode 100644 Test/dafny1/BDD.dfy.expect create mode 100644 Test/dafny1/BinaryTree.dfy.expect create mode 100644 Test/dafny1/Celebrity.dfy.expect create mode 100644 Test/dafny1/Cubes.dfy.expect create mode 100644 Test/dafny1/ExtensibleArray.dfy.expect create mode 100644 Test/dafny1/ExtensibleArrayAuto.dfy.expect create mode 100644 Test/dafny1/FindZero.dfy.expect create mode 100644 Test/dafny1/Induction.dfy.expect create mode 100644 Test/dafny1/KatzManna.dfy.expect create mode 100644 Test/dafny1/ListContents.dfy.expect create mode 100644 Test/dafny1/ListCopy.dfy.expect create mode 100644 Test/dafny1/ListReverse.dfy.expect create mode 100644 Test/dafny1/MatrixFun.dfy.expect create mode 100644 Test/dafny1/MoreInduction.dfy.expect create mode 100644 Test/dafny1/PriorityQueue.dfy.expect create mode 100644 Test/dafny1/Queue.dfy.expect create mode 100644 Test/dafny1/Rippling.dfy.expect create mode 100644 Test/dafny1/SchorrWaite-stages.dfy.expect create mode 100644 Test/dafny1/SchorrWaite.dfy.expect create mode 100644 Test/dafny1/SeparationLogicList.dfy.expect create mode 100644 Test/dafny1/Substitution.dfy.expect create mode 100644 Test/dafny1/SumOfCubes.dfy.expect create mode 100644 Test/dafny1/TerminationDemos.dfy.expect create mode 100644 Test/dafny1/TreeDatatype.dfy.expect create mode 100644 Test/dafny1/UltraFilter.dfy.expect create mode 100644 Test/dafny1/UnboundedStack.dfy.expect create mode 100644 Test/dafny1/pow2.dfy.expect (limited to 'Test/dafny1') diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 06cac03b..e60451c2 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -92,20 +92,20 @@ Dafny program verifier finished with 33 verified, 0 errors Dafny program verifier finished with 141 verified, 0 errors -------------------- MoreInduction.dfy -------------------- -MoreInduction.dfy(75,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(74,11): Related location: This is the postcondition that might not hold. +MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 -MoreInduction.dfy(80,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(79,21): Related location: This is the postcondition that might not hold. +MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 -MoreInduction.dfy(85,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(84,11): Related location: This is the postcondition that might not hold. +MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 -MoreInduction.dfy(90,1): Error BP5003: A postcondition might not hold on this return path. -MoreInduction.dfy(89,22): Related location: This is the postcondition that might not hold. +MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy index 3b6e478c..252164db 100644 --- a/Test/dafny1/BDD.dfy +++ b/Test/dafny1/BDD.dfy @@ -1,4 +1,5 @@ - +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" module SimpleBDD { @@ -57,4 +58,4 @@ module SimpleBDD b := node.b; } } -} \ No newline at end of file +} diff --git a/Test/dafny1/BDD.dfy.expect b/Test/dafny1/BDD.dfy.expect new file mode 100644 index 00000000..790f6509 --- /dev/null +++ b/Test/dafny1/BDD.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 5 verified, 0 errors diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy index ea915f69..edacd931 100644 --- a/Test/dafny1/BinaryTree.dfy +++ b/Test/dafny1/BinaryTree.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class IntSet { ghost var Contents: set; ghost var Repr: set; diff --git a/Test/dafny1/BinaryTree.dfy.expect b/Test/dafny1/BinaryTree.dfy.expect new file mode 100644 index 00000000..acae4413 --- /dev/null +++ b/Test/dafny1/BinaryTree.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 24 verified, 0 errors diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index a4043f4d..7e5ab205 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // Celebrity example, inspired by the Rodin tutorial static function method Knows(a: Person, b: Person): bool diff --git a/Test/dafny1/Celebrity.dfy.expect b/Test/dafny1/Celebrity.dfy.expect new file mode 100644 index 00000000..c87e2af2 --- /dev/null +++ b/Test/dafny1/Celebrity.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 10 verified, 0 errors diff --git a/Test/dafny1/Cubes.dfy b/Test/dafny1/Cubes.dfy index 1ada79fa..ecf26676 100644 --- a/Test/dafny1/Cubes.dfy +++ b/Test/dafny1/Cubes.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + method Cubes(a: array) requires a != null; modifies a; diff --git a/Test/dafny1/Cubes.dfy.expect b/Test/dafny1/Cubes.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny1/Cubes.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 2 verified, 0 errors diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index 57ac69c7..cb48e02b 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class ExtensibleArray { ghost var Contents: seq; ghost var Repr: set; diff --git a/Test/dafny1/ExtensibleArray.dfy.expect b/Test/dafny1/ExtensibleArray.dfy.expect new file mode 100644 index 00000000..f3a9c95f --- /dev/null +++ b/Test/dafny1/ExtensibleArray.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 11 verified, 0 errors diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy index b05af9f9..b2e5ecc4 100644 --- a/Test/dafny1/ExtensibleArrayAuto.dfy +++ b/Test/dafny1/ExtensibleArrayAuto.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class {:autocontracts} ExtensibleArray { ghost var Contents: seq; diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy.expect b/Test/dafny1/ExtensibleArrayAuto.dfy.expect new file mode 100644 index 00000000..f3a9c95f --- /dev/null +++ b/Test/dafny1/ExtensibleArrayAuto.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 11 verified, 0 errors diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy index c92dd065..f0eb6a60 100644 --- a/Test/dafny1/FindZero.dfy +++ b/Test/dafny1/FindZero.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + method FindZero(a: array) returns (r: int) requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i]; requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1]; diff --git a/Test/dafny1/FindZero.dfy.expect b/Test/dafny1/FindZero.dfy.expect new file mode 100644 index 00000000..42fd56a5 --- /dev/null +++ b/Test/dafny1/FindZero.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 8 verified, 0 errors diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 3585dde6..5dc398f3 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class IntegerInduction { // This class considers different ways of proving, for any natural n: // (SUM i in [0, n] :: i^3) == (SUM i in [0, n] :: i)^2 diff --git a/Test/dafny1/Induction.dfy.expect b/Test/dafny1/Induction.dfy.expect new file mode 100644 index 00000000..0d7d6532 --- /dev/null +++ b/Test/dafny1/Induction.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 33 verified, 0 errors diff --git a/Test/dafny1/KatzManna.dfy b/Test/dafny1/KatzManna.dfy index 60b70c1a..5987a82b 100644 --- a/Test/dafny1/KatzManna.dfy +++ b/Test/dafny1/KatzManna.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + method NinetyOne(x: int, ghost proveFunctionalPostcondition: bool) returns (z: int) ensures proveFunctionalPostcondition ==> z == if x > 101 then x-10 else 91; { diff --git a/Test/dafny1/KatzManna.dfy.expect b/Test/dafny1/KatzManna.dfy.expect new file mode 100644 index 00000000..4ef2de53 --- /dev/null +++ b/Test/dafny1/KatzManna.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 6 verified, 0 errors diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy index a8b4861d..b79d3308 100644 --- a/Test/dafny1/ListContents.dfy +++ b/Test/dafny1/ListContents.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class Node { var list: seq; var footprint: set>; diff --git a/Test/dafny1/ListContents.dfy.expect b/Test/dafny1/ListContents.dfy.expect new file mode 100644 index 00000000..249e77e5 --- /dev/null +++ b/Test/dafny1/ListContents.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 9 verified, 0 errors diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy index d5febfe0..4bffd51b 100644 --- a/Test/dafny1/ListCopy.dfy +++ b/Test/dafny1/ListCopy.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class Node { var nxt: Node; diff --git a/Test/dafny1/ListCopy.dfy.expect b/Test/dafny1/ListCopy.dfy.expect new file mode 100644 index 00000000..73ba063c --- /dev/null +++ b/Test/dafny1/ListCopy.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy index ef029b88..0837dd91 100644 --- a/Test/dafny1/ListReverse.dfy +++ b/Test/dafny1/ListReverse.dfy @@ -1,3 +1,5 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" class Node { var nxt: Node; diff --git a/Test/dafny1/ListReverse.dfy.expect b/Test/dafny1/ListReverse.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny1/ListReverse.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 2 verified, 0 errors diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy index 8f9d87ed..08c82132 100644 --- a/Test/dafny1/MatrixFun.dfy +++ b/Test/dafny1/MatrixFun.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + method MirrorImage(m: array2) requires m != null; modifies m; diff --git a/Test/dafny1/MatrixFun.dfy.expect b/Test/dafny1/MatrixFun.dfy.expect new file mode 100644 index 00000000..42fd56a5 --- /dev/null +++ b/Test/dafny1/MatrixFun.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 8 verified, 0 errors diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index 84c32fb3..d71c735f 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + datatype List = Nil | Cons(Node, List); datatype Node = Element(X) | Nary(List); diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect new file mode 100644 index 00000000..c8785e56 --- /dev/null +++ b/Test/dafny1/MoreInduction.dfy.expect @@ -0,0 +1,18 @@ +MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 +MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 +MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 +MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path. +MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 15 verified, 4 errors diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy index 0343cb07..4b2b2283 100644 --- a/Test/dafny1/PriorityQueue.dfy +++ b/Test/dafny1/PriorityQueue.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class PriorityQueue { var N: int; // capacity var n: int; // current size diff --git a/Test/dafny1/PriorityQueue.dfy.expect b/Test/dafny1/PriorityQueue.dfy.expect new file mode 100644 index 00000000..acae4413 --- /dev/null +++ b/Test/dafny1/PriorityQueue.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 24 verified, 0 errors diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy index 8396ec5c..c7892df6 100644 --- a/Test/dafny1/Queue.dfy +++ b/Test/dafny1/Queue.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // Queue.dfy // Dafny version of Queue.bpl // Rustan Leino, 2008 diff --git a/Test/dafny1/Queue.dfy.expect b/Test/dafny1/Queue.dfy.expect new file mode 100644 index 00000000..39123c41 --- /dev/null +++ b/Test/dafny1/Queue.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 4aaa9a38..0f32d529 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // Datatypes datatype Bool = False | True; diff --git a/Test/dafny1/Rippling.dfy.expect b/Test/dafny1/Rippling.dfy.expect new file mode 100644 index 00000000..5bec7f90 --- /dev/null +++ b/Test/dafny1/Rippling.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 141 verified, 0 errors diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 63c55506..7b2e7eda 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // Schorr-Waite algorithms, written and verified in Dafny. // Rustan Leino // Original version: 7 November 2008 diff --git a/Test/dafny1/SchorrWaite-stages.dfy.expect b/Test/dafny1/SchorrWaite-stages.dfy.expect new file mode 100644 index 00000000..d903c7c5 --- /dev/null +++ b/Test/dafny1/SchorrWaite-stages.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 16 verified, 0 errors diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 18adf491..de07fdcc 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // Rustan Leino // 7 November 2008 // Schorr-Waite and other marking algorithms, written and verified in Dafny. diff --git a/Test/dafny1/SchorrWaite.dfy.expect b/Test/dafny1/SchorrWaite.dfy.expect new file mode 100644 index 00000000..c87e2af2 --- /dev/null +++ b/Test/dafny1/SchorrWaite.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 10 verified, 0 errors diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy index 0b803afc..5a4d967f 100644 --- a/Test/dafny1/SeparationLogicList.dfy +++ b/Test/dafny1/SeparationLogicList.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // This file contains three variations of the separation-logic lseg linked-list example. // In this first variation, the auxiliary information about the contents represented by a linked list diff --git a/Test/dafny1/SeparationLogicList.dfy.expect b/Test/dafny1/SeparationLogicList.dfy.expect new file mode 100644 index 00000000..d903c7c5 --- /dev/null +++ b/Test/dafny1/SeparationLogicList.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 16 verified, 0 errors diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index ad39e3f2..10b70e09 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + datatype List = Nil | Cons(Expr, List); datatype Expr = diff --git a/Test/dafny1/Substitution.dfy.expect b/Test/dafny1/Substitution.dfy.expect new file mode 100644 index 00000000..b9a9bc89 --- /dev/null +++ b/Test/dafny1/Substitution.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 12 verified, 0 errors diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy index 7ed7ce9b..f1bcf6c7 100644 --- a/Test/dafny1/SumOfCubes.dfy +++ b/Test/dafny1/SumOfCubes.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class SumOfCubes { static function SumEmUp(n: int, m: int): int requires 0 <= n && n <= m; diff --git a/Test/dafny1/SumOfCubes.dfy.expect b/Test/dafny1/SumOfCubes.dfy.expect new file mode 100644 index 00000000..5f41963f --- /dev/null +++ b/Test/dafny1/SumOfCubes.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 17 verified, 0 errors diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 0aa36a10..f8fd2953 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class Example { method M(n: int) { diff --git a/Test/dafny1/TerminationDemos.dfy.expect b/Test/dafny1/TerminationDemos.dfy.expect new file mode 100644 index 00000000..f5019f3b --- /dev/null +++ b/Test/dafny1/TerminationDemos.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 14 verified, 0 errors diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy index a94283e6..763cef1b 100644 --- a/Test/dafny1/TreeDatatype.dfy +++ b/Test/dafny1/TreeDatatype.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // ------------------ generic list, non-generic tree datatype List = Nil | Cons(T, List); diff --git a/Test/dafny1/TreeDatatype.dfy.expect b/Test/dafny1/TreeDatatype.dfy.expect new file mode 100644 index 00000000..c87e2af2 --- /dev/null +++ b/Test/dafny1/TreeDatatype.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 10 verified, 0 errors diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index c78d5e81..a32e6e0b 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // ultra filter class UltraFilter { diff --git a/Test/dafny1/UltraFilter.dfy.expect b/Test/dafny1/UltraFilter.dfy.expect new file mode 100644 index 00000000..74590090 --- /dev/null +++ b/Test/dafny1/UltraFilter.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 19 verified, 0 errors diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy index dfc10327..58351ebb 100644 --- a/Test/dafny1/UnboundedStack.dfy +++ b/Test/dafny1/UnboundedStack.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + class UnboundedStack { ghost var representation: set; ghost var content: seq; diff --git a/Test/dafny1/UnboundedStack.dfy.expect b/Test/dafny1/UnboundedStack.dfy.expect new file mode 100644 index 00000000..b9a9bc89 --- /dev/null +++ b/Test/dafny1/UnboundedStack.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 12 verified, 0 errors diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy index bc23fb0b..ad6a9737 100644 --- a/Test/dafny1/pow2.dfy +++ b/Test/dafny1/pow2.dfy @@ -1,3 +1,6 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + // This is a Dafny adaptation of a Coq program by David Pichardie. function IsEven(n: int): bool diff --git a/Test/dafny1/pow2.dfy.expect b/Test/dafny1/pow2.dfy.expect new file mode 100644 index 00000000..42fd56a5 --- /dev/null +++ b/Test/dafny1/pow2.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 8 verified, 0 errors -- cgit v1.2.3