Merge

3 files changed, 22 insertions, 4 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0ee81392..4bdea760 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -490,9 +490,12 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela
 Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)

 Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)

 Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts

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

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

-10 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts

+Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts

+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

 

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

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

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index adce71a8..59052ac2 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -121,6 +121,21 @@ class Ghosty {
   ghost method Theorem(a: int) { }

 }

 

+var SomeField: int;

+

+method SpecialFunctions()

+  modifies this;

+{

+  SomeField := SomeField + 4;

+  var a := old(SomeField);  // error: old can only be used in ghost contexts

+  var b := fresh(this);  // error: fresh can only be used in ghost contexts

+  var c := allocated(this);  // error: allocated can only be used in ghost contexts

+  if (fresh(this)) {  // this guard makes the if statement a ghost statement

+    ghost var x := old(SomeField);  // this is a ghost context, so it's okay

+    ghost var y := allocated(this);  // this is a ghost context, so it's okay

+  }

+}

+

 // ---------------------- illegal match expressions ---------------

 

 datatype Tree { Nil; Cons(int, Tree, Tree); }

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 93bd4b65..6b7ce9b9 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -60,7 +60,7 @@ datatype List<T> {
   Cons(nat, T, List<T>);

 }

 

-method MatchIt(list: List<bool>) returns (k: nat)

+method MatchIt(list: List<object>) returns (k: nat)

 {

   match (list) {

     case Nil =>