diff options
| author |  leino <unknown> | 2014-11-06 14:16:25 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-11-06 14:16:25 -0800 |
| commit | 41ae0ef413e2806e1ee753f56de2152938902fac (patch) | |
| tree | 5e244485b41f61c4e1f76605920e24a87cb657ec /Test/dafny0/ModifyStmt.dfy | |
| parent | ae0982daf944f7e79fc6b8d73afd1f62f943d7ed (diff) | |
Started fixing a number of LL(1) warnings
Disallow empty modifies/reads clauses (this eliminates some LL(1) warnings)
Require modify statement to take a nonempty list of frame expressions
Diffstat (limited to 'Test/dafny0/ModifyStmt.dfy')
| -rw-r--r-- | Test/dafny0/ModifyStmt.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/ModifyStmt.dfy b/Test/dafny0/ModifyStmt.dfy index 6d041b43..00b39e7a 100644 --- a/Test/dafny0/ModifyStmt.dfy +++ b/Test/dafny0/ModifyStmt.dfy @@ -16,7 +16,7 @@ class MyClass { modify {this}, this, {this}, S;
modify this;
modify {:myAttribute} {:another true} {this}, this, S;
- modify ;
+ modify {} ;
}
method N()
|