summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* [IronDafny] fix for ambiguous identifier error.Gravatar Michael Lowell Roberts2015-07-15
* [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
* 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
* | Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero.Gravatar Clément Pit--Claudel2015-06-07
|/
* Generate #requires function for OpaqueFunction.Gravatar qunyanm2015-06-04
* Added {:auto_generated} trigger, which indicates that a declaration was not e...Gravatar Rustan Leino2015-06-02
* MergeGravatar leino2015-05-29
|\
| * Add an infinite set collection type.Gravatar qunyanm2015-05-29
* | MergeGravatar leino2015-05-29
|\|
* | Bug fix in type-antecedent for traits in allocation axiomsGravatar leino2015-05-29
| * MergeGravatar Rustan Leino2015-05-29
| |\
| * | Changes to ComputeFreeVariables--bug fix as well as beautificationGravatar Rustan Leino2015-05-29
| | * Fix build break. Part of the change was not checked in last check-in somehow.Gravatar qunyanm2015-05-19
| | * Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.Gravatar qunyanm2015-05-18
| | * DafnyExtension: Added experimental support for diagnosing timeouts.Gravatar wuestholz2015-05-18