| Commit message (Expand) | Author | Age |
* | Merge | leino | 2014-11-04 |
|\ |
|
| * | Made dirty statements ghost. | chmaria | 2014-11-04 |
* | | Merge | leino | 2014-11-01 |
|\| |
|
* | | Various DafnyPrelude.bpl cleanup. | leino | 2014-11-01 |
| * | 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 |
|\ |
|