summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Fix issue 91 - Change how we compute the bounds of quantified variables so thatGravatar qunyanm2015-10-29
* 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 Ru...Gravatar wuestholz2015-10-26
|/
* Make /autoTriggers:1 be the default in Visual StudioGravatar leino2015-10-24
* In Visual Studio, be willing to display both resolution warnings and verifica...Gravatar leino2015-10-24
* In method and iterator specifications, inline top-level predicates (exceptGravatar leino2015-10-24
* Introduced new datatype update syntax: D.(f := E)Gravatar leino2015-10-23
* 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 its...Gravatar Bryan Parno2015-10-19
* 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
* Parsing and pretty printing of the new "existential guards" of the two kinds ...Gravatar leino2015-10-03
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l...Gravatar Rustan Leino2015-10-02
* Fixed latent crash of hovertext/outlining with include.Gravatar Rustan Leino2015-10-02
* 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
* | Removed the 'inSpecOnlyContext' map that had been part of the resolution ofGravatar leino2015-09-28
* | Renamed CheckIsNonGhost to CheckIsCompilable.Gravatar leino2015-09-28
* | Removed more traces of the previous resolution checks that happened during pa...Gravatar leino2015-09-28
* | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
| * 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 lates...Gravatar Michael Lowell Roberts2015-09-22
* | 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 ENA...Gravatar Michael Lowell Roberts2015-09-21
* | | 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 f...Gravatar leino2015-08-31
| * 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
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
* Small fix: there is no loop in (forall x :: Q(x) && Q(0))Gravatar Clément Pit--Claudel2015-08-27
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
* 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
* 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-22 19:12:35 +0000