summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
| * | merged IronDafny updates. two unit tests related to traits do not pass if ENA...Gravatar Michael Lowell Roberts2015-09-21
* | | Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
| | * Fix a check that occasionally led to an out of bounds exception in the extensionGravatar Bryan Parno2015-09-17
| * | Only print extraneous comments if asked.Gravatar Michael Lowell Roberts2015-09-17
| |/
* | MergeGravatar leino2015-09-11
|\|
* | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing f...Gravatar leino2015-08-31
| * Align the server's default kill time with the one of the VS extensionGravatar Clément Pit--Claudel2015-08-28
| * 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
* Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)Gravatar 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
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...Gravatar Clément Pit--Claudel2015-08-23
* Grant "wishlist/useless-casts-in-decreases-clauses.dfy"Gravatar Clément Pit--Claudel2015-08-22
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
* | 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
* | 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
* | Give up on trying to set the console's input encoding to UTF8Gravatar 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
| * MergeGravatar Rustan Leino2015-08-20
| |\ | |/ |/|
| * Changed equality tests involving traits from using strings to using reference...Gravatar Rustan Leino2015-08-20
| * Minor refactoringGravatar Rustan Leino2015-08-20
| * Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
* | Make the dependency that DafnyServer has on DafnyPipeline explicitGravatar Clément Pit--Claudel2015-08-20
* | Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
* | Merge.Gravatar Clément Pit--Claudel2015-08-20
|\|
* | Move indentation of error messages to the ConsoleErrorReporterGravatar Clément Pit--Claudel2015-08-20
* | Discard error messages that refer to a non-nested TokenWrapper.Gravatar Clément Pit--Claudel2015-08-20
| * Fixed bug in type unificationGravatar Rustan Leino2015-08-20
| * MergeGravatar Rustan Leino2015-08-20
| |\
* | | Simplify error reporting in the trigger generator to get cleaner messagesGravatar Clément Pit--Claudel2015-08-20
* | | Mark a few reporting functions as staticGravatar 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
* | | Add a check for SplitQuantifiers that had been incorrectly left out from the ...Gravatar Clément Pit--Claudel2015-08-19
* | | Factor out some AST visiting codeGravatar Clément Pit--Claudel2015-08-19
| |/ |/|
| * Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
* | Use /tracePO instead of /trace in the serverGravatar Clément Pit--Claudel2015-08-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 21:49:35 +0000