diff options
| author |  Rustan Leino <unknown> | 2014-04-03 18:28:56 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-03 18:28:56 -0700 |
| commit | cd206ac033a1e369277f824dd3a13eca32f0396c (patch) | |
| tree | 23f3d5863237de9def3f5c10cb4974dc3191ef14 /Test/dafny0/ResolutionErrors.dfy | |
| parent | 7c64906cd2eb3d0258b29e91bdc861743a05ff42 (diff) | |
Added "modify" statement.
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index f7a7ed3e..1eb69a8e 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -826,3 +826,13 @@ module ObjectType { o := co; // error
}
}
+
+// ------------------ modify statment ---------------------------
+
+class ModifyStatementClass {
+ var x: int;
+ method M()
+ {
+ modify x; // error: type error
+ }
+}
|