summaryrefslogtreecommitdiff
path: root/Test/dafny0
Commit message (Collapse)AuthorAge
* Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
| | | | the auto-triggers can be computed for ForallStmt.
* Fixed compilation of equality between reference typesGravatar leino2015-11-11
|
* 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.
* 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)
* 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.
* 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].
* 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
|
* 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.
* 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
|
* Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
|
* MergeGravatar Clément Pit--Claudel2015-09-02
|\
* | 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.
| * Added tests for Boogie's new /verifySnapshots:3, which will be used by the ↵Gravatar Rustan Leino2015-08-28
|/ | | | Dafny emacs mode
* Add change missing from bd47e3cdb79cGravatar 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/
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect ↵Gravatar Clément Pit--Claudel2015-08-23
| | | | locations.
* MergeGravatar Rustan Leino2015-08-20
|\
* | Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
| |
| * Merge.Gravatar Clément Pit--Claudel2015-08-20
| |\ | |/ |/|
* | MergeGravatar Rustan Leino2015-08-20
|\ \
| | * Add a test to check that there are as many errors as failed preconditionsGravatar Clément Pit--Claudel2015-08-19
| |/
* | Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
| |
| * Merge.Gravatar Clément Pit--Claudel2015-08-19
| |\ | |/ |/| | | | | Changes that were needed included preventing the InductionRewriter from iterating on a SplitQuantifier and using the new error reporting engine.
| * Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
| |
| * Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
| | | | | | | | This new version will include a cleaner pipeline, and trigger splitting.
* | Change the induction heuristic for lemmas to also look in precondition for ↵Gravatar leino2015-08-12
|/ | | | | | clues about which parameters to include. As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.
* MergeGravatar Rustan Leino2015-07-31
|\
| * MergeGravatar leino2015-07-31
| |\
* | | Bug fix: check that assign-such-that constraint is of type booleanGravatar Rustan Leino2015-07-31
| |/ |/|
| * Allow forall statements in refinementsGravatar leino2015-07-31
| |
* | Add quotes in snapshot tests.Gravatar Clément Pit--Claudel2015-07-30
| | | | | | | | Thanks Valentin for elucidating this issue!
* | Fixed crash in resolution where, after reporting an error, the cases #type ↵Gravatar Rustan Leino2015-07-29
| | | | | | | | and #module were not handled
* | Clarify the inlining warning.Gravatar Clément Pit--Claudel2015-07-27
|/
* Fix: Read clauses should be checked before lit liftingGravatar Clément Pit--Claudel2015-07-23
| | | | | | | | | The function IgnoreFuel in UnfoldingPerformance.dfy used to be lit-wrapped. It shouldn't be, because its reads clause is non-empty. This is not a soundness bug, but fixing it improves performance in cases where a function call would be incorrectly unrolled. Test case written by Rustan.
* Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
| | | | | | | | | Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests.
* Improved rank axioms for containersGravatar Rustan Leino2015-07-21
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 00:46:59 +0000