summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* 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
* Use /tracePO instead of /trace in the serverGravatar Clément Pit--Claudel2015-08-19
* 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
* Generate triggers for nested quantifiers as wellGravatar Clément Pit--Claudel2015-08-19
* Merge.Gravatar Clément Pit--Claudel2015-08-19
|\
* | Server: disable tracing when running tests, and fix an encoding issue.Gravatar Clément Pit--Claudel2015-08-18
* | 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
* | 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
| * 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
* | Implement self-loop detectionGravatar Clément Pit--Claudel2015-08-14
* | 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
* | Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
* | 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 cl...Gravatar leino2015-08-12
* | | 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
| * 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
* 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
| | |\
| * | | Bug fix: check that assign-such-that constraint is of type booleanGravatar Rustan Leino2015-07-31
| | |/ | |/|
* | | Add a Linux z3 binary to the repo, and use that or z3.exe based on the OSGravatar Clément Pit--Claudel2015-07-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 19:34:42 +0000