summaryrefslogtreecommitdiff
path: root/Source
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.
* 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
| | | | | 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
|
* 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.
* | 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
| |
* | 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
| |\
| * | Add a UniqueIdPrefix in the server and bump up the prover kill timeGravatar Clément Pit--Claudel2015-08-13
| | |
| | * 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
|/ /
| * Bug fixes and improvements in pretty printingGravatar leino2015-08-11
| |
| * Disallow user-defined attributes that begin with an underscoreGravatar leino2015-08-11
| |
| * Removed the unused type ThisSurrogateGravatar leino2015-08-11
| |
| * Moved discovery of induction variables into a Rewriter.Gravatar leino2015-08-11
| | | | | | | | | | Generate warnings for malformed :induction arguments. Removed the functionality that allowed induction on 'this'.
| * Added routine OneAttributeToString to pretty printerGravatar leino2015-08-10
|/
* Tiny refactoring in the extension's driverGravatar Clément Pit--Claudel2015-07-31
|
* Fix an issue with column numbers in the VS extensionGravatar Clément Pit--Claudel2015-07-31
| | | | | | The error came from the fact that Dafny now consistently used 0-based indexing. Boogie gets its traces from text that's inserted by Dafny in the Boogie file, so there's no need to apply an extra offset in the VS extension.
* MergeGravatar Clément Pit--Claudel2015-07-31
|\
* | Integrate the DafnyServer project into the main Dafny solutionGravatar Clément Pit--Claudel2015-07-31
| |
| * Add path to DafnyPrelude.bpl from DafnyServer projectGravatar Rustan Leino2015-07-31
| |
| * MergeGravatar Rustan Leino2015-07-31
| |\
| | * MergeGravatar leino2015-07-31
| | |\ | |_|/ |/| |
| | * MergeGravatar leino2015-07-31
| | |\
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 21:46:52 +0000