Benchmark | KLEE | TBF Test-Suite Validator | ||||||||||||||||||||||||
Tool | KLEE 2.0.0-pre-test-comp | Tbf Test-suite Validator v1.2 | ||||||||||||||||||||||||
Limits | timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 | timelimit: 10800 s, memlimit: 7000 MB, CPU core limit: 2 | ||||||||||||||||||||||||
Host | apollon* | |||||||||||||||||||||||||
OS | Linux 4.15.0-45-generic | |||||||||||||||||||||||||
System | CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB | |||||||||||||||||||||||||
Date of execution | 2019-02-05 21:09:47 CET | 2019-02-06 06:16:47 CET | ||||||||||||||||||||||||
Run set | klee.test-comp19_prop-coverage-branches.ReachSafety-Heap | tbf-testsuite-validator-klee.test-comp19_prop-coverage-branches.ReachSafety-Heap | ||||||||||||||||||||||||
Options | --verbose --sequence-file cov-seq.txt -r --test-suite ../../results-verified/klee.2019-02-05_2109.logfiles/${rundefinition_name}.${inputfile_name}.files/test-suite.zip | |||||||||||||||||||||||||
sv-benchmarks/c/ldv-regression/ | status | score | program | test-suite | TS size | inspect test-suite | cpu (s) | wall (s) | mem (MB) | energy (J) | blkio-w (MB) | blkio-r (MB) | status | program | test-suite | TS size | inspect test-suite | cov | branch cov (%) | line cov (%) | cpu (s) | wall (s) | mem (MB) | energy | blkio-w (MB) | blkio-r (MB) |
alias_of_return_2.c_1.yml | done | .25 | prog | tests | 1 | inspect | .13 | .15 | 21 | 1.3 | .016 | 0 | unknown | prog | tests | 0 | inspect | 25.0 | 45.5 | .12 | .12 | 17 | .078 | 0 | ||
alias_of_return_2.yml | done | .75 | prog | tests | 3 | inspect | .11 | .13 | 21 | 1.6 | .016 | 0 | unknown | prog | tests | 0 | inspect | 75.0 | 81.8 | .12 | .12 | 17 | .11 | 0 | ||
fo_test.yml | false(unreach-call) | 1.0 | prog | tests | 3 | inspect | .12 | .12 | 21 | 1.3 | .016 | 0 | true | prog | tests | 1 | inspect | 100 | 100 | .16 | .21 | 17 | .20 | 0 | ||
rule60_list2.c_1.yml | false(unreach-call) | .929 | prog | tests | 16 | inspect | .12 | .14 | 21 | 1.7 | .016 | 0 | true | prog | tests | 1 | inspect | 92.9 | 100 | .20 | .21 | 17 | .76 | 0 | ||
rule60_list2.yml | done | .857 | prog | tests | 13 | inspect | .11 | .13 | 21 | 1.4 | .016 | 0 | unknown | prog | tests | 0 | inspect | 85.7 | 92.9 | .18 | .17 | 16 | .63 | 0 | ||
sizeofparameters_test.yml | done | .5 | prog | tests | 1 | inspect | .11 | .13 | 21 | 1.8 | .016 | 0 | unknown | prog | tests | 0 | inspect | 50.0 | 80.0 | .13 | .13 | 16 | .078 | 0 | ||
test10.yml | done | .5 | prog | tests | 1 | inspect | .12 | .14 | 21 | 1.2 | .016 | 0 | unknown | prog | tests | 0 | inspect | 50.0 | 95.5 | .13 | .13 | 17 | .078 | 0 | ||
test11.yml | done | .6 | prog | tests | 4 | inspect | .13 | .15 | 22 | 1.3 | .016 | 0 | unknown | prog | tests | 0 | inspect | 60.0 | 86.7 | .12 | .12 | 16 | .13 | 0 | ||
test14.yml | done | .625 | prog | tests | 4 | inspect | .13 | .15 | 21 | 1.1 | .016 | 0 | unknown | prog | tests | 0 | inspect | 62.5 | 91.7 | .13 | .14 | 17 | .13 | 0 | ||
test15.yml | done | .5 | prog | tests | 1 | inspect | .12 | .14 | 21 | 1.1 | .016 | 0 | unknown | prog | tests | 0 | inspect | 50.0 | 80.0 | .11 | .11 | 17 | .078 | 0 | ||
test19.yml | done | .5 | prog | tests | 1 | inspect | .13 | .15 | 21 | 1.1 | .016 | 0 | unknown | prog | tests | 0 | inspect | 50.0 | 85.7 | .12 | .14 | 16 | .078 | 0 | ||
test21-1.yml | done | .75 | prog | tests | 7 | inspect | .12 | .14 | 21 | 1.5 | .016 | 0 | unknown | prog | tests | 0 | inspect | 75.0 | 88.9 | .14 | .13 | 16 | .18 | 0 | ||
test21-2.yml | false(unreach-call) | .875 | prog | tests | 9 | inspect | .11 | .13 | 21 | 1.6 | .016 | 0 | true | prog | tests | 1 | inspect | 87.5 | 100 | .15 | .17 | 16 | .21 | 0 | ||
test22-1.yml | done | .833 | prog | tests | 11 | inspect | .14 | .14 | 21 | 1.5 | .016 | 0 | unknown | prog | tests | 0 | inspect | 83.3 | 91.3 | .16 | .15 | 17 | .25 | 0 | ||
test22-2.yml | timeout (false(unreach-call)) | .917 | prog | tests | 12 | inspect | 900 | 900 | 250 | 9900 | .045 | 0 | true | prog | tests | 1 | inspect | 91.7 | 100 | .18 | .19 | 16 | .26 | 0 | ||
test23-1.yml | false(unreach-call) | .857 | prog | tests | 11 | inspect | .33 | .35 | 23 | 4.1 | .016 | 0 | true | prog | tests | 1 | inspect | 85.7 | 100 | .17 | .18 | 16 | .23 | 0 | ||
test23-2.yml | done | .857 | prog | tests | 10 | inspect | .31 | .33 | 23 | 3.7 | .016 | 0 | unknown | prog | tests | 0 | inspect | 85.7 | 91.7 | .15 | .15 | 17 | .23 | 0 | ||
test24-1.yml | done | .875 | prog | tests | 6 | inspect | .14 | .16 | 21 | 1.3 | .016 | 0 | unknown | prog | tests | 0 | inspect | 87.5 | 86.7 | .14 | .16 | 17 | .16 | 0 | ||
test24-2.yml | false(unreach-call) | .9 | prog | tests | 8 | inspect | .13 | .15 | 24 | 1.8 | .016 | 0 | true | prog | tests | 1 | inspect | 90.0 | 94.4 | .15 | .14 | 17 | .19 | 0 | ||
test25-1.yml | false(unreach-call) | 1.0 | prog | tests | 10 | inspect | .22 | .24 | 23 | 2.7 | .016 | 0 | true | prog | tests | 1 | inspect | 100 | 100 | .16 | .19 | 17 | .23 | 0 | ||
test25-2.yml | done | .917 | prog | tests | 8 | inspect | .20 | .20 | 22 | 2.3 | .016 | 0 | unknown | prog | tests | 0 | inspect | 91.7 | 88.9 | .15 | .17 | 17 | .19 | 0 | ||
test28-1.yml | false(unreach-call) | .875 | prog | tests | 4 | inspect | .13 | .15 | 21 | 1.1 | .016 | 0 | true | prog | tests | 1 | inspect | 87.5 | 100 | .13 | .12 | 16 | .12 | 0 | ||
test28-2.yml | done | .875 | prog | tests | 3 | inspect | .13 | .14 | 21 | .99 | .016 | 0 | unknown | prog | tests | 0 | inspect | 87.5 | 80.0 | .12 | .12 | 16 | .10 | 0 | ||
test29-1.yml | false(unreach-call) | 1.0 | prog | tests | 6 | inspect | .12 | .14 | 21 | 1.0 | .016 | 0 | true | prog | tests | 1 | inspect | 100 | 100 | .13 | .13 | 16 | .16 | 0 | ||
test29-2.yml | done | .875 | prog | tests | 3 | inspect | .14 | .16 | 21 | 1.0 | .016 | 0 | unknown | prog | tests | 0 | inspect | 87.5 | 80.0 | .12 | .15 | 16 | .10 | 0 | ||
sv-benchmarks/c/ldv-regression/ | status | score | program | test-suite | TS size | inspect test-suite | cpu (s) | wall (s) | mem (MB) | energy (J) | blkio-w (MB) | blkio-r (MB) | status | program | test-suite | TS size | inspect test-suite | cov | branch cov (%) | line cov (%) | cpu (s) | wall (s) | mem (MB) | energy | blkio-w (MB) | blkio-r (MB) |
total | 25 | 19.4 | 900 | 900 | 770 | 10000 | .44 | 0 | 25 | 1940 | 2240 | 3.6 | 3.8 | 410 | 5.0 | 0 | ||||||||||
Run set | klee.test-comp19_prop-coverage-branches.ReachSafety-Heap | tbf-testsuite-validator-klee.test-comp19_prop-coverage-branches.ReachSafety-Heap |