summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Release for unstableHEADmasterBenjamin Barenblat2016-06-05
* Patch Dafny to use the system Z3Benjamin Barenblat2016-06-05
* Update debian/gbp.confBenjamin Barenblat2016-06-05
* Update debian/copyrightBenjamin Barenblat2016-06-05
* Update debian/copyrightBenjamin Barenblat2016-06-05
* Update debian/controlBenjamin Barenblat2016-06-05
* Bump debian/changelogBenjamin Barenblat2016-06-05
* Merge commit 'df5c5f5'Benjamin Barenblat2016-05-30
|\
* | Update dependencies and Standards-VersionBenjamin Barenblat2016-04-06
| * New version number 1.9.7.30401, for binary release on Codeplex and Rise4fun.leino2016-04-01
| * Mergeleino2016-04-01
| |\
| * | New test file, for recursive and iterative versions of McCarthy's 91 functionleino2016-04-01
| * | New test case, proving monad laws for listsleino2016-04-01
| | * Fix issue 148. The results for sign comparison for BigRational.CompareTo wasqunyanm2016-04-01
| |/
| * Allow modifies clauses for a "Main" method annotated with {:main} attribute.qunyanm2016-03-31
| * Fix issue 143. The list that stores the function fuel constants was declared asqunyanm2016-03-31
| * Mergequnyanm2016-03-31
| |\
| * | Fix issue 75. Adjust the fuel for existentials to use more fuel in an assumequnyanm2016-03-31
| | * Add a wrapper for DafnyServer.exeClément Pit--Claudel2016-03-30
| |/
| * Allow users to annontate a method as main with {:main} attribute. It’s an e...qunyanm2016-03-28
| * Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresqunyanm2016-03-28
| * Update module export error messages. Also for "import Y" if there is at leastqunyanm2016-03-21
| * Fix issue 93. Add per-function fuel setting that can be adjusted locally basedqunyanm2016-03-18
| * Added test case to go with the recent fix of Issue #49 (changeset f354709009a5).Rustan Leino2016-03-01
| * MergeRustan Leino2016-03-01
| |\
| * | Revised the $Is and $IsAlloc axioms for arrow terms. It is now possible toRustan Leino2016-03-01
| * | Added a return-value contractRustan Leino2016-02-29
| | * Revert change 1997 (bfe7c149bef1). IDE performance. Don't delay the resolverqunyanm2016-02-29
| | * Fix issue 139. Allow bound variables in nested case patterns to shadow variablesqunyanm2016-02-26
| |/
| * MergeRustan Leino2016-02-26
| |\
| * | Changes to CanCall assumptions:Rustan Leino2016-02-26
| | * Fix issue 138. Allow parenthese with the nullary constructor inqunyanm2016-02-26
| | * Fix test failure. Print the resulting boogie code to a file insteadqunyanm2016-02-26
| | * Fix issue 140. Move the initializion of _this before the TAIL_CALL_START label.qunyanm2016-02-26
| | * Fix issue 136. Less aggressive Lit wrap for assert/assume.qunyanm2016-02-26
| |/
| * Update the test's .expect file since the fix is merged into boogie.qunyanm2016-02-12
| * Fix issue 132. The formal argument can't be assume to be allocated when aqunyanm2016-02-12
| * Fix issue 134. Wrong variable was used in the loop.qunyanm2016-02-11
| * Fix issue 133. The return type for some compare operators was wrongly typedqunyanm2016-02-11
| * Add /view:<view1, view2> option to filter module exports to be printed.qunyanm2016-02-11
| * Mergequnyanm2016-02-09
| |\
| * | Fix issue 131. Instead of crashing, report an error when an undefined member ofqunyanm2016-02-09
| | * Renamed identifiers for increased geopolitical appealRustan Leino2016-02-08
| |/
| * Fix issue 120. Need to wrap operations that are "lit lifted" and turned intoqunyanm2016-02-08
| * Fix issue 124. Consider math operators that later turned into function callsqunyanm2016-02-08
| * Last checkin checked in the wrong version of bug125.dfy. The failure part ofqunyanm2016-02-05
| * Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.qunyanm2016-02-05
| * Fix issue 128. Change the translation of CanCallAssumption for let-such-thatqunyanm2016-02-04
| * Fix issue 129. When looking for a constructor for which Dafny knows how toqunyanm2016-02-02
| * Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"qunyanm2016-02-02