summaryrefslogtreecommitdiff
path: root/Test/alltests.txt
blob: ebe396e9733a0bce9df89e8fe6ac0827033671e7 (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
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        Use	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
AbsHoudini       Postponed    Test for abstract houdini