| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Merge |  leino | 2016-04-01 |
| |\ | |||
| * | | New test file, for recursive and iterative versions of McCarthy's 91 function | leino | 2016-04-01 |
| | | | |||
| * | | New test case, proving monad laws for lists | leino | 2016-04-01 |
| | | | |||
| | * | Fix issue 148. The results for sign comparison for BigRational.CompareTo was | qunyanm | 2016-04-01 |
| |/ | | | | wrong. | ||
| * | Fix issue 75. Adjust the fuel for existentials to use more fuel in an assume | qunyanm | 2016-03-31 |
| | | | | | context and less in an assert. | ||
| * | Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires | qunyanm | 2016-03-28 |
| | | | | | | it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. | ||
| * | Fix issue 93. Add per-function fuel setting that can be adjusted locally based | qunyanm | 2016-03-18 |
| | | | | | on context. | ||
| * | Added test case to go with the recent fix of Issue #49 (changeset f354709009a5). | Rustan Leino | 2016-03-01 |
| | | |||
| * | Fix issue 139. Allow bound variables in nested case patterns to shadow variables | qunyanm | 2016-02-26 |
| | | | | | declared outside the enclosing match. | ||
| * | Fix issue 138. Allow parenthese with the nullary constructor in | qunyanm | 2016-02-26 |
| | | | | | "case" of a match statement and match expression. | ||
| * | Fix test failure. Print the resulting boogie code to a file instead | qunyanm | 2016-02-26 |
| | | | | | of console. | ||
| * | Fix issue 140. Move the initializion of _this before the TAIL_CALL_START label. | qunyanm | 2016-02-26 |
| | | |||
| * | Fix issue 136. Less aggressive Lit wrap for assert/assume. | qunyanm | 2016-02-26 |
| | | |||
| * | Update the test's .expect file since the fix is merged into boogie. | qunyanm | 2016-02-12 |
| | | |||
| * | Fix issue 132. The formal argument can't be assume to be allocated when a | qunyanm | 2016-02-12 |
| | | | | | function is invoked inside an "Old" expression. | ||
| * | Fix issue 134. Wrong variable was used in the loop. | qunyanm | 2016-02-11 |
| | | |||
| * | Fix issue 133. The return type for some compare operators was wrongly typed | qunyanm | 2016-02-11 |
| | | | | | as int instead of bool. | ||
| * | Fix issue 131. Instead of crashing, report an error when an undefined member of | qunyanm | 2016-02-09 |
| | | | | | a class is referenced. | ||
| * | Fix issue 120. Need to wrap operations that are "lit lifted" and turned into | qunyanm | 2016-02-08 |
| | | | | | boogie function calls with "Lit" function. | ||
| * | Fix issue 124. Consider math operators that later turned into function calls | qunyanm | 2016-02-08 |
| | | | | | as candidates for triggers. | ||
| * | Last checkin checked in the wrong version of bug125.dfy. The failure part of | qunyanm | 2016-02-05 |
| | | | | | | the test was moved into test\dafny0\modules0.dfy so that bug125.dfy can be verified that it was resolved to the correct types. | ||
| * | Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports. | qunyanm | 2016-02-05 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For the following situation module LibA { // ...things declared here... } module LibB { // ...things declared here... } module R { import opened LibA // ...things declared here... } module S refines R { import opened LibB // ...declared here... } 1. If module R declares a TopLevelDecl “G”, then we should report an error if S attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already. 2. If LibA declares a TopLevelDecl “G” but R does not directly declare any TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G” in S. This behavior is missing in Dafny. 3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S directly declares any TopLevelDecl “G”, then no error should be issued, and any use of “G” in S should resolve to the “G” in LibA. This behavior is missing in Dafny. | ||
| * | Fix issue 128. Change the translation of CanCallAssumption for let-such-that | qunyanm | 2016-02-04 |
| | | | | | | | | | | | | | | expression from // CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] = // (forall b0,b1 :: typeAntecedent ==> // CanCall[[ RHS(b,g) ]] && // (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) && // $let$canCall(b,g)) to // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] = // $let$canCall(g) && // CanCall[[ Body($let$b0(g), $let$b1(g), h) ]] | ||
| * | Fix issue 129. When looking for a constructor for which Dafny knows how to | qunyanm | 2016-02-02 |
| | | | | | | | | | instantiate all it arguments, don't stop as soon as one instantiable constructor is found. Instead, figure out all instantiable constructors and then pick the best among these. A simple and reasonable "best" is an instantiable constructor that requires a minimal number of already constructed type arguments, and to break ties among these, pick the first one listed. | ||
| * | Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B" | qunyanm | 2016-02-02 |
| | | |||
| * | Fix issue 121. Don't split QuantifierExpr that are empty. | qunyanm | 2016-01-25 |
| | | |||
| * | 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 |
| | | |||
| * | 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. | ||
| * | 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 |
| | | |||
| * | 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. | ||
| * | 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. | ||
| * | Fixed bug introduced in changeset 7ebdf9cd4154 | leino | 2015-10-22 |
| | | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |