summaryrefslogtreecommitdiff
path: root/Test/cloudmake
Commit message (Collapse)AuthorAge
* Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresGravatar qunyanm2016-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 ↵Gravatar Rustan Leino2015-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>").Gravatar leino2014-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"Gravatar Rustan Leino2014-07-15
|
* Removed the old test infrastructure.Gravatar wuestholz2014-07-01
|
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Moved the (long running) CloudMake test files to their own directoryGravatar Rustan Leino2014-02-28