Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Changed computation of ghosts until pass 2 of resolution. | leino | 2015-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. | ||
* | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| | |||
* | Dafny: fixed unsoundness having to do with a function depending on the ↵ | Unknown | 2012-04-27 |
| | | | | allocation state | ||
* | Dafny: added optional range expressions to logical quantifiers, preparing ↵ | Rustan Leino | 2011-05-15 |
| | | | | for addition other other comprehensions (like set comprehension) | ||
* | Dafny: improved and corrected physical/ghost distinction | rustanleino | 2011-03-26 |
| | |||
* | Dafny: compile quantifiers | rustanleino | 2011-03-26 |
Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges |