From 27241e69516368f116baea922938d1cb10570d85 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 11 May 2011 17:25:34 -0700
Subject: Dafny: * added missing error checking for ghost-vs-physical contexts
 (e.g., use of the "old" keyword) * check that arrays are not null when
 accessed * added dafny1/FindZero.dfy test case

---
 Test/dafny0/Answer       |  9 ++++++---
 Test/dafny0/Modules0.dfy | 15 +++++++++++++++
 Test/dafny0/NatTypes.dfy |  2 +-
 3 files changed, 22 insertions(+), 4 deletions(-)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1ac8fc1c..afa88a47 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -483,9 +483,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 =>
-- 
cgit v1.2.3