summaryrefslogtreecommitdiff
path: root/Test/dafny4
Commit message (Expand)AuthorAge
* Fix issue 131. Instead of crashing, report an error when an undefined member ofGravatar qunyanm2016-02-09
* Fix issue 120. Need to wrap operations that are "lit lifted" and turned intoGravatar qunyanm2016-02-08
* Fix issue 124. Consider math operators that later turned into function callsGravatar qunyanm2016-02-08
* Last checkin checked in the wrong version of bug125.dfy. The failure part ofGravatar qunyanm2016-02-05
* Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.Gravatar qunyanm2016-02-05
* Fix issue 128. Change the translation of CanCallAssumption for let-such-thatGravatar qunyanm2016-02-04
* Fix issue 129. When looking for a constructor for which Dafny knows how toGravatar qunyanm2016-02-02
* Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"Gravatar qunyanm2016-02-02
* Fix issue 121. Don't split QuantifierExpr that are empty.Gravatar qunyanm2016-01-25
* Fix issue 122. Only generate autoTriggers for QuantifierExpr that are notGravatar qunyanm2016-01-25
* Fix issue 117. Generate an error when the "opened" of an import doesn't matchGravatar qunyanm2016-01-08
* Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typedGravatar qunyanm2016-01-07
* Added flying robots example to test suiteGravatar Rustan Leino2016-01-06
* Fix issue 116. Add the missing @ for the generated c# code.Gravatar qunyanm2016-01-05
* Fix issue 114. Do not export private terms for ComprehensionExpr in triggerGravatar qunyanm2015-12-08
* Fix issue 113. Make sure the tempVar name used in ToString() method doesn'tGravatar qunyanm2015-12-03
* Add the test for Bug88.Gravatar qunyanm2015-12-02
* Fix issue 110. Set useImport to true when trying to registerTopLevelDeclsGravatar qunyanm2015-12-02
* Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr whenGravatar qunyanm2015-11-30
* MergeGravatar leino2015-11-27
|\
* | Added Union-Find program to test suite (could be cleaned up, but verifies)Gravatar leino2015-11-27
| * Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
|/
* Fix issue 108. Use idGenerator to create a new collection name for eachGravatar qunyanm2015-11-18
* Fix issue 107. Instead of writing out StaticReceiverExpr as null valuedGravatar qunyanm2015-11-17
* 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
* Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr,Gravatar qunyanm2015-11-10
* Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, weGravatar qunyanm2015-11-06
* Fix issue 104. Use ResolvedExpression to compute subexpressions forGravatar qunyanm2015-11-04
* Fix issue89. Copy the out param to a local before use it in an anonymousGravatar qunyanm2015-11-04
* update the test.Gravatar qunyanm2015-10-30
* Fix issue 91 - Change how we compute the bounds of quantified variables so thatGravatar qunyanm2015-10-29
* Fixed bug introduced in changeset 7ebdf9cd4154Gravatar leino2015-10-22
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
* Improvements in proofsGravatar leino2015-09-28
* Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
* A test file with an example of least vs greatest fixpoints.Gravatar leino2015-09-22
* Proof that Ackermann can be curried and that it is monotonic in both arguments.Gravatar Rustan Leino2015-09-08
* Fix some tests by locally disabling auto triggersGravatar Clément Pit--Claudel2015-08-28
* Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
* Make use of new syntax in a test fileGravatar Rustan Leino2015-08-21
* Fixed bug in type unificationGravatar Rustan Leino2015-08-20
* Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
* Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...Gravatar Rustan Leino2015-07-28
* Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\
* | Enable autoTriggers in LitTriggers and SeqFromArrayGravatar Clément Pit--Claudel2015-07-17
* | Fix multiple tests that relied on z3 triggering on $BoxGravatar Clément Pit--Claudel2015-07-13
| * Added another lemma to a test fileGravatar Rustan Leino2015-07-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 21:38:29 +0000