Merge

4 files changed, 25 insertions, 5 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index fdfdf823..1eb22708 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -645,6 +645,12 @@ Dafny program verifier finished with 7 verified, 1 error
 -------------------- Modules0.dfy --------------------

 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

 Modules0.dfy(13,7): Error: module T named among imports does not exist

+Modules0.dfy(196,8): Error: Duplicate name of top-level declaration: WazzupA

+Modules0.dfy(197,11): Error: Duplicate name of top-level declaration: WazzupA

+Modules0.dfy(198,7): Error: Duplicate name of top-level declaration: WazzupA

+Modules0.dfy(201,7): Error: Duplicate name of top-level declaration: WazzupB

+Modules0.dfy(202,8): Error: Duplicate name of top-level declaration: WazzupB

+Modules0.dfy(203,11): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G

 Modules0.dfy(51,8): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)

 Modules0.dfy(62,9): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)

@@ -656,7 +662,7 @@ Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification
 Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts

 Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context

 Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context

-13 resolution/type errors detected in Modules0.dfy

+19 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 17500c97..d8bffce4 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -136,7 +136,7 @@ class A {
   }

 }

 

-class B { }

+type B;

 

 // -------------------------------

 

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index c14aece6..4eb02905 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -188,3 +188,17 @@ function NestedMatch3(tree: Tree): int
       case Nil => 0

       case Cons(h1,l1,r1) => h + h0 + h1

 }

+

+// ---------------------- more duplicates

+

+module Wazzup {

+  class WazzupA { }

+  class WazzupA { }  // error: duplicate type

+  datatype WazzupA = W_A_X;  // error: duplicate type

+  type WazzupA;  // error: duplicate type

+

+  type WazzupB;

+  type WazzupB;  // error: duplicate type

+  class WazzupB { }  // error: duplicate type

+  datatype WazzupB = W_B_X;  // error: duplicate type

+}

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 211afd83..677e6e70 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -278,11 +278,11 @@ function mirror(t: Tree): Tree
 // Function parameters

 

 // Dafny currently does not support passing functions as arguments.  To simulate

-// arbitrary functions, the following type (declared as a class) and Apply function

-// play the role of applying some prescribed function (here, an instance of the class)

+// arbitrary functions, the following type and Apply function play the role of

+// applying some prescribed function (here, a value of the type)

 // to some argument.

 

-class FunctionValue { }

+type FunctionValue;

 function Apply(f: FunctionValue, x: Nat): Nat  // this function is left uninterpreted

 

 // The following functions stand for the constant "false" and "true" functions,