summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
Commit message (Expand)AuthorAge
* Fix issue 143. The list that stores the function fuel constants was declared asGravatar qunyanm2016-03-31
* Fix issue 75. Adjust the fuel for existentials to use more fuel in an assumeGravatar qunyanm2016-03-31
* Fix issue 93. Add per-function fuel setting that can be adjusted locally basedGravatar qunyanm2016-03-18
* Revised the $Is and $IsAlloc axioms for arrow terms. It is now possible toGravatar Rustan Leino2016-03-01
* Added a return-value contractGravatar Rustan Leino2016-02-29
* MergeGravatar Rustan Leino2016-02-26
|\
* | Changes to CanCall assumptions:Gravatar Rustan Leino2016-02-26
| * Fix issue 136. Less aggressive Lit wrap for assert/assume.Gravatar qunyanm2016-02-26
|/
* Fix issue 132. The formal argument can't be assume to be allocated when aGravatar qunyanm2016-02-12
* Fix issue 133. The return type for some compare operators was wrongly typedGravatar qunyanm2016-02-11
* Fix issue 120. Need to wrap operations that are "lit lifted" and turned intoGravatar qunyanm2016-02-08
* Fix issue 128. Change the translation of CanCallAssumption for let-such-thatGravatar qunyanm2016-02-04
* MergeGravatar leino2015-11-27
|\
* | Make cached results dependent on if a function is ghost or notGravatar leino2015-11-27
| * Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
|/
* Add code that uses Z3's optimization features (currently disabled by default).Gravatar wuestholz2015-11-19
* Fix issue 100. Add an axiom for functionHandle to trigger off of the origialGravatar qunyanm2015-11-17
* Fix issue 94. Allow tuple-based assignment in statement contexts.Gravatar qunyanm2015-11-14
* Fixed location of blue dots to appear after semi-colons, not just before them.Gravatar leino2015-10-26
* In method and iterator specifications, inline top-level predicates (exceptGravatar leino2015-10-24
* Fixed bug introduced in changeset 7ebdf9cd4154Gravatar leino2015-10-22
* Implemented resolution, verification, and (poorly performing) compilation of ...Gravatar leino2015-10-05
* Parsing and pretty printing of the new "existential guards" of the two kinds ...Gravatar leino2015-10-03
* merged IronDafny updates. two unit tests related to traits do not pass if ENA...Gravatar Michael Lowell Roberts2015-09-21
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...Gravatar Clément Pit--Claudel2015-08-23
* Adjust WF checks to use unsplit quantifiers.Gravatar Clément Pit--Claudel2015-08-21
* Add some diversity to Dafny's alimentationGravatar Clément Pit--Claudel2015-08-21
* Merge.Gravatar Clément Pit--Claudel2015-08-20
|\
| * MergeGravatar Rustan Leino2015-08-20
| |\
* | | Mark a few reporting functions as staticGravatar Clément Pit--Claudel2015-08-20
* | | Add a check for SplitQuantifiers that had been incorrectly left out from the ...Gravatar Clément Pit--Claudel2015-08-19
| |/ |/|
| * Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
* | Merge.Gravatar Clément Pit--Claudel2015-08-19
|\|
* | Check Reads and Decreases clauses for expressions that could prevent inliningGravatar Clément Pit--Claudel2015-08-18
* | Refactor calls to 'new CallCmd' and clear a few FIXMEsGravatar Clément Pit--Claudel2015-08-18
* | Review preceding commit with RustanGravatar Clément Pit--Claudel2015-08-17
* | Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
* | Implement self-loop detectionGravatar Clément Pit--Claudel2015-08-14
* | Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
* | Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| * Removed the unused type ThisSurrogateGravatar leino2015-08-11
| * Moved discovery of induction variables into a Rewriter.Gravatar leino2015-08-11
|/
* MergeGravatar Clément Pit--Claudel2015-07-28
|\
* | Clarify the inlining warning.Gravatar Clément Pit--Claudel2015-07-27
* | Clean up error reporting.Gravatar Clément Pit--Claudel2015-07-27
| * Translate triggers with the same ExpressionTranslator as the bodyGravatar Rustan Leino2015-07-24
|/
* Fix: Read clauses should be checked before lit liftingGravatar Clément Pit--Claudel2015-07-23
* Improved rank axioms for containersGravatar Rustan Leino2015-07-21
* Code reviewed some of the triggers added by changeset 1dacb6d3cc3cGravatar Rustan Leino2015-07-21
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 05:58:45 +0000