Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | 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. | |||
* | 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. | |||
* | 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 location of blue dots to appear after semi-colons, not just before them. | leino | 2015-10-26 | |
| | ||||
* | 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) | |||
* | Refactored resolution of datatype updates, preparing for a change of syntax | leino | 2015-10-23 | |
| | ||||
* | 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. | |||
* | 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]. | |||
* | Removed some unused code. | Rustan Leino | 2015-09-30 | |
| | ||||
* | Merge | leino | 2015-09-28 | |
|\ | ||||
* | | Removed specContextOnly parameter from ResolveStatement. | leino | 2015-09-28 | |
| | | | | | | | | Moved all bounds discovery to resolution pass 1. | |||
* | | Removed the 'inSpecOnlyContext' map that had been part of the resolution of | leino | 2015-09-28 | |
| | | | | | | | | | | 'break' statements out of ghost structures. This is now done in pass 2 by looking at the .IsGhost field of the target statement. | |||
* | | Renamed CheckIsNonGhost to CheckIsCompilable. | leino | 2015-09-28 | |
| | | ||||
* | | 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. | |||
* | | 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. | |||
| * | fixed bugs related to identifying newtypes as types of integers and reals. | Michael Lowell Roberts | 2015-09-23 | |
| | | ||||
| * | fix for warnings related to deprecated z3 options (please update to the ↵ | Michael Lowell Roberts | 2015-09-22 | |
| | | | | | | | | latest revision of z3). | |||
* | | Removed unused code (old code from previous ghost-statement handling) | leino | 2015-09-21 | |
| | | ||||
* | | Moved premature uses of .IsGhost for Statement's | leino | 2015-09-21 | |
| | | ||||
| * | merged IronDafny updates. two unit tests related to traits do not pass if ↵ | Michael Lowell Roberts | 2015-09-21 | |
| | | | | | | | | ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly. | |||
* | | Preliminary refactoring of ghost-statement computations to after type checking | leino | 2015-09-20 | |
| | | ||||
| * | Only print extraneous comments if asked. | Michael Lowell Roberts | 2015-09-17 | |
| | | ||||
* | | Merge | leino | 2015-09-11 | |
|\| | ||||
* | | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing ↵ | leino | 2015-08-31 | |
| | | | | | | | | for way to build up and later solve type constraints. | |||
| * | Implement {:nowarn}, clarify some messages, and add a few tests | Clément Pit--Claudel | 2015-08-28 | |
|/ | ||||
* | Tiny cleanup in TriggersCollector | Clément Pit--Claudel | 2015-08-27 | |
| | ||||
* | Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience) | Clément Pit--Claudel | 2015-08-27 | |
| | | | | | | Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it looks for one in Binaries/z3.exe (mostly for backwards-compatibility with already set-up source installations). | |||
* | Further relax the loop detection conditions | Clément Pit--Claudel | 2015-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)) | Clément Pit--Claudel | 2015-08-27 | |
| | | | | Again, spotted by Chris :) | |||
* | Improve the redundancy detection algorithm used while constructing sets of terms | Clément Pit--Claudel | 2015-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. | |||
* | s/loops with/may loop with/ | Clément Pit--Claudel | 2015-08-23 | |
| | ||||
* | Make quantifier splitting a two step process | Clément Pit--Claudel | 2015-08-23 | |
| | | | | This fixes a bug that affected Monad.dfy | |||
* | Shallow-copy quantifier attributes when splitting | Clément Pit--Claudel | 2015-08-23 | |
| | ||||
* | Add a sanity check in QuantifiersCollection | Clément Pit--Claudel | 2015-08-23 | |
| | ||||
* | Improve error reporting for split quantifiers | Clément Pit--Claudel | 2015-08-23 | |
| | ||||
* | Allow MultiSelectExpr as quantifier heads | Clément Pit--Claudel | 2015-08-23 | |
| | ||||
* | Trivial code cleanup | Clément Pit--Claudel | 2015-08-23 | |
| |