summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Allow modifies clauses for a "Main" method annotated with {:main} attribute.Gravatar qunyanm2016-03-31
* Fix issue 143. The list that stores the function fuel constants was declared asGravatar qunyanm2016-03-31
* MergeGravatar qunyanm2016-03-31
|\
* | Fix issue 75. Adjust the fuel for existentials to use more fuel in an assumeGravatar qunyanm2016-03-31
| * Add a wrapper for DafnyServer.exeGravatar Clément Pit--Claudel2016-03-30
|/
* Allow users to annontate a method as main with {:main} attribute. It’s an e...Gravatar qunyanm2016-03-28
* Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresGravatar qunyanm2016-03-28
* Update module export error messages. Also for "import Y" if there is at leastGravatar qunyanm2016-03-21
* Fix issue 93. Add per-function fuel setting that can be adjusted locally basedGravatar qunyanm2016-03-18
* Added test case to go with the recent fix of Issue #49 (changeset f354709009a5).Gravatar Rustan Leino2016-03-01
* MergeGravatar Rustan Leino2016-03-01
|\
* | Revised the $Is and $IsAlloc axioms for arrow terms. It is now possible toGravatar Rustan Leino2016-03-01
* | Added a return-value contractGravatar Rustan Leino2016-02-29
| * Revert change 1997 (bfe7c149bef1). IDE performance. Don't delay the resolverGravatar qunyanm2016-02-29
| * Fix issue 139. Allow bound variables in nested case patterns to shadow variablesGravatar qunyanm2016-02-26
|/
* MergeGravatar Rustan Leino2016-02-26
|\
* | Changes to CanCall assumptions:Gravatar Rustan Leino2016-02-26
| * Fix issue 138. Allow parenthese with the nullary constructor inGravatar qunyanm2016-02-26
| * Fix test failure. Print the resulting boogie code to a file insteadGravatar qunyanm2016-02-26
| * Fix issue 140. Move the initializion of _this before the TAIL_CALL_START label.Gravatar qunyanm2016-02-26
| * Fix issue 136. Less aggressive Lit wrap for assert/assume.Gravatar qunyanm2016-02-26
|/
* Update the test's .expect file since the fix is merged into boogie.Gravatar qunyanm2016-02-12
* Fix issue 132. The formal argument can't be assume to be allocated when aGravatar qunyanm2016-02-12
* Fix issue 134. Wrong variable was used in the loop.Gravatar qunyanm2016-02-11
* Fix issue 133. The return type for some compare operators was wrongly typedGravatar qunyanm2016-02-11
* Add /view:<view1, view2> option to filter module exports to be printed.Gravatar qunyanm2016-02-11
* MergeGravatar qunyanm2016-02-09
|\
* | Fix issue 131. Instead of crashing, report an error when an undefined member ofGravatar qunyanm2016-02-09
| * Renamed identifiers for increased geopolitical appealGravatar Rustan Leino2016-02-08
|/
* Fix issue 120. Need to wrap operations that are "lit lifted" and turned intoGravatar qunyanm2016-02-08
* Fix issue 124. Consider math operators that later turned into function callsGravatar qunyanm2016-02-08
* Last checkin checked in the wrong version of bug125.dfy. The failure part ofGravatar qunyanm2016-02-05
* Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.Gravatar qunyanm2016-02-05
* Fix issue 128. Change the translation of CanCallAssumption for let-such-thatGravatar qunyanm2016-02-04
* Fix issue 129. When looking for a constructor for which Dafny knows how toGravatar qunyanm2016-02-02
* Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"Gravatar qunyanm2016-02-02
* Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
* Revert Makefile to its prior settingsGravatar Richard L. Ford2016-01-29
* Add Dafny reference manualGravatar Richard L. Ford2016-01-27
* Fix build and test failures, cleanup grammar.Gravatar Richard L. Ford2016-01-27
* Add ExternNegative2.dfy.expect.Gravatar Richard L. Ford2016-01-27
* Implement 'extern' declaration modifier.Gravatar Richard L. Ford2016-01-27
* Fix issue 121. Don't split QuantifierExpr that are empty.Gravatar qunyanm2016-01-25
* Fix issue 122. Only generate autoTriggers for QuantifierExpr that are notGravatar qunyanm2016-01-25
* VS IDE performance - invoke dafny parser when the buffer hasn't changed forGravatar qunyanm2016-01-20
* Mark temps that are generated in the resolver as auto-generated identifiers soGravatar qunyanm2016-01-20
* Fix issue 117. Generate an error when the "opened" of an import doesn't matchGravatar qunyanm2016-01-08
* Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typedGravatar qunyanm2016-01-07
* Removed Contract.Requires from method overrides (preconditions of overrides a...Gravatar Rustan Leino2016-01-06
* Added flying robots example to test suiteGravatar Rustan Leino2016-01-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 21:00:46 +0000