summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Move indentation of error messages to the ConsoleErrorReporterGravatar Clément Pit--Claudel2015-08-20
| | | | This indentation is just needed by CLI-based clients
* Discard error messages that refer to a non-nested TokenWrapper.Gravatar Clément Pit--Claudel2015-08-20
| | | | | | | | The VS extension already did that, but it also filtered out nested tokens. That prevented info about triggers from being reported. Other interfaces (the CLI and Emacs, in particular) should have the same ability. Surprinsingly, this doesn't cause any tests failures.
* Add unit tests for trigger-related error messagesGravatar Clément Pit--Claudel2015-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
|
* Add a test to show how trigger splitting balances the downsides of loop ↵Gravatar Clément Pit--Claudel2015-08-20
| | | | detection
* Allow users to disable quantifier splitting by with a {:split false} attributeGravatar Clément Pit--Claudel2015-08-20
|
* Add a wishlist folder to the test suite, with things that we do not support ↵Gravatar Clément Pit--Claudel2015-08-19
| | | | | | | (yet!) The curent examples include semi-bugs regarding calc statements and strings, and stuff about sequences
* Add a test to check that there are as many errors as failed preconditionsGravatar Clément Pit--Claudel2015-08-19
|
* Add tests for quantifier splitting and trigger generationGravatar Clément Pit--Claudel2015-08-19
|
* Print matches for triggers as they appear in the bufferGravatar Clément Pit--Claudel2015-08-19
| | | | | Triggers themselves, however, are printed exactly as used. For example, a term (x !in s) yields a trigger (x in s).
* Add a check for SplitQuantifiers that had been incorrectly left out from the ↵Gravatar Clément Pit--Claudel2015-08-19
| | | | merge
* Factor out some AST visiting codeGravatar Clément Pit--Claudel2015-08-19
|
* runTests: Accept tests one by one, even if they are given as a .lst fileGravatar Clément Pit--Claudel2015-08-19
|
* Use /tracePO instead of /trace in the serverGravatar Clément Pit--Claudel2015-08-19
| | | | | This removes the need for special treatment of test input (/trace includes timings in the output, which are not suitable for tests. /tracePO does not)
* Enable unicode output in the VS extensionGravatar Clément Pit--Claudel2015-08-19
|
* server: always print tooltipsGravatar 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
| | | | (compare by value, not by reference to boxed value)
* Generate triggers for nested quantifiers as wellGravatar Clément Pit--Claudel2015-08-19
| | | | | | The new 'quantifiers' list keeps track of the quantifiers that have already been seen, so that they are not added both as a member of a collection and as a single quantifier.
* Merge.Gravatar Clément Pit--Claudel2015-08-19
|\ | | | | | | | | Changes that were needed included preventing the InductionRewriter from iterating on a SplitQuantifier and using the new error reporting engine.
* | runTests: Include failed tests in mean completion timeGravatar Clément Pit--Claudel2015-08-19
| |
* | runTests: Report mean completion time of passed tests, excluding outliersGravatar Clément Pit--Claudel2015-08-18
| |
* | Server: disable tracing when running tests, and fix an encoding issue.Gravatar Clément Pit--Claudel2015-08-18
| | | | | | | | | | | | z3 doesn't support byte-order marks; thus using the default UTF8Encoding object (to allow printing nice warning signs) causes issues, as it sends a BOM before anything else.
* | Slightly improve the condition used to filter out trigger setsGravatar Clément Pit--Claudel2015-08-18
| |
* | Check Reads and Decreases clauses for expressions that could prevent inliningGravatar Clément Pit--Claudel2015-08-18
| |
* | Exclude folders named 'sandbox' from lit testsGravatar Clément Pit--Claudel2015-08-18
| |
* | Refactor calls to 'new CallCmd' and clear a few FIXMEsGravatar Clément Pit--Claudel2015-08-18
| |
* | Use nested tokens in the quantifier splitterGravatar Clément Pit--Claudel2015-08-18
| | | | | | | | | | This allows it to report the source of the error, giving better feedback to the user about which precondition to a function failed to hold, for example.
* | Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
| |
* | Small cleanups, fixes, and refactoringsGravatar Clément Pit--Claudel2015-08-18
| | | | | | | | | | In particular, start detecting loops between terms that don't look like each other at the Dafny level, such as {a[x]} and {x in a} (when a is a multiset)
* | Use a nice warning symbol in some warning messagesGravatar Clément Pit--Claudel2015-08-18
| | | | | | | | | | This is useful because trigger-related messages can contain quite a bit of information, especially if they include info about multiple split quantifiers.
| * Changed hover-text location for recursive ind/co-lemma callsGravatar Rustan Leino2015-08-17
| |
| * Update the way bounds are discovered to try to choose "better" bounds.Gravatar Bryan Parno2015-08-17
| |
* | Review preceding commit with RustanGravatar Clément Pit--Claudel2015-08-17
| |
* | Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
| | | | | | | | | | | | | | | | | | This requires rewriting the parts of the AST that contain these quantifiers. We unfortunately don't have facilities to do such rewrites at the moment (and there are loops in the AST, so it would be hard to write such a facility). As a workaround, this commit introduces a field in quantifier expressions, SplitQuantifiers. Code that manipulate triggers is expected to look for this field, and ignore the other fields if that one is found.
* | Implement self-loop detectionGravatar Clément Pit--Claudel2015-08-14
| | | | | | | | | | | | | | | | | | | | Implementing loop detection between multiple triggers is much harder, as it seems to require walking an exponentially sized graph. Self-loop detection is still a net gain compared to the current situation: we used to not detect loops in large quantifiers; not we break these apart, suppress the loops where we can in the smaller parts, and report the ones that we can't suppress. It could be that the broken-up quantifiers are mutually recursive, but these cases would have already led to a loop in the past.
* | Start committing generated triggers when /autoTriggers is 1Gravatar Clément Pit--Claudel2015-08-14
| |
* | Run the trigger rewriter after the quantifier splitterGravatar Clément Pit--Claudel2015-08-14
| |
* | Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
| | | | | | | | This new version will include a cleaner pipeline, and trigger splitting.
* | Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| | | | | | | | | | The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
* | server: Add a Checked configurationGravatar Clément Pit--Claudel2015-08-14
| |
| * MergeGravatar Clément Pit--Claudel2015-08-13
| |\
| * | Update INSTALL notes to mention the wrapper scriptGravatar Clément Pit--Claudel2015-08-13
| | |
| * | Add a UniqueIdPrefix in the server and bump up the prover kill timeGravatar Clément Pit--Claudel2015-08-13
| | |
| | * Add a wrapper script around the Dafny binary (for mono).Gravatar Clément Pit--Claudel2015-08-13
| | |
| | * Changed dafny3/Filter.dfy to use higher-order functions instead of the ↵Gravatar leino2015-08-12
| | | | | | | | | | | | previous function handles
| | * Change the induction heuristic for lemmas to also look in precondition for ↵Gravatar leino2015-08-12
| | | | | | | | | | | | | | | | | | clues about which parameters to include. As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.
* | | Add a few utility methods to the visitorsGravatar Clément Pit--Claudel2015-08-12
| | |
* | | runTests.py: Pretty-print stderr output to TRACE upon test failureGravatar Clément Pit--Claudel2015-08-12
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 23:58:59 +0000