summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
...
* Renamed ExistentialGuards... to BindingGuards...Gravatar Rustan Leino2015-10-07
|
* Use /env:0 to avoid full pathnames in test outputGravatar Rustan Leino2015-10-06
|
* 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].
* MergeGravatar leino2015-09-29
|\
| * Fix two test cases that failed if the path to "DafnySever.exe" contained spaces.Gravatar wuestholz2015-09-30
| |
* | Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
| | | | | | | | Moved all bounds discovery to resolution pass 1.
* | 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.
* | Additional testsGravatar leino2015-09-28
| |
* | Whitespace changes in test fileGravatar leino2015-09-28
| |
* | Improvements in proofsGravatar leino2015-09-28
| |
* | 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
| |
* | 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
|/
* 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
|\
* | Fix some tests by locally disabling auto triggersGravatar 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
| |
| * 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
| |
* | 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.
* Add change missing from bd47e3cdb79cGravatar Clément Pit--Claudel2015-08-23
|
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
|
* 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
* Improve error reporting for split quantifiersGravatar Clément Pit--Claudel2015-08-23
|
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
|
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect ↵Gravatar Clément Pit--Claudel2015-08-23
| | | | locations.
* Add one more wish: it would be nice to be able to prove exists b: bool :: bGravatar Clément Pit--Claudel2015-08-22
| | | | | This is an issue because splitting `exists b: bool :: b || !b` produces two quantifiers that we don't know how to prove.
* Grant "wishlist/useless-casts-in-decreases-clauses.dfy"Gravatar Clément Pit--Claudel2015-08-22
|
* Add more wishes to the wishlistGravatar Clément Pit--Claudel2015-08-22
|
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
|
* Add a 'tutorial' folder to the distribution, with an initial example.Gravatar Clément Pit--Claudel2015-08-22
| | | | | | | | | | It would be nice to gather neat Dafny examples there; each new feature could have its own small file that demoes it, and we could also have examples that showcase stuff that we think is impressive. I'm adding this as a test folder, because it's important to check that these cool examples don't break, but the focus probably shouldn't be on exhaustively testing the features being demoed.
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
* | Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
| | | | | | | | | | | | Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and old(f(x)). This has a number of implications; see the new tests files for more information.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:03:23 +0000