summaryrefslogtreecommitdiff
path: root/Source/Dafny
Commit message (Expand)AuthorAge
* Added routine OneAttributeToString to pretty printerGravatar leino2015-08-10
* 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
| |/ |/|
| * Allow forall statements in refinementsGravatar leino2015-07-31
* | 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
|\ \
| * | 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
| * Translate triggers with the same ExpressionTranslator as the bodyGravatar Rustan Leino2015-07-24
|/
* MergeGravatar 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
| * 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
| * IronDafny related changes:Gravatar Michael Lowell Roberts2015-07-22
* | MergeGravatar Clément Pit--Claudel2015-07-21
|\|
* | Simplify some of the deduplication code in TriggerGenerator.csGravatar Clément Pit--Claudel2015-07-21
| * Improved rank axioms for containersGravatar Rustan Leino2015-07-21
| * Code reviewed some of the triggers added by changeset 1dacb6d3cc3cGravatar Rustan Leino2015-07-21
|/
* MergeGravatar Clément Pit--Claudel2015-07-20
|\
* | Add calc's attributes to its SubExpressions.Gravatar Clément Pit--Claudel2015-07-20
| * clarified error message that occurs when the "opened" keyword is left off of ...Gravatar Michael Lowell Roberts2015-07-20
| * fix for apparent typo in Rewriter.csGravatar Michael Lowell Roberts2015-07-20
|/
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\
* | Clean up new trigger declarations in Translator.csGravatar Clément Pit--Claudel2015-07-17
* | Fix column numbers in warning and info messagesGravatar Clément Pit--Claudel2015-07-16
* | Clean up a few thing and set proper defaults before mergingGravatar Clément Pit--Claudel2015-07-16
| * MergeGravatar Rustan Leino2015-07-16
| |\
| | * Fixed bugs in the parsing of explicit type arguments.Gravatar Rustan Leino2015-07-16
* | | Force IsTriggerKiller to return false when /autoTriggers is offGravatar Clément Pit--Claudel2015-07-16
* | | Use MapConcat instead of String.Join in TriggerGeneratorGravatar Clément Pit--Claudel2015-07-16
* | | Strip literals from triggersGravatar Clément Pit--Claudel2015-07-16
| * | [IronDafny] fix for ambiguous identifier error.Gravatar Michael Lowell Roberts2015-07-15
* | | Weaken the trigger cycling check to allow more patternsGravatar Clément Pit--Claudel2015-07-15
* | | Fix broken interaction between triggers and inlining of function callsGravatar Clément Pit--Claudel2015-07-14
* | | Detect matching loops at the mutli-trigger levelGravatar Clément Pit--Claudel2015-07-13
* | | Start adding missing triggers to the translatorGravatar Clément Pit--Claudel2015-07-13
* | | Add /printTooltips and /autoTriggers to the CLIGravatar Clément Pit--Claudel2015-07-13
* | | Register the trigger generator as a a rewriter in the Resolver.Gravatar Clément Pit--Claudel2015-07-13
* | | Initial import of the TriggerGenerator code.Gravatar Clément Pit--Claudel2015-07-13
* | | Make attributes enumerable.Gravatar Clément Pit--Claudel2015-07-13
| * | [IronDafny] implemented workaround for "import opened" bug(s).Gravatar Michael Lowell Roberts2015-07-13
| |/
| * Fixed crashes in overrides checking of function decreases clauses, and improv...Gravatar Rustan Leino2015-07-07
| * Report warnings only once. (This is the last step in fixing Issue #86.)Gravatar Rustan Leino2015-07-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 03:37:56 +0000