diff options
Diffstat (limited to 'Test/dafny0/Modules0.dfy')
-rw-r--r-- | Test/dafny0/Modules0.dfy | 15 |
1 files changed, 15 insertions, 0 deletions
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); }
|