summaryrefslogtreecommitdiff
path: root/Test/dafny4/set-compr.dfy.expect
Commit message (Collapse)AuthorAge
* Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
| | | | Moved all bounds discovery to resolution pass 1.
* Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
| | | | | | | Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions.
* Fix issue 61. Decreases are by default in ghost context. Therefore,Gravatar qunyanm2015-03-31
dontCareAboutCompilation flag should be set to false in the ResolveOpts.