summaryrefslogtreecommitdiff
path: root/Test/dafny0/ModifyStmt.dfy
Commit message (Collapse)AuthorAge
* Started fixing a number of LL(1) warningsGravatar leino2014-11-06
| | | | | Disallow empty modifies/reads clauses (this eliminates some LL(1) warnings) Require modify statement to take a nonempty list of frame expressions
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Changed an error from a verification error to a syntactic (resolution) errorGravatar Rustan Leino2014-04-04
|
* Added "modify Frame { Body }" statement.Gravatar Rustan Leino2014-04-04
|
* Added "modify" statement.Gravatar Rustan Leino2014-04-03
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.