Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Merge | leino | 2015-10-26 | |
| |\ | ||||
| * | | Fixed location of blue dots to appear after semi-colons, not just before them. | leino | 2015-10-26 | |
| | | | ||||
| | * | DafnyExtension: Add menu item for automatic induction (mainly developed by ↵ | wuestholz | 2015-10-26 | |
| |/ | | | | | | | Rustan). | |||
| * | Make /autoTriggers:1 be the default in Visual Studio | leino | 2015-10-24 | |
| | | ||||
| * | In Visual Studio, be willing to display both resolution warnings and ↵ | leino | 2015-10-24 | |
| | | | | | | | | | | | | verification errors (previously, verification errors were masked by resolution warnings) | |||
| * | In method and iterator specifications, inline top-level predicates (except | leino | 2015-10-24 | |
| | | | | | | | | protected predicated in cross-module calls) like in other places. | |||
| * | Introduced new datatype update syntax: D.(f := E) | leino | 2015-10-23 | |
| | | | | | | | | | | The old syntax, D[f := E], is still supported for a short while, but generates a warning about that syntax being deprecated. The new syntax also supports multiple updates: D.(f := E0, g := E1, h := E2) | |||
| * | Refactored resolution of datatype updates, preparing for a change of syntax | leino | 2015-10-23 | |
| | | ||||
| * | Fixed bug introduced in changeset 7ebdf9cd4154 | leino | 2015-10-22 | |
| | | ||||
| * | Improve Dafny's ability to find fueled functions by checking the function ↵ | Bryan Parno | 2015-10-19 | |
| | | | | | | | | | | | | itself, as well as the signature and body of other functions. | |||
| * | Version 1.9.6.21012 | Rustan Leino | 2015-10-12 | |
| | | ||||
| * | Merge | Rustan Leino | 2015-10-12 | |
| |\ | ||||
| | * | DafnyExtension: Re-added assembly reference. | wuestholz | 2015-10-08 | |
| | | | ||||
| | * | DafnyExtension: Fix concurrency issue. | wuestholz | 2015-10-08 | |
| | | | ||||
| | * | Make the Dafny extension compile on VS 2015 without any old versions. | wuestholz | 2015-10-08 | |
| | | | ||||
| | * | Add vsix to releases and fix invalid path separators in packaging script | Clément Pit--Claudel | 2015-10-08 | |
| | | | ||||
| * | | Renamed ExistentialGuards... to BindingGuards... | Rustan Leino | 2015-10-07 | |
| |/ | ||||
| * | Use /env:0 to avoid full pathnames in test output | Rustan Leino | 2015-10-06 | |
| | | ||||
| * | Implemented resolution, verification, and (poorly performing) compilation of ↵ | leino | 2015-10-05 | |
| | | | | | | | | | | | | | | existential if guards. Fixed bugs in ghost checks involving comprehensions and attributes. Added SubstituteBoundedPool method. | |||
| * | Parsing and pretty printing of the new "existential guards" of the two kinds ↵ | leino | 2015-10-03 | |
| | | | | | | | | of "if" statements. | |||
| * | 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]. | |||
| * | Fixed latent crash of hovertext/outlining with include. | Rustan Leino | 2015-10-02 | |
| | | | | | | | | (This also undoes two previous attempted fixes, which had accidentally disabled some outlining and hovertexts.) | |||
| * | Removed some unused code. | Rustan Leino | 2015-09-30 | |
| | | ||||
| * | Merge | leino | 2015-09-29 | |
| |\ | ||||
| | * | Fix two test cases that failed if the path to "DafnySever.exe" contained spaces. | wuestholz | 2015-09-30 | |
| | | | ||||
| | * | Fix the build. | wuestholz | 2015-09-29 | |
| | | | ||||
| * | | Merge | leino | 2015-09-28 | |
| |\ \ | ||||
| | * | | Merge | leino | 2015-09-28 | |
| | |\| | ||||
| * | | | Removed specContextOnly parameter from ResolveStatement. | leino | 2015-09-28 | |
| | | | | | | | | | | | | | | | | Moved all bounds discovery to resolution pass 1. | |||
| * | | | Removed the 'inSpecOnlyContext' map that had been part of the resolution of | leino | 2015-09-28 | |
| | | | | | | | | | | | | | | | | | | | | 'break' statements out of ghost structures. This is now done in pass 2 by looking at the .IsGhost field of the target statement. | |||
| * | | | Renamed CheckIsNonGhost to CheckIsCompilable. | leino | 2015-09-28 | |
| | | | | ||||
| * | | | Removed more traces of the previous resolution checks that happened during ↵ | leino | 2015-09-28 | |
| | | | | | | | | | | | | | | | | | | | | | | | | pass 0. Fixed resolution of specification components of alternative loops. | |||
| * | | | Additional tests | leino | 2015-09-28 | |
| | | | | ||||
| * | | | Whitespace changes in test file | leino | 2015-09-28 | |
| | | | | ||||
| * | | | Improvements in proofs | leino | 2015-09-28 | |
| | | | | ||||
| * | | | Changed computation of ghosts until pass 2 of resolution. | leino | 2015-09-28 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions. | |||
| | | * | merge heads | Michael Lowell Roberts | 2015-09-23 | |
| | | |\ | ||||
| | | * | | fixed bugs related to identifying newtypes as types of integers and reals. | Michael Lowell Roberts | 2015-09-23 | |
| | | | | | ||||
| | | | * | Revert part of 1899 (47fd7d09d605, "Fix a check that occasionally led to ...") | Clément Pit--Claudel | 2015-09-23 | |
| | | |/ | | | | | | | | | | | | | That commit accidentally overwrote the dafny shell script for Linux and MacOS. | |||
| | * | | Fixed typo in INSTALL file | leino | 2015-09-23 | |
| | | | | ||||
| * | | | A test file with an example of least vs greatest fixpoints. | leino | 2015-09-22 | |
| | | | | ||||
| | | * | fix for warnings related to deprecated z3 options (please update to the ↵ | Michael Lowell Roberts | 2015-09-22 | |
| | | | | | | | | | | | | | | | | latest revision of z3). | |||
| * | | | Removed unused code (old code from previous ghost-statement handling) | leino | 2015-09-21 | |
| | | | | ||||
| * | | | Moved premature uses of .IsGhost for Statement's | leino | 2015-09-21 | |
| | | | | ||||
| | | * | Auto-merged heads. | Michael Lowell Roberts | 2015-09-21 | |
| | | |\ | ||||
| | | * | | merged IronDafny updates. two unit tests related to traits do not pass if ↵ | Michael Lowell Roberts | 2015-09-21 | |
| | | | | | | | | | | | | | | | | | | | | ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly. | |||
| * | | | | Added back in various ghost tests | leino | 2015-09-20 | |
| | | | | | ||||
| * | | | | Changes that only affect line numbers in test case | leino | 2015-09-20 | |
| | | | | | ||||
| * | | | | Removed tabs from test file | leino | 2015-09-20 | |
| | | | | |