| Commit message (Expand) | Author | Age |
|---|
| * | Added initial support for dirty while statements. |  chmaria | 2014-11-01 |
| * | Allow assignment LHSs in a forall statement to be the same, so long as the th... | leino | 2014-10-30 |
| * | Resolve attributes of a forall statement only after bound variables have been... | leino | 2014-10-29 |
| * | Fix bug in translation of 'new' for arrays | Rustan Leino | 2014-10-29 |
| * | Merge | leino | 2014-10-28 |
| |\ |
|
| * | | Fixed type-inference bug that could create cycles in proxy type graph | leino | 2014-10-28 |
| * | | Disallow automatic completion of type arguments to the LHS of datatype declar... | leino | 2014-10-28 |
| | * | Create large stack in DafnyDriver.cs, before calling main, |  Bryan Parno | 2014-10-28 |
| |/ |
|
| * | Fixed a bug in the Substituter for datatype update expressions. | leino | 2014-10-28 |
| * | Add a DafnyCC option that disables some of Dafny's cleverness to better match... | Bryan Parno | 2014-10-27 |
| * | Fix datatype updates so chained updates don't explode performance | Bryan Parno | 2014-10-27 |
| * | Make autoreqs of free requires not free | Bryan Parno | 2014-10-27 |
| * | Allow autoReq in methods to generate auto-requirements on requires | Bryan Parno | 2014-10-27 |
| * | Fixed range bug that was causing extension to sometimes crash | Bryan Parno | 2014-10-27 |
| * | Don't process opaque functions more than once when generating auto-reqs | Bryan Parno | 2014-10-27 |
| * | Fix fixup to opaque-function revealer to deal with zero-argument lemmas | Bryan Parno | 2014-10-27 |
| * | Fix autoreq handling of quantifiers | Bryan Parno | 2014-10-27 |
| * | Ensure that no file is processed twice, even if one command-line file is incl... | Bryan Parno | 2014-10-27 |
| * | Added an attribute :timeLimitMultiplier for setting relative time outs. | Bryan Parno | 2014-10-27 |
| * | Push the translation of user-supplied triggers deeper | Bryan Parno | 2014-10-27 |
| * | Add support for counting spec/impl/proof lines by supressing, e.g., ghost sta... | Bryan Parno | 2014-10-27 |
| * | Add an option to allow automatically generated requirements to be printed | Bryan Parno | 2014-10-27 |
| * | Even with noCheating enabled, don't check included files or methods marked wi... | Bryan Parno | 2014-10-27 |
| * | Allow non-ghost axioms in order to model trusted external calls, | Bryan Parno | 2014-10-27 |
| * | Merge | leino | 2014-10-25 |
| |\ |
|
| * | | Marked "free" as soon-to-be-deprecated | leino | 2014-10-25 |
| * | | Made semi-colons are specification clauses optional. In a future version, th... | leino | 2014-10-25 |
| | * | Add an option to use reduce Z3's knowledge of non-linear arithmetic. | Bryan Parno | 2014-10-24 |
| |/ |
|
| * | Allow underscores in numeric literals (and in field/destructor names that are... | leino | 2014-10-23 |
| * | Changed version to 1.9.1.11022 | leino | 2014-10-21 |
| * | When guessing decreases clauses for loops, convert numeric values to their ul... | leino | 2014-10-21 |
| * | Fixed crash in inferred descreases clauses involving newtypes. | leino | 2014-10-21 |
| * | Changed version to 1.9.1.11021 | leino | 2014-10-21 |
| * | Comparisons and well-founded order of char | leino | 2014-10-21 |
| * | Add char literals. | leino | 2014-10-20 |
| * | Merge | leino | 2014-10-20 |
| |\ |
|
| * | | Added types "char" and "string" (the latter being a synonym for "seq<char>"). | leino | 2014-10-20 |
| | * | DafnyExtension: Fixed minor issue in the menu. | wuestholz | 2014-10-19 |
| |/ |
|
| * | Updated version to 1.9.0.11016. This version is going on rise4fun.com. | leino | 2014-10-16 |
| * | Merge | leino | 2014-10-14 |
| |\ |
|
| | * | Minor change | wuestholz | 2014-10-14 |
| * | | Fixed parsing crash on malformed chaining with == and !! | leino | 2014-10-09 |
| * | | Print arrow types with parentheses around the domain type when the domain con... | leino | 2014-10-09 |
| * | | Stricter rules about that types need to be completely resolved. | leino | 2014-10-08 |
| |/ |
|
| * | Allow any integer-based type, not just 'int', in the following places: | leino | 2014-10-06 |
| * | Merge | leino | 2014-09-29 |
| |\ |
|
| * | | Shorter wait-for-idle time in the Dafny IDE | leino | 2014-09-29 |
| | * | DafnyExtension: Made it not log the pretty-printed program. | wuestholz | 2014-09-28 |
| | * | DafnyExtension: minor change due to change in Boogie | wuestholz | 2014-09-28 |
| | * | Did more refactoring. | wuestholz | 2014-09-23 |
chmaria
Bryan Parno