Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | leino | 2014-08-05 |
|\ | |||
* | | Resolved further merge issues | leino | 2014-08-05 |
| | | |||
| * | Tests for non-terminating computations. Already passing. | Nada Amin | 2014-08-05 |
| | | |||
* | | Merge | leino | 2014-08-02 |
|\| | |||
* | | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵ | leino | 2014-08-02 |
| | | | | | | | | the resolver and translator | ||
| * | added one more test case | Reza Ahmadi | 2014-07-31 |
| | | |||
| * | combined few tests | Reza Ahmadi | 2014-07-31 |
| | | |||
| * | combined two tests | Reza Ahmadi | 2014-07-31 |
| | | |||
| * | Merge | Reza Ahmadi | 2014-07-31 |
| |\ | |||
| | * | Changed test case to not use '/doNotUseParallelism' anymore. | wuestholz | 2014-07-31 |
| | | | |||
* | | | Test file whitespace delta | leino | 2014-07-23 |
| |/ |/| | |||
| * | added one more test. | Reza Ahmadi | 2014-07-20 |
| | | |||
| * | - fixed a bug in inheriting members from a trait | Reza Ahmadi | 2014-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. | Reza Ahmadi | 2014-07-20 |
| | | |||
| * | - fixed an issue regarding including ghost functions in the compiled interface | Reza Ahmadi | 2014-07-20 |
| | | | | | | | | - added one more test | ||
| * | added trait feature: | Reza Ahmadi | 2014-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 ↵ | Rustan Leino | 2014-07-15 |
| | | | | predictably | ||
* | Renamed "arbitrary type" to "opaque type" | Rustan Leino | 2014-07-15 |
| | |||
* | Allow an arbitrary-type to take type parameters | Rustan Leino | 2014-07-15 |
| | |||
* | Added more tests. | wuestholz | 2014-07-15 |
| | |||
* | Another variation of GenericSort, this time instantiating with "int" | Rustan Leino | 2014-07-14 |
| | |||
* | Merge | Rustan Leino | 2014-07-14 |
|\ | |||
* | | Support for type synonyms in refinements | Rustan Leino | 2014-07-14 |
| | | | | | | | | Started allowing arbitrary types to have type parameters | ||
| * | Added a test. | wuestholz | 2014-07-13 |
|/ | |||
* | Merge | Rustan Leino | 2014-07-11 |
|\ | |||
* | | Added type synonyms. (No support yet for these in refinements.) | Rustan Leino | 2014-07-11 |
| | | |||
| * | Check that type arguments to map display expressions are fully resolved | Dan Rosén | 2014-07-11 |
|/ | | | | Also add a test case for the different display expressions. | ||
* | Make reveal axioms from opaque functions quantify over layers | Dan Rosén | 2014-07-10 |
| | |||
* | Added more tests for the more advanced verification result caching. | wuestholz | 2014-07-10 |
| | |||
* | Merge | Rustan Leino | 2014-07-09 |
|\ | |||
* | | Improved AnalyzeList encoding in a way that performs way better. | Rustan Leino | 2014-07-09 |
| | | | | | | | | Cleaned up file to use some improved Dafny constructs. | ||
* | | Include an explicit trigger to make NumberRepresentations.dfy behave more ↵ | Rustan Leino | 2014-07-09 |
| | | | | | | | | consistently. (There is a future opportunity to heuristically figure out such triggers.) | ||
| * | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 |
|/ | |||
* | Further resolved merge conflicts | Rustan Leino | 2014-07-08 |
| | |||
* | Merge | Rustan Leino | 2014-07-08 |
|\ | |||
* | | Test cases for int<->real conversions | Rustan Leino | 2014-07-08 |
| | | |||
* | | Cleaned up a test program | Rustan Leino | 2014-07-08 |
| | | |||
| * | Tidy up two files in test suite | Dan Rosen | 2014-07-07 |
| | | |||
| * | Merge | Dan Rosén | 2014-07-07 |
| |\ | |||
| * | | New logical encoding of types with Is and IsAlloc | Dan Rosén | 2014-07-07 |
| | | | |||
| | * | Merge | leino | 2014-07-03 |
| | |\ | |||
| | | * | Changed "dummy" checksums to "stable" and added more tests for the ↵ | wuestholz | 2014-07-03 |
| | | | | | | | | | | | | | | | | verification result caching. | ||
* | | | | Updated expected test results for previous check-in | Rustan Leino | 2014-07-02 |
| | | | | |||
* | | | | Fixed a crash in the translation of fresh(seq<T>). | Rustan Leino | 2014-07-02 |
| |_|/ |/| | | |||
| | * | Allow array-type parameters to be filled in automatically. | leino | 2014-07-02 |
| | | | | | | | | | | | | Enhanced filling in of datatype parameters: allow places that need only a prefix of the parameters of the datatype | ||
| | * | Merge | leino | 2014-07-01 |
| | |\ | |_|/ |/| | | |||
* | | | Removed the old test infrastructure. | wuestholz | 2014-07-01 |
| | | | |||
* | | | Added support for verifying Dafny program snapshots from the command-line. | wuestholz | 2014-07-01 |
| | | | |||
* | | | Added tuples and tuple types. Syntax is the expected one, namely parentheses ↵ | Rustan Leino | 2014-06-27 |
| | | | | | | | | | | | | around a comma-delimited list of expressions or types. Unit and the unit type are denoted (). | ||
| | * | Merge | leino | 2014-06-24 |
| | |\ | |_|/ |/| | |