summaryrefslogtreecommitdiff
path: root/Test/alltests.txt
blob: 0236e694ad9a903c4f3c7595412f96c96292c1e5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
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
test7            Use    Some tests for VCVariety.BlockNested
test20           Use    Types introduced in Boogie2
test21           Use    Verify Boogie 2 programs
aitest0          Use    Constant propagation test
aitest1          Use    Linear ineqality test
aitest9          Use    Test for the abstract domain of intervals
lock             Use    SLAM example
test13           Use    error messages for failing asserts vs. loop invariants
inline           Use    Procedure inlining
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 loop unrolling
codeexpr         Use    Tests code expressions
prover           Use    Tests checking various prover options
test17           Postponed    Tests inference of parameterized contracts
z3api            Postponed    Test for Z3 Managed .NET API prover
houdini          Use    Test for Houdini decision procedure
datatypes        SoonToBeIncluded	Test for datatypes
generalizedarray Use	Test for generalized array theory
livevars         Use    STORM benchmarks for testing correctness of live variable analysis
stratifiedinline Use    Stratified inlining benchmarks
extractloops     Use    Extract loops benchmarks
havoc0           Use    HAVOC-generated bpl files
dafny0           Use    Dafny functionality tests
dafny1           Use    Various Dafny examples
dafny2           Use    More Dafny examples
VSI-Benchmarks   Use    Solutions to Verified Software Initiative verification challenges
vacid0           Use    Dafny attempts to VACID Edition 0 benchmarks
vstte2012        Use    Dafny solutions for the VSTTE 2012 program verification competition
VSComp2010       Use    Dafny solutions to VSComp (verified software competition) problems