summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* | Don't inline opaque functions.Gravatar Rustan Leino2013-12-17
| * MergeGravatar Rustan Leino2013-12-16
| |\ | |/ |/|
| * Fixed bug where free conditions preceded checked conditions (for inlined pred...Gravatar Rustan Leino2013-12-16
* | Pass assert/assume attributes down to BoogieGravatar Rustan Leino2013-12-16
* | Fix build failure due to changes in Boogie.Gravatar wuestholz2013-12-16
* | MergeGravatar Bryan Parno2013-12-13
|\ \
* | | Add support for the :axiom attribute for ghost methods.Gravatar Bryan Parno2013-12-13
| * | Produce "tail recursive" hover text in the IDE only for methods that are recu...Gravatar Rustan Leino2013-12-13
* | | Added support for opaque function definitions, indicated via the {:opaque} at...Gravatar Bryan Parno2013-12-13
|/ /
* | Add a command-line option to disable include directives.Gravatar Bryan Parno2013-12-13
* | Fixed emacs coloring to not color things that are only substrings of symbolsGravatar Bryan Parno2013-12-12
* | MergeGravatar Rustan Leino2013-12-11
|\ \
* | | Refactored the calling of rewritersGravatar Rustan Leino2013-12-11
| * | Fix build failures due to changes in Boogie.Gravatar wuestholz2013-12-11
| * | Add support for the "include" keyword, which accepts a (possibly relative) pathGravatar Bryan Parno2013-12-10
| * | Update an 'Answer' file.Gravatar wuestholz2013-12-10
| * | Change a test program to verify faster (by a factor of 10-25).Gravatar wuestholz2013-12-10
|/ /
* | Fixed a bug in the Boogie generated for refinement checks (now that there is ...Gravatar Rustan Leino2013-12-09
* | Fixed bug reported as discussion:472216 on dafny.codeplex.comGravatar Rustan Leino2013-12-09
* | Fix some things due to changes in Boogie (execution engine API, 'UnivBackPred...Gravatar wuestholz2013-12-09
* | Updated an 'Answer' file.Gravatar wuestholz2013-12-03
* | Fixed build failures due to changes in Boogie.Gravatar wuestholz2013-11-23
|/
* Use full name of type in compilation errorGravatar Rustan Leino2013-11-18
* MergeGravatar Rustan Leino2013-11-18
|\
| * Added support for attributes on variable declarations.Gravatar wuestholz2013-11-18
* | Let compiler complain about body-less functions and methods, even if these ar...Gravatar Rustan Leino2013-11-14
|/
* Fixed build failure due to changes in Boogie.Gravatar wuestholz2013-10-28
* Fixed typo in build scriptGravatar Rustan Leino2013-08-06
* Removed old keyword "choose"Gravatar Rustan Leino2013-08-06
* Bumped version to 1.7.0, to be released as a binary and on rise4fun.Gravatar wuestholz2013-08-06
* Removed code for an unreachable caseGravatar Rustan Leino2013-08-06
* MergeGravatar Rustan Leino2013-08-06
|\
* | Allow calls to side-effect-free ghost methods from expressionsGravatar Rustan Leino2013-08-06
* | Merged PredicateExpr and CalcExpr into a single StmtExprGravatar Rustan Leino2013-08-06
| * Updated 'PrepareDafnyZip.bat'.Gravatar wuestholz2013-08-05
| * DafnyExtension: Use the same version number as Dafny (unfortunately needs to ...Gravatar wuestholz2013-08-05
* | Added hover text ("additional information") in places where co-predicates pro...Gravatar Rustan Leino2013-08-04
* | Allow co-predicates to be wrapped inside bounded existential quantifiersGravatar Rustan Leino2013-08-04
* | Added hover text ("additional information") in places where co-methods provid...Gravatar Rustan Leino2013-08-04
* | Unified function/method context heightsGravatar Rustan Leino2013-08-04
* | Disallow call-graph clusters that mix co-methods / prefix methods with other ...Gravatar Rustan Leino2013-08-04
* | Set up call-graph to keep track of edges between functions and methods. (To ...Gravatar Rustan Leino2013-08-04
| * DafnyExtension: Fixed issue with visual elements being accessed by non-owning...Gravatar wuestholz2013-08-04
| * DafnyExtension: Did some refactoring and added a description to error states.Gravatar wuestholz2013-08-03
|/
* Introduced keywords "lemma" (like a "ghost method", but not allowed to have a...Gravatar Rustan Leino2013-08-02
* More and improved CaptureState infoGravatar Rustan Leino2013-08-02
* Merge adjustmentsGravatar Rustan Leino2013-08-02
|\
* | Added activation antecedents for co-predicate / prefix predicate axioms.Gravatar Rustan Leino2013-08-02
* | Changed the encoding of recursive functions. Previous, three hardcoded layer...Gravatar Rustan Leino2013-08-02
| * DafnyExtension: Fixed a minor issue in the error selection.Gravatar wuestholz2013-08-01