summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Fix issue 91 - Change how we compute the bounds of quantified variables so thatGravatar qunyanm2015-10-29
| | | | it does not depend on the order they appeared.
* MergeGravatar leino2015-10-26
|\
* | Fixed location of blue dots to appear after semi-colons, not just before them.Gravatar leino2015-10-26
| |
| * DafnyExtension: Add menu item for automatic induction (mainly developed by ↵Gravatar wuestholz2015-10-26
|/ | | | Rustan).
* Make /autoTriggers:1 be the default in Visual StudioGravatar leino2015-10-24
|
* In Visual Studio, be willing to display both resolution warnings and ↵Gravatar leino2015-10-24
| | | | | | verification errors (previously, verification errors were masked by resolution warnings)
* In method and iterator specifications, inline top-level predicates (exceptGravatar leino2015-10-24
| | | | protected predicated in cross-module calls) like in other places.
* Introduced new datatype update syntax: D.(f := E)Gravatar leino2015-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 syntaxGravatar leino2015-10-23
|
* Fixed bug introduced in changeset 7ebdf9cd4154Gravatar leino2015-10-22
|
* Improve Dafny's ability to find fueled functions by checking the function ↵Gravatar Bryan Parno2015-10-19
| | | | | | itself, as well as the signature and body of other functions.
* Version 1.9.6.21012Gravatar Rustan Leino2015-10-12
|
* DafnyExtension: Re-added assembly reference.Gravatar wuestholz2015-10-08
|
* DafnyExtension: Fix concurrency issue.Gravatar wuestholz2015-10-08
|
* Make the Dafny extension compile on VS 2015 without any old versions.Gravatar wuestholz2015-10-08
|
* Implemented resolution, verification, and (poorly performing) compilation of ↵Gravatar leino2015-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 ↵Gravatar leino2015-10-03
| | | | of "if" statements.
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
|
* Hover text includes #[_k-1] suffix for terms rewritten in prefix ↵Gravatar Rustan Leino2015-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.Gravatar Rustan Leino2015-10-02
| | | | (This also undoes two previous attempted fixes, which had accidentally disabled some outlining and hovertexts.)
* Removed some unused code.Gravatar Rustan Leino2015-09-30
|
* MergeGravatar leino2015-09-29
|\
| * Fix the build.Gravatar wuestholz2015-09-29
| |
* | MergeGravatar leino2015-09-28
|\|
* | Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
| | | | | | | | Moved all bounds discovery to resolution pass 1.
* | Removed the 'inSpecOnlyContext' map that had been part of the resolution ofGravatar leino2015-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.Gravatar leino2015-09-28
| |
* | Removed more traces of the previous resolution checks that happened during ↵Gravatar leino2015-09-28
| | | | | | | | | | | | pass 0. Fixed resolution of specification components of alternative loops.
* | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-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.
| * fixed bugs related to identifying newtypes as types of integers and reals.Gravatar Michael Lowell Roberts2015-09-23
| |
| * fix for warnings related to deprecated z3 options (please update to the ↵Gravatar Michael Lowell Roberts2015-09-22
| | | | | | | | latest revision of z3).
* | Removed unused code (old code from previous ghost-statement handling)Gravatar leino2015-09-21
| |
* | Moved premature uses of .IsGhost for Statement'sGravatar leino2015-09-21
| |
| * Auto-merged heads.Gravatar Michael Lowell Roberts2015-09-21
| |\
| * | merged IronDafny updates. two unit tests related to traits do not pass if ↵Gravatar Michael Lowell Roberts2015-09-21
| | | | | | | | | | | | ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
* | | Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
| | |
| | * Fix a check that occasionally led to an out of bounds exception in the extensionGravatar Bryan Parno2015-09-17
| | |
| * | Only print extraneous comments if asked.Gravatar Michael Lowell Roberts2015-09-17
| |/
* | MergeGravatar leino2015-09-11
|\|
* | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing ↵Gravatar leino2015-08-31
| | | | | | | | for way to build up and later solve type constraints.
| * Align the server's default kill time with the one of the VS extensionGravatar Clément Pit--Claudel2015-08-28
| |
| * Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
|/
* Tiny cleanup in TriggersCollectorGravatar Clément Pit--Claudel2015-08-27
|
* Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)Gravatar Clément Pit--Claudel2015-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).
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
| | | | | Mismatches are now allowed up to expressions not involving any of the bound variables of the quantifier under inspection.
* Small fix: there is no loop in (forall x :: Q(x) && Q(0))Gravatar Clément Pit--Claudel2015-08-27
| | | | Again, spotted by Chris :)
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
| | | | | | | | Based on an issue noted by Chris with redundancy removal resuls being dependent on the order of the terms. Interestingly, one of our tests already had an instance of that problem. Also fix the issue with nested quantifiers getting redundant triggers.
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
|
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
| | | | This fixes a bug that affected Monad.dfy
* Shallow-copy quantifier attributes when splittingGravatar Clément Pit--Claudel2015-08-23
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 00:32:30 +0000