summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* 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
* | Small refactoring of Printer.csGravatar Clément Pit--Claudel2015-07-06
| * MergeGravatar Rustan Leino2015-07-02
| |\
| * | Added command-line option /warnShadowing, which emits warnings if variables s...Gravatar Rustan Leino2015-07-02
| * | Type parameters in method/function signatures are no longer auto-declared. A...Gravatar Rustan Leino2015-07-02
| | * multiple changes...Gravatar Michael Lowell Roberts2015-07-02
| |/
| * MergeGravatar leino2015-07-02
| |\
| | * Fixed a contract error provoked by one of the tests.Gravatar Bryan Parno2015-07-02
| * | Made code contracts compliantGravatar leino2015-07-01
| * | MergeGravatar leino2015-07-01
| |\|
| * | Fixed bug in BplImp!Gravatar leino2015-07-01
| | * Compile function methods into C# in a more efficient manner,Gravatar Bryan Parno2015-07-01
| | * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
| | * MergeGravatar Bryan Parno2015-07-01
| | |\
| | * | Add code to calculate various interesting statistics about Dafny files.Gravatar Bryan Parno2015-07-01
| |/ / |/| |
| * | Fixed bugs in encoding of preconditions of function values, Issue #84.Gravatar leino2015-06-30
| |/
| * Fix identifiers in nested match patterns not showing in the IDE bug. RememberGravatar qunyanm2015-06-29
|/
* MergeGravatar leino2015-06-25
|\
* | Tried to reduce frame-axiom instantiations by saying the earlier heap must be...Gravatar leino2015-06-25
| * Fix issue #85. Only try to interpret an identifier as a datatype constructorGravatar qunyanm2015-06-22
| * Fix various bugs in nested match patterns listed in issue #83Gravatar qunyanm2015-06-19
|/
* Auto-merged heads.Gravatar Michael Lowell Roberts2015-06-16
|\
* | System.Collections.Immutable.dll is now stored in the Binaries directory and ...Gravatar Michael Lowell Roberts2015-06-16
| * Changed logical order of requires and reads clauses on functions. Reads clausesGravatar Rustan Leino2015-06-15
| * Do postponsed reads checking also for the body of functions -- see Test/dafny...Gravatar Rustan Leino2015-06-15
| * Postpone reads checks of function preconditions until after the entire precon...Gravatar leino2015-06-15