summaryrefslogtreecommitdiff
path: root/Test
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.
* Fix issue 108. Use idGenerator to create a new collection name for eachGravatar qunyanm2015-11-18
| | | | occurrence of Set/MapComprehension when translating it to c#.
* Fix issue 107. Instead of writing out StaticReceiverExpr as null valuedGravatar qunyanm2015-11-17
| | | | LiteralExpr, write out its type instead.
* Fix issue 100. Add an axiom for functionHandle to trigger off of the origialGravatar qunyanm2015-11-17
| | | | function and connect with Apply1 of the function.
* Fix issue 94. Allow tuple-based assignment in statement contexts.Gravatar qunyanm2015-11-14
|
* MergeGravatar leino2015-11-11
|\
* | Fixed compilation of equality between reference typesGravatar leino2015-11-11
| |
| * Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr,Gravatar qunyanm2015-11-10
| | | | | | | | | | swap them when the expr is first created in parser or for calcstmt. This avoids problems of operands being swapped again when the expr is copied.
| * Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, weGravatar qunyanm2015-11-06
| | | | | | | | | | need exclude the private terms (the ones that includes the quantifier expr's bv) from it exported terms.
* | MergeGravatar leino2015-11-06
|\|
* | Updated syntax of test case to remove unnecessary semicolons and parenthesesGravatar leino2015-11-05
| |
| * Fix issue 104. Use ResolvedExpression to compute subexpressions forGravatar qunyanm2015-11-04
| | | | | | | | DatatypeUpdateExpr if ResovedExpression is not null.
| * Fix issue89. Copy the out param to a local before use it in an anonymousGravatar qunyanm2015-11-04
| | | | | | | | | | | | method that is generated by LetExpr. Change the compiler so that each stmt writes to its own buffer before add it to the program's buffer so that we can insert the above mentioned copy instruction before the stmt.
| * update the test.Gravatar qunyanm2015-10-30
| |
| * 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.
| * Check version info before delete white space so that it will work with pythonGravatar qunyanm2015-10-28
|/ | | | version that is less than 3.
* 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)
* 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.
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 00:52:48 +0000