diff options
| author |  tabarbe <unknown> | 2010-07-29 22:15:48 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-29 22:15:48 +0000 |
| commit | 4a9e9a62ff2d9a530e56c8ed9c3f6bae2b9bf8d4 (patch) | |
| tree | bddf8c3b127c3b7ec7f9a84456c1da3f220d182a /Test/alltests.txt | |
| parent | 0bfac83cfa77e5f14d2c10f225436151eb98fbf0 (diff) | |
Boogie: Added a new simple regression test, "sanity", which runs a single 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.)
Diffstat (limited to 'Test/alltests.txt')
| -rw-r--r-- | Test/alltests.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Test/alltests.txt b/Test/alltests.txt index b566d8af..588a5eda 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -1,3 +1,4 @@ +sanity Use Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)
test0 Use Name resolution tests
test1 Use Typechecking tests
test2 Use VC generation
|