summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* MergeGravatar Rustan Leino2014-11-05
|\
* | Temporarily disabled one of the methods in NumberRepresentations.dfy -- this ...Gravatar leino2014-11-05
* | MergeGravatar leino2014-11-05
|\ \
| * | Refactored the generation of unique IDs for temporary variable names.Gravatar wuestholz2014-11-05
| * | Did some refactoring.Gravatar wuestholz2014-11-05
* | | MergeGravatar leino2014-11-04
|\| |
* | | MergeGravatar leino2014-11-04
|\ \ \
* | | | Refactored SnapshotableTrees a bit and made it verify in a reasonable amount ...Gravatar leino2014-11-04
| | * | Made dirty statements ghost.Gravatar chmaria2014-11-04
| | | * MergeGravatar Rustan Leino2014-11-03
| | | |\ | | | |/ | | |/|
| | | * Updated a test case for new syntax and convensionsGravatar Rustan Leino2014-11-03
| | * | Fixed test output after refactoring in Boogie.Gravatar wuestholz2014-11-03
| | * | Fixed test output after refactoring in Boogie.Gravatar wuestholz2014-11-02
| * | | MergeGravatar leino2014-11-01
| |\| |
| * | | Various DafnyPrelude.bpl cleanup.Gravatar leino2014-11-01
| | * | Minor fix in test dafny2/SnapshotableTrees.dfy.Gravatar chmaria2014-11-01
| | * | Added initial support for dirty while statements.Gravatar chmaria2014-11-01
| * | | Improved power of axioms Seq#FromArrayGravatar leino2014-10-31
| |/ /
| * | Allow assignment LHSs in a forall statement to be the same, so long as the th...Gravatar leino2014-10-30
| * | Resolve attributes of a forall statement only after bound variables have been...Gravatar leino2014-10-29
| |/
| * Fix bug in translation of 'new' for arraysGravatar Rustan Leino2014-10-29
| * MergeGravatar leino2014-10-28
| |\
| * | Fixed type-inference bug that could create cycles in proxy type graphGravatar leino2014-10-28
| * | Disallow automatic completion of type arguments to the LHS of datatype declar...Gravatar leino2014-10-28
| | * Create large stack in DafnyDriver.cs, before calling main,Gravatar Bryan Parno2014-10-28
| |/
| * Fixed a bug in the Substituter for datatype update expressions.Gravatar leino2014-10-28
| * Add a DafnyCC option that disables some of Dafny's cleverness to better match...Gravatar Bryan Parno2014-10-27
| * Fix datatype updates so chained updates don't explode performanceGravatar Bryan Parno2014-10-27
| * Make autoreqs of free requires not freeGravatar Bryan Parno2014-10-27
| * Allow autoReq in methods to generate auto-requirements on requiresGravatar Bryan Parno2014-10-27
| * Fixed range bug that was causing extension to sometimes crashGravatar Bryan Parno2014-10-27
| * Don't process opaque functions more than once when generating auto-reqsGravatar Bryan Parno2014-10-27
| * Fix fixup to opaque-function revealer to deal with zero-argument lemmasGravatar Bryan Parno2014-10-27
| * Fix autoreq handling of quantifiersGravatar Bryan Parno2014-10-27
| * Ensure that no file is processed twice, even if one command-line file is incl...Gravatar Bryan Parno2014-10-27
| * Added an attribute :timeLimitMultiplier for setting relative time outs.Gravatar Bryan Parno2014-10-27
| * Push the translation of user-supplied triggers deeperGravatar Bryan Parno2014-10-27
| * Add support for counting spec/impl/proof lines by supressing, e.g., ghost sta...Gravatar Bryan Parno2014-10-27
| * Add an option to allow automatically generated requirements to be printedGravatar Bryan Parno2014-10-27
| * Even with noCheating enabled, don't check included files or methods marked wi...Gravatar Bryan Parno2014-10-27
| * Allow non-ghost axioms in order to model trusted external calls,Gravatar Bryan Parno2014-10-27
| * MergeGravatar leino2014-10-25
| |\
| * | Marked "free" as soon-to-be-deprecatedGravatar leino2014-10-25
| * | Made semi-colons are specification clauses optional. In a future version, th...Gravatar leino2014-10-25
| | * Add an option to use reduce Z3's knowledge of non-linear arithmetic.Gravatar Bryan Parno2014-10-24
| |/
| * Allow underscores in numeric literals (and in field/destructor names that are...Gravatar leino2014-10-23
|/
* Changed version to 1.9.1.11022Gravatar leino2014-10-21
* When guessing decreases clauses for loops, convert numeric values to their ul...Gravatar leino2014-10-21
* Fixed crash in inferred descreases clauses involving newtypes.Gravatar leino2014-10-21
* Changed version to 1.9.1.11021Gravatar leino2014-10-21