summaryrefslogtreecommitdiff
path: root/Test/alltests.txt
diff options
context:
space:
mode:
Diffstat (limited to 'Test/alltests.txt')
-rw-r--r--Test/alltests.txt13
1 files changed, 7 insertions, 6 deletions
diff --git a/Test/alltests.txt b/Test/alltests.txt
index 588a5eda..4b12e6fd 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -1,4 +1,4 @@
-sanity Use Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)
+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
@@ -15,15 +15,16 @@ textbook Use Some textbook examples
test15 Use Benchmarks for error messages
bitvectors Use Smoke tests for bitvectors
smoke Use Soundness smoke testing
-test16 Use Tests methodology of visible-state semantics and loop unrolling
+test16 Use Tests loop unrolling
+codeexpr Use Tests code expressions
test17 Postponed Tests inference of parameterized contracts
z3api Postponed Test for Z3 Managed .NET API prover
houdini Postponed Test for Houdini decision procedure
dafny0 Use Dafny functionality tests
-dafny1 Use Various Dafny examples
+dafny1 Use Various Dafny examples
havoc0 Use HAVOC-generated bpl files
VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
-livevars Use STORM benchmarks for testing correctness of live variable analysis
-lazyinline Use Lazy inlining benchmarks
-stratifiedinline Use Stratified inlining benchmarks
+livevars Use STORM benchmarks for testing correctness of live variable analysis
+lazyinline Use Lazy inlining benchmarks
+stratifiedinline Use Stratified inlining benchmarks