summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* [IronDafny] implemented workaround for "import opened" bug(s).Gravatar Michael Lowell Roberts2015-07-13
* Auto-merged heads.Gravatar Michael Lowell Roberts2015-07-08
|\
* | added unit tests for exclusive refinement.Gravatar Michael Lowell Roberts2015-07-08
| * 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
| * 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
|/
* Added another lemma to a test fileGravatar Rustan Leino2015-07-02
* MergeGravatar leino2015-07-01
|\
* | Fixed bug in BplImp!Gravatar leino2015-07-01
| * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
* | Fixed bugs in encoding of preconditions of function values, Issue #84.Gravatar leino2015-06-30
* | Additional test case for instance functionsGravatar leino2015-06-30
|/
* MergeGravatar leino2015-06-25
|\
* | Tried to reduce frame-axiom instantiations by saying the earlier heap must be...Gravatar leino2015-06-25
* | Removed unneeded :heapQuantifier from test case (rendinging this attribute cu...Gravatar leino2015-06-25
| * Fix various bugs in nested match patterns listed in issue #83Gravatar qunyanm2015-06-19
|/
* 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
* Some more reads testsGravatar Rustan Leino2015-06-15
* More reads testsGravatar Rustan Leino2015-06-15
* Postpone reads checks of function preconditions until after the entire precon...Gravatar leino2015-06-15
* More tests of reads-clause checkingGravatar Rustan Leino2015-06-15
* MergeGravatar leino2015-06-12
|\
* | Added /vcs... cop-out to test case to make it go throughGravatar 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
| * MergeGravatar Clément Pit--Claudel2015-06-12
| |\
| * | Small fix in runTests.pyGravatar Clément Pit--Claudel2015-06-12
| | * mergeGravatar Michael Lowell Roberts2015-06-12
| | |\ | | |/ | |/|
| | * added -optimize option to compiler.Gravatar Michael Lowell Roberts2015-06-12
| |/ |/|
| * Add missing default parameter in runTests.pyGravatar Clément Pit--Claudel2015-06-11
| * A few more improvements to runTests.pyGravatar Clément Pit--Claudel2015-06-11
| * Small improvements to runTests.pyGravatar Clément Pit--Claudel2015-06-10
|/
* Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero.Gravatar Clément Pit--Claudel2015-06-07
* Fix lit headers implicitly relying on bash-style constructsGravatar Clément Pit--Claudel2015-06-08
* Add the beginning of a new testing infrastructureGravatar Clément Pit--Claudel2015-06-08
* Generate #requires function for OpaqueFunction.Gravatar qunyanm2015-06-04
* MergeGravatar leino2015-05-29
|\
| * Add an infinite set collection type.Gravatar qunyanm2015-05-29
* | Improvements in traits test caseGravatar leino2015-05-29
* | Improvements to Nipkow and Klein test cases: Changed imap to map, removed ne...Gravatar leino2015-05-29
|/
* Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.Gravatar qunyanm2015-05-18
* Updated test output after change in Boogie.Gravatar wuestholz2015-05-17
* Fix issue #79. Allow tuple pattern matching with parenthesis only.Gravatar qunyanm2015-05-15
* Allow MatchExpr and MatchStmt to have nested patterns. Such asGravatar qunyanm2015-05-14
* Don't include arrow types among ordered types.Gravatar leino2015-05-11
* Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and Kle...Gravatar leino2015-05-10
* Additional test case for inductive predicatesGravatar leino2015-05-07