summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
* | | 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
| * Little edits in new CheckWellformedAndAssume codeGravatar leino2015-06-12
| * MergeGravatar leino2015-06-12
| |\
| | * Fix a bug spotted by Chris in my BigInteger patch; thanks!Gravatar Clément Pit--Claudel2015-06-12
| |/ |/|
| * MergeGravatar leino2015-06-12
| |\ | |/ |/|
| * Combined some common routines into CheckWellformedAndAssume, which also allow...Gravatar leino2015-06-12
* | added -optimize option to compiler.Gravatar Michael Lowell Roberts2015-06-12
|/
* Add a compatibility layer over BigInteger.ParseGravatar Clément Pit--Claudel2015-06-07
* MergeGravatar Clément Pit--Claudel2015-06-08
|\
| * Update the hash code for datatypes to use the djb2 hash algorithm,Gravatar Bryan Parno2015-06-08
| * Fix some issues when compiling generic types and generic function method callsGravatar Bryan Parno2015-06-08