| Commit message (Expand) | Author | Age |
* | Mark temps that are generated in the resolver as auto-generated identifiers so | qunyanm | 2016-01-20 |
* | Fix issue 117. Generate an error when the "opened" of an import doesn't match | qunyanm | 2016-01-08 |
* | Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typed | qunyanm | 2016-01-07 |
* | Removed Contract.Requires from method overrides (preconditions of overrides a... | Rustan Leino | 2016-01-06 |
* | Fix some VS IDE performance issues. | qunyanm | 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 |
* | Fix printing for ForallStmt. Previously we traverse the resolved forall | qunyanm | 2015-12-04 |
* | Fix issue 113. Make sure the tempVar name used in ToString() method doesn't | qunyanm | 2015-12-03 |
* | Fix issue 110. Set useImport to true when trying to registerTopLevelDecls | qunyanm | 2015-12-02 |
* | Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr when | qunyanm | 2015-11-30 |
* | Made an adjustment in the printing of resolved forall expressions (previous c... | leino | 2015-11-28 |
* | Merge | leino | 2015-11-27 |
|\ |
|
* | | Make cached results dependent on if a function is ghost or not | leino | 2015-11-27 |
* | | autocontracts: Don't add modifies clause to ghost methods | leino | 2015-11-27 |
| * | Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that | qunyanm | 2015-11-25 |
|/ |
|
* | Add code that uses Z3's optimization features (currently disabled by default). | wuestholz | 2015-11-19 |
* | Fix issue 108. Use idGenerator to create a new collection name for each | qunyanm | 2015-11-18 |
* | Fix issue 107. Instead of writing out StaticReceiverExpr as null valued | qunyanm | 2015-11-17 |
* | Fix issue 100. Add an axiom for functionHandle to trigger off of the origial | qunyanm | 2015-11-17 |
* | Updated version number to 1.9.6.21116. This version is now on rise4fun. | leino | 2015-11-16 |
* | 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 |
| * | Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, we | qunyanm | 2015-11-06 |
* | | Merge | leino | 2015-11-06 |
|\| |
|
* | | In the VS IDE, don't generate hover-text information for auto-generated ident... | leino | 2015-11-05 |
| * | Fix issue 104. Use ResolvedExpression to compute subexpressions for | qunyanm | 2015-11-04 |
| * | Fix issue89. Copy the out param to a local before use it in an anonymous | qunyanm | 2015-11-04 |
| * | Fix issue 91 - Change how we compute the bounds of quantified variables so that | qunyanm | 2015-10-29 |
|/ |
|
* | Merge | leino | 2015-10-26 |
|\ |
|
* | | Fixed location of blue dots to appear after semi-colons, not just before them. | leino | 2015-10-26 |
| * | DafnyExtension: Add menu item for automatic induction (mainly developed by Ru... | wuestholz | 2015-10-26 |
|/ |
|
* | Make /autoTriggers:1 be the default in Visual Studio | leino | 2015-10-24 |
* | In Visual Studio, be willing to display both resolution warnings and verifica... | leino | 2015-10-24 |
* | In method and iterator specifications, inline top-level predicates (except | leino | 2015-10-24 |
* | Introduced new datatype update syntax: D.(f := E) | leino | 2015-10-23 |
* | 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 its... | Bryan Parno | 2015-10-19 |
* | Version 1.9.6.21012 | Rustan Leino | 2015-10-12 |
* | DafnyExtension: Re-added assembly reference. | wuestholz | 2015-10-08 |
* | DafnyExtension: Fix concurrency issue. | wuestholz | 2015-10-08 |
* | Make the Dafny extension compile on VS 2015 without any old versions. | wuestholz | 2015-10-08 |
* | Implemented resolution, verification, and (poorly performing) compilation of ... | leino | 2015-10-05 |
* | Parsing and pretty printing of the new "existential guards" of the two kinds ... | leino | 2015-10-03 |
* | Made /rewriteFocalPredicates:1 the default | Rustan Leino | 2015-10-02 |
* | Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l... | Rustan Leino | 2015-10-02 |
* | Fixed latent crash of hovertext/outlining with include. | Rustan Leino | 2015-10-02 |