summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers
Commit message (Expand)AuthorAge
* Fix issue 124. Consider math operators that later turned into function callsGravatar qunyanm2016-02-08
* 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
* Removed Contract.Requires from method overrides (preconditions of overrides a...Gravatar Rustan Leino2016-01-06
* Fix issue 114. Do not export private terms for ComprehensionExpr in triggerGravatar qunyanm2015-12-08
* Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
* Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, weGravatar qunyanm2015-11-06
* Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
* Tiny cleanup in TriggersCollectorGravatar Clément Pit--Claudel2015-08-27
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
* Small fix: there is no loop in (forall x :: Q(x) && Q(0))Gravatar Clément Pit--Claudel2015-08-27
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
* Shallow-copy quantifier attributes when splittingGravatar Clément Pit--Claudel2015-08-23
* Add a sanity check in QuantifiersCollectionGravatar Clément Pit--Claudel2015-08-23
* Improve error reporting for split quantifiersGravatar Clément Pit--Claudel2015-08-23
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
* Trivial code cleanupGravatar Clément Pit--Claudel2015-08-23
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
* Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
* Rephrase the message about triggers being rejected because they are too strongGravatar Clément Pit--Claudel2015-08-21
* Allow display expressions as trigger termsGravatar Clément Pit--Claudel2015-08-21
* Cleanup a number of FIXMEs that I had left in the codeGravatar Clément Pit--Claudel2015-08-20
* Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
* Move indentation of error messages to the ConsoleErrorReporterGravatar Clément Pit--Claudel2015-08-20
* Simplify error reporting in the trigger generator to get cleaner messagesGravatar Clément Pit--Claudel2015-08-20
* Allow users to disable quantifier splitting by with a {:split false} attributeGravatar Clément Pit--Claudel2015-08-20
* Print matches for triggers as they appear in the bufferGravatar Clément Pit--Claudel2015-08-19
* Enable unicode output in the VS extensionGravatar Clément Pit--Claudel2015-08-19
* Collect ApplyExpr nodes when looking for trigger candidatesGravatar Clément Pit--Claudel2015-08-19
* Fix the equality test for literal expressionsGravatar Clément Pit--Claudel2015-08-19
* Generate triggers for nested quantifiers as wellGravatar Clément Pit--Claudel2015-08-19
* Slightly improve the condition used to filter out trigger setsGravatar Clément Pit--Claudel2015-08-18
* Use nested tokens in the quantifier splitterGravatar Clément Pit--Claudel2015-08-18
* Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
* Small cleanups, fixes, and refactoringsGravatar Clément Pit--Claudel2015-08-18
* Use a nice warning symbol in some warning messagesGravatar Clément Pit--Claudel2015-08-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:16:45 +0000