summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
* MergeGravatar leino2014-08-05
|\
* | Resolved further merge issuesGravatar leino2014-08-05
| |
| * Tests for non-terminating computations. Already passing.Gravatar Nada Amin2014-08-05
| |
* | MergeGravatar leino2014-08-02
|\|
* | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵Gravatar leino2014-08-02
| | | | | | | | the resolver and translator
| * added one more test caseGravatar Reza Ahmadi2014-07-31
| |
| * combined few testsGravatar Reza Ahmadi2014-07-31
| |
| * combined two testsGravatar Reza Ahmadi2014-07-31
| |
| * MergeGravatar Reza Ahmadi2014-07-31
| |\
| | * Changed test case to not use '/doNotUseParallelism' anymore.Gravatar wuestholz2014-07-31
| | |
* | | Test file whitespace deltaGravatar leino2014-07-23
| |/ |/|
| * added one more test.Gravatar Reza Ahmadi2014-07-20
| |
| * - fixed a bug in inheriting members from a traitGravatar Reza Ahmadi2014-07-20
| | | | | | | | | | | | | | => ResolvedClass in userdefinedtypes used to be null-> fixed - checking only bodyless methods and functions to make sure they have been implemented in the child class - added one more test
| * fixed one .expect file. now all 11 tests related to Traits pass.Gravatar Reza Ahmadi2014-07-20
| |
| * - fixed an issue regarding including ghost functions in the compiled interfaceGravatar Reza Ahmadi2014-07-20
| | | | | | | | - added one more test
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/ | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* An attempt at making dafny4/NumberRepresentations.dfy run faster and more ↵Gravatar Rustan Leino2014-07-15
| | | | predictably
* Renamed "arbitrary type" to "opaque type"Gravatar Rustan Leino2014-07-15
|
* Allow an arbitrary-type to take type parametersGravatar Rustan Leino2014-07-15
|
* Added more tests.Gravatar wuestholz2014-07-15
|
* Another variation of GenericSort, this time instantiating with "int"Gravatar Rustan Leino2014-07-14
|
* MergeGravatar Rustan Leino2014-07-14
|\
* | Support for type synonyms in refinementsGravatar Rustan Leino2014-07-14
| | | | | | | | Started allowing arbitrary types to have type parameters
| * Added a test.Gravatar wuestholz2014-07-13
|/
* MergeGravatar Rustan Leino2014-07-11
|\
* | Added type synonyms. (No support yet for these in refinements.)Gravatar Rustan Leino2014-07-11
| |
| * Check that type arguments to map display expressions are fully resolvedGravatar Dan Rosén2014-07-11
|/ | | | Also add a test case for the different display expressions.
* Make reveal axioms from opaque functions quantify over layersGravatar Dan Rosén2014-07-10
|
* Added more tests for the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* MergeGravatar Rustan Leino2014-07-09
|\
* | Improved AnalyzeList encoding in a way that performs way better.Gravatar Rustan Leino2014-07-09
| | | | | | | | Cleaned up file to use some improved Dafny constructs.
* | Include an explicit trigger to make NumberRepresentations.dfy behave more ↵Gravatar Rustan Leino2014-07-09
| | | | | | | | consistently. (There is a future opportunity to heuristically figure out such triggers.)
| * Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
|/
* Further resolved merge conflictsGravatar Rustan Leino2014-07-08
|
* MergeGravatar Rustan Leino2014-07-08
|\
* | Test cases for int<->real conversionsGravatar Rustan Leino2014-07-08
| |
* | Cleaned up a test programGravatar Rustan Leino2014-07-08
| |
| * Tidy up two files in test suiteGravatar Dan Rosen2014-07-07
| |
| * MergeGravatar Dan Rosén2014-07-07
| |\
| * | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| | |
| | * MergeGravatar leino2014-07-03
| | |\
| | | * Changed "dummy" checksums to "stable" and added more tests for the ↵Gravatar wuestholz2014-07-03
| | | | | | | | | | | | | | | | verification result caching.
* | | | Updated expected test results for previous check-inGravatar Rustan Leino2014-07-02
| | | |
* | | | Fixed a crash in the translation of fresh(seq<T>).Gravatar Rustan Leino2014-07-02
| |_|/ |/| |
| | * Allow array-type parameters to be filled in automatically.Gravatar leino2014-07-02
| | | | | | | | | | | | Enhanced filling in of datatype parameters: allow places that need only a prefix of the parameters of the datatype
| | * MergeGravatar leino2014-07-01
| | |\ | |_|/ |/| |
* | | Removed the old test infrastructure.Gravatar wuestholz2014-07-01
| | |
* | | Added support for verifying Dafny program snapshots from the command-line.Gravatar wuestholz2014-07-01
| | |
* | | Added tuples and tuple types. Syntax is the expected one, namely parentheses ↵Gravatar Rustan Leino2014-06-27
| | | | | | | | | | | | around a comma-delimited list of expressions or types. Unit and the unit type are denoted ().
| | * MergeGravatar leino2014-06-24
| | |\ | |_|/ |/| |