| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | New version number 1.9.7.30401, for binary release on Codeplex and Rise4fun. |  leino | 2016-04-01 |
| | | | | | Changed copyright date to include 2016. | ||
| * | Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires | qunyanm | 2016-03-28 |
| | | | | | | it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. | ||
| * | Add /view:<view1, view2> option to filter module exports to be printed. | qunyanm | 2016-02-11 |
| | | |||
| * | Made /rewriteFocalPredicates:1 the default | Rustan Leino | 2015-10-02 |
| | | |||
| * | Hover text includes #[_k-1] suffix for terms rewritten in prefix ↵ | Rustan Leino | 2015-10-02 |
| | | | | | | | | predicates/lemmas (this fixes an item from the wishlist). Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?). Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1]. | ||
| * | fix for warnings related to deprecated z3 options (please update to the ↵ |  Michael Lowell Roberts | 2015-09-22 |
| | | | | | latest revision of z3). | ||
| * | Only print extraneous comments if asked. | Michael Lowell Roberts | 2015-09-17 |
| | | |||
| * | Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience) |  Clément Pit--Claudel | 2015-08-27 |
| | | | | | | | Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it looks for one in Binaries/z3.exe (mostly for backwards-compatibility with already set-up source installations). | ||
| * | Merge. | Clément Pit--Claudel | 2015-08-19 |
| |\ | | | | | | | | | Changes that were needed included preventing the InductionRewriter from iterating on a SplitQuantifier and using the new error reporting engine. | ||
| * | | Use a nice warning symbol in some warning messages | Clément Pit--Claudel | 2015-08-18 |
| | | | | | | | | | | | This is useful because trigger-related messages can contain quite a bit of information, especially if they include info about multiple split quantifiers. | ||
| | * | Moved discovery of induction variables into a Rewriter. | leino | 2015-08-11 |
| |/ | | | | | Generate warnings for malformed :induction arguments. Removed the functionality that allowed induction on 'this'. | ||
| * | Add a Linux z3 binary to the repo, and use that or z3.exe based on the OS | Clément Pit--Claudel | 2015-07-31 |
| | | |||
| * | Merge my autoTriggers work into the master branch | Clément Pit--Claudel | 2015-07-17 |
| |\ | | | | | | | | | This contains trigger related things under the autoTriggers flag (disabled by default), and some bug-fixes and cleanups that are already enabled. | ||
| * | | Clean up a few thing and set proper defaults before merging | Clément Pit--Claudel | 2015-07-16 |
| | | | |||
| * | | Add /printTooltips and /autoTriggers to the CLI | Clément Pit--Claudel | 2015-07-13 |
| | | | |||
| | * | [IronDafny] implemented workaround for "import opened" bug(s). | Michael Lowell Roberts | 2015-07-13 |
| | | | |||
| | * | Added command-line option /warnShadowing, which emits warnings if variables ↵ | Rustan Leino | 2015-07-02 |
| | | | | | | | | | shadow other variables (Issue #86) | ||
| | * | Add code to calculate various interesting statistics about Dafny files. |  Bryan Parno | 2015-07-01 |
| |/ | |||
| * | added -optimize option to compiler. | Michael Lowell Roberts | 2015-06-12 |
| | | |||
| * | Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero. | Clément Pit--Claudel | 2015-06-07 |
| | | | | | | The test suite relies on error codes all being zero (except for preprocessing errors), so add a flag for that (as suggested in a source comment). | ||
| * | Changed version to 1.9.3.20406 and updated copyright year to include 2015. | leino | 2015-04-06 |
| | | |||
| * | Minor change due to a change in Boogie | wuestholz | 2015-01-13 |
| | | |||
| * | Added command-line switch /allowGlobals to simplify transition from language ↵ | leino | 2015-01-07 |
| | | | | | changes introduced in changeset c56031307ac1 | ||
| * | Add a DafnyCC option that disables some of Dafny's cleverness to better ↵ | Bryan Parno | 2014-10-27 |
| | | | | | match DafnyCC's capabilities | ||
| * | Add support for counting spec/impl/proof lines by supressing, e.g., ghost ↵ | Bryan Parno | 2014-10-27 |
| | | | | | statements | ||
| * | Add an option to allow automatically generated requirements to be printed | Bryan Parno | 2014-10-27 |
| | | | | | to a file, making them easier to inspect and manipulate. | ||
| * | Add an option to use reduce Z3's knowledge of non-linear arithmetic. | Bryan Parno | 2014-10-24 |
| | | | | | Results in more manual work, but it also produces more predictable behavior. | ||
| * | Added /compile:3, which compiles in memory and then executes the program (if ↵ | Rustan Leino | 2014-01-13 |
| | | | | | there is a Main and there are no errors). Primarily intended for use with rise4fun. | ||
| * | Produce "tail recursive" hover text in the IDE only for methods that are ↵ | Rustan Leino | 2013-12-13 |
| | | | | | recursive | ||
| * | Add a command-line option to disable include directives. | Bryan Parno | 2013-12-13 |
| | | |||
| * | Fixed printing of Dafny version number. | Rustan Leino | 2013-01-23 |
| | | |||
| * | Put all sources under \Source directory |  Rustan Leino | 2012-10-04 |
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |