summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* 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
* 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
* 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
* 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
| | |/ | |/|
* | | Update install notes and test themGravatar Clément Pit--Claudel2015-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
| | * Allow forall statements in refinementsGravatar leino2015-07-31
* | | Add tests for the serverGravatar Clément Pit--Claudel2015-07-31
* | | Update .ignoreGravatar Clément Pit--Claudel2015-07-31
* | | Split the server source into multiple filesGravatar Clément Pit--Claudel2015-07-31
* | | Fix an issue where the server would reverify the same file multiple times.Gravatar Clément Pit--Claudel2015-07-30
|/ /
* | Add quotes in snapshot tests.Gravatar Clément Pit--Claudel2015-07-30
* | Implement a Dafny server.Gravatar Clément Pit--Claudel2015-07-30
* | Fixed crash in resolution where, after reporting an error, the cases #type an...Gravatar Rustan Leino2015-07-29
* | Update the VS extension to use the error interface defined in 576eac2e17ffGravatar Clément Pit--Claudel2015-07-29
* | MergeGravatar Clément Pit--Claudel2015-07-28
|\ \
* | | Save failing tests to failing.lst, making it easy to re-run themGravatar Clément Pit--Claudel2015-07-28
| * | Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...Gravatar Rustan Leino2015-07-28
| * | Updated parser generation to work with latest update in boogiepartners. Note ...Gravatar Rustan Leino2015-07-27
| |/
* | Clarify the inlining warning.Gravatar Clément Pit--Claudel2015-07-27
* | Small refactoringGravatar Clément Pit--Claudel2015-07-27
* | Clean up error reporting.Gravatar Clément Pit--Claudel2015-07-27
| * Renamed "ghost method" to "lemma" in a couple of test filesGravatar Rustan Leino2015-07-24
| * Translate triggers with the same ExpressionTranslator as the bodyGravatar Rustan Leino2015-07-24
|/
* Update DafnyExtension to use the parser constructor introduced in d2e394fc4b93Gravatar Clément Pit--Claudel2015-07-24
* MergeGravatar Clément Pit--Claudel2015-07-23
|\
| * Bump up the time limit in runTests.py and save a bit of space in outputGravatar Clément Pit--Claudel2015-07-23
| * Fix: Read clauses should be checked before lit liftingGravatar Clément Pit--Claudel2015-07-23
| * Fix a bug with includes and /useBaseNameForFileNameGravatar Clément Pit--Claudel2015-07-23
| * Let runTests.py generate expect filesGravatar Clément Pit--Claudel2015-07-23
| * Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
| * Fix: Visual studio did not show warnings.Gravatar Clément Pit--Claudel2015-07-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 14:12:43 +0000