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-ControlFlow tbf-testsuite-validator-klee.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow
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/ 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)
ntdrivers-simplified/cdaudio_simpl1.cil-1.yml false(unreach-call) .738 prog tests 196 inspect .35 .37 26 5.2 .082 0   true prog tests 1 inspect
73.8 88.4 1.4  1.5  21 26   0  
ntdrivers-simplified/cdaudio_simpl1.cil-2.yml done .737 prog tests 195 inspect .35 .37 26 5.4 .082 0   unknown prog tests 0 inspect
73.7 88.2 1.3  1.3  21 26   0  
ntdrivers-simplified/diskperf_simpl1.cil.yml timeout .679 prog tests 82 inspect 900    900    520 15000   .066 0   unknown prog tests 0 inspect
67.9 85.5 .59 .69 18 5.8 0  
ntdrivers-simplified/floppy_simpl3.cil-1.yml false(unreach-call) .784 prog tests 98 inspect .30 .32 23 3.6 .053 0   true prog tests 1 inspect
78.4 91.7 .69 .68 18 6.9 0  
ntdrivers-simplified/floppy_simpl3.cil-2.yml done .784 prog tests 99 inspect .30 .32 23 3.5 .053 0   unknown prog tests 0 inspect
78.4 90.3 .66 .67 18 7.0 0  
ntdrivers-simplified/floppy_simpl4.cil-1.yml false(unreach-call) .847 prog tests 161 inspect .47 .49 28 6.4 .070 0   true prog tests 1 inspect
84.7 93.9 1.1  1.0  20 17   0  
ntdrivers-simplified/floppy_simpl4.cil-2.yml done .847 prog tests 159 inspect .44 .46 28 7.1 .070 0   unknown prog tests 0 inspect
84.7 93.6 1.0  1.3  19 16   0  
ntdrivers-simplified/kbfiltr_simpl1.cil.yml done .742 prog tests 47 inspect .15 .15 21 1.9 .033 0   unknown prog tests 0 inspect
74.2 89.2 .35 .37 17 2.2 0  
ntdrivers-simplified/kbfiltr_simpl2.cil-1.yml done .784 prog tests 92 inspect .22 .24 23 2.1 .045 0   unknown prog tests 0 inspect
78.4 90.7 .58 .53 17 6.5 0  
ntdrivers-simplified/kbfiltr_simpl2.cil-2.yml false(unreach-call) .787 prog tests 100 inspect .22 .24 23 2.4 .045 0   true prog tests 1 inspect
78.7 91.2 .64 .70 18 7.1 0  
ssh-simplified/s3_clnt_1.cil-1.yml done .790 prog tests 94 inspect 1.7  1.7  31 21   .029 0   unknown prog tests 0 inspect
79.0 88.6 .63 .69 17 6.2 0  
ssh-simplified/s3_clnt_1.cil-2.yml false(unreach-call) .790 prog tests 95 inspect .92 .94 25 12   .029 0   true prog tests 1 inspect
79.0 88.9 .69 .81 17 6.3 0  
ssh-simplified/s3_clnt_2.cil-1.yml false(unreach-call) .778 prog tests 91 inspect .93 .95 26 11   .029 0   true prog tests 1 inspect
77.8 89.5 .66 .62 17 6.0 0  
ssh-simplified/s3_clnt_2.cil-2.yml done .772 prog tests 88 inspect 1.6  1.7  31 21   .029 0   unknown prog tests 0 inspect
77.2 89.0 .61 .74 17 5.8 0  
ssh-simplified/s3_clnt_3.cil-1.yml done .356 prog tests 32 inspect .14 .16 21 1.5 .029 0   unknown prog tests 0 inspect
35.6 46.0 .33 .31 17 2.1 0  
ssh-simplified/s3_clnt_3.cil-2.yml false(unreach-call) .840 prog tests 107 inspect 3.4  3.4  42 49   .029 0   true prog tests 1 inspect
84.0 93.3 .80 .85 17 7.1 0  
ssh-simplified/s3_clnt_3.cil-3.yml done .772 prog tests 90 inspect 1.7  1.7  31 23   .029 0   unknown prog tests 0 inspect
77.2 88.4 .62 .57 17 6.0 0  
ssh-simplified/s3_clnt_4.cil-1.yml done .772 prog tests 88 inspect 1.7  1.7  31 28   .029 0   unknown prog tests 0 inspect
77.2 89.0 .62 .57 17 5.8 0  
ssh-simplified/s3_clnt_4.cil-2.yml false(unreach-call) .840 prog tests 104 inspect 3.3  3.3  40 41   .029 0   true prog tests 1 inspect
84.0 93.1 .75 .83 17 6.9 0  
sv-benchmarks/c/ 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 19 14.4  920   920 1000 15000 .86 0   19 1440 1670 14 15 340 170 0  
Run set klee.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow tbf-testsuite-validator-klee.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow