summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* 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.
* A test file with an example of least vs greatest fixpoints.Gravatar leino2015-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
|
* Added back in various ghost testsGravatar leino2015-09-20
|
* Changes that only affect line numbers in test caseGravatar leino2015-09-20
|
* Removed tabs from test fileGravatar leino2015-09-20
|
* Adjusted (corrected, I think) test outputGravatar leino2015-09-20
|
* Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
|
* MergeGravatar leino2015-09-11
|\
| * Fix #90Gravatar Clément Pit--Claudel2015-09-09
| | | | | | | | The mono wrapper for Dafny didn't forward command line arguments.
| * Proof that Ackermann can be curried and that it is monotonic in both arguments.Gravatar Rustan Leino2015-09-08
| |
| * MergeGravatar Clément Pit--Claudel2015-09-02
| |\
* | | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing ↵Gravatar leino2015-08-31
| | | | | | | | | | | | for way to build up and later solve type constraints.
| | * fix for comparison error in prelude when using /optimize.Gravatar Michael Lowell Roberts2015-08-31
| |/ |/|
| * Fix some tests by locally disabling auto triggersGravatar Clément Pit--Claudel2015-08-28
| |
| * Align the server's default kill time with the one of the VS extensionGravatar Clément Pit--Claudel2015-08-28
| |
| * Add a small test from a discussion with BryanGravatar Clément Pit--Claudel2015-08-28
| |
| * Implement workarounds for some tests that fail with /autoTriggers.Gravatar Clément Pit--Claudel2015-08-28
| | | | | | | | | | | | The issues here are mostly with induction (wrt. to trigger selection and quantifier splitting) and with expressions like P(i, j-1) where no good choices are available.
| * Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
| | | | | | | | | | We already have separate tests for those, and we want the output to be the same with and without /autoTriggers.
| * Clarify a commentGravatar Clément Pit--Claudel2015-08-28
| |
| * Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
| |
| * Put contents od release packages into a dafny/ directoryGravatar Clément Pit--Claudel2015-08-28
| |
* | MergeGravatar Rustan Leino2015-08-28
|\|
* | Added tests for Boogie's new /verifySnapshots:3, which will be used by the ↵Gravatar Rustan Leino2015-08-28
| | | | | | | | Dafny emacs mode
* | Fixed spelling mistake in test fileGravatar Rustan Leino2015-08-28
| |
| * Add a small test from the IronClad notebookGravatar Clément Pit--Claudel2015-08-27
| |
| * Tiny cleanup in TriggersCollectorGravatar Clément Pit--Claudel2015-08-27
| |
| * Add a tip to the packaging scriptGravatar Clément Pit--Claudel2015-08-27
| |
| * Update INSTALL to reflect the latest packaging changesGravatar Clément Pit--Claudel2015-08-27
| |
| * package.py: Keep z3's exec bits, and set the exec bit on the dafny/ scriptGravatar Clément Pit--Claudel2015-08-27
| |
| * More fixes to the packaging scriptGravatar Clément Pit--Claudel2015-08-27
| |
| * Make the packaging script Windows-compatibleGravatar 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 :)
| * MergeGravatar Clément Pit--Claudel2015-08-26
| |\ | |/ |/|
| * 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.
* | MergeGravatar Clément Pit--Claudel2015-08-24
|\ \ | |/ |/|
| * Add the Package folder to .hgignoreGravatar Clément Pit--Claudel2015-08-24
| |
* | Add change missing from bd47e3cdb79cGravatar Clément Pit--Claudel2015-08-23
| |
* | s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
| |
* | MergeGravatar Clément Pit--Claudel2015-08-23
|\|
| * Write a new packaging script for DafnyGravatar Clément Pit--Claudel2015-08-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is intended to superseed the PrepareDafnyZip.bat script. I tried doing this as an msbuild config, then as a makefile, but the first one was too cumbersome and the second one required too many dependencies to work properly (and parsing JSON from a makefile is not fun). The new script calls the Github API to retrieve the description of the latest z3 release, downloads the zip corresponding to each supported platfom, and packages one copy of Dafny for each copy of z3 that the latest release contains. The next step will be to make Dafny load its binary from the z3 folder.
| * Replace the Emacs mode files by a pointer to the boogie-friends repo.Gravatar Clément Pit--Claudel2015-08-23
| | | | | | | | Does mercurial support submodules? That could be a good option too.
* | Added /autoTriggers to two tests where it only makes a cosmetic differenceGravatar Clément Pit--Claudel2015-08-23
| |
* | Replace b || !b by true in Snapshots5.v1.dfyGravatar Clément Pit--Claudel2015-08-23
| | | | | | | | | | | | We can't prove `exists b: bool :: b || !b` when splitting is enabled, at least for now, and there's already a separate test for that particular issue in wishlist/
* | 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
| |
* | Add a sanity check in QuantifiersCollectionGravatar Clément Pit--Claudel2015-08-23
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 13:09:49 +0000