Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires | qunyanm | 2016-03-28 |
| | | | | | it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. | ||
* | Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ↵ | Rustan Leino | 2015-07-28 |
| | | | | | | time) in the test suite. Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do. | ||
* | Added types "char" and "string" (the latter being a synonym for "seq<char>"). | leino | 2014-10-20 |
| | | | | | | Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes. | ||
* | Renamed "arbitrary type" to "opaque type" | Rustan Leino | 2014-07-15 |
| | |||
* | Removed the old test infrastructure. | wuestholz | 2014-07-01 |
| | |||
* | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| | |||
* | Moved the (long running) CloudMake test files to their own directory | Rustan Leino | 2014-02-28 |