summaryrefslogtreecommitdiff
path: root/Test/sanity
Commit message (Collapse)AuthorAge
* Add lit.local.cfg that instructs not to run any tests in thisGravatar Dan Liew2014-05-05
| | | | | | | directory or its subdirectories. The test in this directory is pointless because we will run it later on anyway! When we migrate to lit this test directory should be removed
* Disengaged Dafny testsGravatar Rustan Leino2012-11-20
|
* Dafny: re-ran parser generator to include semicolon-less body-less ↵Gravatar Rustan Leino2011-07-26
| | | | functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
* Fixed regression test failures due to removal of bodiless methods and functions.Gravatar Jason Koenig2011-07-15
|
* Reflect effect of Celebrity.dfy change in previous check-inGravatar rustanleino2011-03-27
|
* Updated answer to this regression to reflect the fact that it is now verified.Gravatar tabarbe2010-08-12
|
* Boogie: This reg test was not running verification.Gravatar tabarbe2010-08-12
|
* Boogie: That file should not have been in the depot, but rather be created ↵Gravatar tabarbe2010-08-09
| | | | locally
* Boogie: Added a new simple regression test, "sanity", which runs a single ↵Gravatar tabarbe2010-07-29
test for Boogie and a single test for Dafny, just to check for grievous runtime errors in the code. (In my porting, I work with code that, in some cases, is not tested until the 3rd or 4th regression test. These 2 test files should make use of that more obscure code and alert me to my errors quickly, rather than making me wait through a full regression cycle.)