| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix issue 122. Only generate autoTriggers for QuantifierExpr that are not |  qunyanm | 2016-01-25 |
| | | | | | empty. | ||
| * | Fix issue 117. Generate an error when the "opened" of an import doesn't match | qunyanm | 2016-01-08 |
| | | | | | between a module and its refinement base. | ||
| * | Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typed | qunyanm | 2016-01-07 |
| | | | | | bound as undetermined so that iteration will continue. | ||
| * | Added flying robots example to test suite | Rustan Leino | 2016-01-06 |
| | | |||
| * | Fix issue 116. Add the missing @ for the generated c# code. | qunyanm | 2016-01-05 |
| | | |||
| * | Add /autoTriggers:1 to remove the undeterminateness of proof search. | qunyanm | 2015-12-15 |
| | | |||
| * | Fix issue 114. Do not export private terms for ComprehensionExpr in trigger | qunyanm | 2015-12-08 |
| | | | | | collectors. | ||
| * | Fix issue 113. Make sure the tempVar name used in ToString() method doesn't | qunyanm | 2015-12-03 |
| | | | | | collide with the names of its formals. | ||
| * | Add the test for Bug88. | qunyanm | 2015-12-02 |
| | | |||
| * | Fix issue 110. Set useImport to true when trying to registerTopLevelDecls | qunyanm | 2015-12-02 |
| | | | | | in MakeAbstractSignature. | ||
| * | Update the test .expect files since the line number info is fixed with boogie | qunyanm | 2015-12-02 |
| | | | | | merge #24 | ||
| * | Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr when | qunyanm | 2015-11-30 |
| | | | | | trying to substitute the nested CasePattern with the BoundVar. | ||
| * | Merge | leino | 2015-11-27 |
| |\ | |||
| * | | Added Union-Find program to test suite (could be cleaned up, but verifies) | leino | 2015-11-27 |
| | | | |||
| | * | Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that | qunyanm | 2015-11-25 |
| |/ | | | | the auto-triggers can be computed for ForallStmt. | ||
| * | Fix issue 108. Use idGenerator to create a new collection name for each | qunyanm | 2015-11-18 |
| | | | | | occurrence of Set/MapComprehension when translating it to c#. | ||
| * | Fix issue 107. Instead of writing out StaticReceiverExpr as null valued | qunyanm | 2015-11-17 |
| | | | | | LiteralExpr, write out its type instead. | ||
| * | Fix issue 100. Add an axiom for functionHandle to trigger off of the origial | qunyanm | 2015-11-17 |
| | | | | | function and connect with Apply1 of the function. | ||
| * | Fix issue 94. Allow tuple-based assignment in statement contexts. | qunyanm | 2015-11-14 |
| | | |||
| * | Merge | leino | 2015-11-11 |
| |\ | |||
| * | | Fixed compilation of equality between reference types | leino | 2015-11-11 |
| | | | |||
| | * | Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr, | qunyanm | 2015-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, we | qunyanm | 2015-11-06 |
| | | | | | | | | | | | need exclude the private terms (the ones that includes the quantifier expr's bv) from it exported terms. | ||
| * | | Merge | leino | 2015-11-06 |
| |\| | |||
| * | | Updated syntax of test case to remove unnecessary semicolons and parentheses | leino | 2015-11-05 |
| | | | |||
| | * | Fix issue 104. Use ResolvedExpression to compute subexpressions for | qunyanm | 2015-11-04 |
| | | | | | | | | | DatatypeUpdateExpr if ResovedExpression is not null. | ||
| | * | Fix issue89. Copy the out param to a local before use it in an anonymous | qunyanm | 2015-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. | qunyanm | 2015-10-30 |
| | | | |||
| | * | Fix issue 91 - Change how we compute the bounds of quantified variables so that | qunyanm | 2015-10-29 |
| | | | | | | | | | it does not depend on the order they appeared. | ||
| | * | Check version info before delete white space so that it will work with python | qunyanm | 2015-10-28 |
| |/ | | | | version that is less than 3. | ||
| * | In method and iterator specifications, inline top-level predicates (except | leino | 2015-10-24 |
| | | | | | protected predicated in cross-module calls) like in other places. | ||
| * | Introduced new datatype update syntax: D.(f := E) | leino | 2015-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 7ebdf9cd4154 | leino | 2015-10-22 |
| | | |||
| * | Improve Dafny's ability to find fueled functions by checking the function ↵ |  Bryan Parno | 2015-10-19 |
| | | | | | | | itself, as well as the signature and body of other functions. | ||
| * | Renamed ExistentialGuards... to BindingGuards... | Rustan Leino | 2015-10-07 |
| | | |||
| * | Use /env:0 to avoid full pathnames in test output | Rustan Leino | 2015-10-06 |
| | | |||
| * | Implemented resolution, verification, and (poorly performing) compilation of ↵ | leino | 2015-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 ↵ | leino | 2015-10-03 |
| | | | | | of "if" statements. | ||
| * | Made /rewriteFocalPredicates:1 the default | Rustan Leino | 2015-10-02 |
| | | |||
| * | Hover text includes #[_k-1] suffix for terms rewritten in prefix ↵ | Rustan Leino | 2015-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]. | ||
| * | Merge | leino | 2015-09-29 |
| |\ | |||
| | * | Fix two test cases that failed if the path to "DafnySever.exe" contained spaces. | wuestholz | 2015-09-30 |
| | | | |||
| * | | Removed specContextOnly parameter from ResolveStatement. | leino | 2015-09-28 |
| | | | | | | | | | Moved all bounds discovery to resolution pass 1. | ||
| * | | Removed more traces of the previous resolution checks that happened during ↵ | leino | 2015-09-28 |
| | | | | | | | | | | | | | pass 0. Fixed resolution of specification components of alternative loops. | ||
| * | | Additional tests | leino | 2015-09-28 |
| | | | |||
| * | | Whitespace changes in test file | leino | 2015-09-28 |
| | | | |||
| * | | Improvements in proofs | leino | 2015-09-28 |
| | | | |||
| * | | Changed computation of ghosts until pass 2 of resolution. | leino | 2015-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. | leino | 2015-09-22 |
| | | | |||
| * | | Added back in various ghost tests | leino | 2015-09-20 |
| | | | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |