Tool BLAST 2.7.1 CBMC 4.5 CPAchecker 1.2.11-svcomp14b ESBMC 1.22.1 FrankenBit LLBMC Predator 2013-10-30 Symbiotic UFO UltimateAutomizer UltimateKojak
Limits timelimit: 900 s, memlimit: 15360 MB, CPU core limit: 8
OS Linux 3.2.0-56-generic x86_64 Linux 3.2.0-57-generic x86_64 Linux 3.2.0-56-generic x86_64
System CPU: Intel Core i7-2600 CPU @ 3.40GHz with 8 cores, frequency: 3401 MHz; RAM: 32827640 kB
Date of execution 13-11-19 16:04 13-11-18 23:43 13-11-18 14:59 13-11-18 23:26 13-12-04 17:02 13-12-04 20:07 13-11-19 22:09 13-11-25 00:14 13-11-18 15:05 13-11-19 23:49 13-11-21 12:52
Options -alias empty
-enable-recursion
-noprofile
-cref
-sv-comp
-lattice
-include-lattice symb
-nosserr
-errorpathfile ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
-propertyfile ${sourcefile_path}/ALL.prp		 --propertyfile ${sourcefile_path}/ALL.prp
--32		 -sv-comp14
-heap 10000M
-spec ${sourcefile_path}/ALL.prp
-disable-java-assertions		 -c ${sourcefile_path}/ALL.prp --spec=${sourcefile_path}/ALL.prp
--cex=${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt		 -spec ${sourcefile_path}/ALL.prp
-witness ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
-simple-mem		 --propertyfile ${sourcefile_path}/ALL.prp
--trace ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
-m32		 --spec=${sourcefile_path}/ALL.prp
--cex=${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt		 ${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt ${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
../../sv-benchmarks/c/ status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB)
ntdrivers/diskperf_false.i.cil.c false(label) 8.7  170   false(label) 0.81 43   false(label) 4.2  230   unknown 1.8  80   false(label) 0.51 25   unknown 0.07 0   unknown 0.86 10.0 unknown 0.58 23   false(label) 0.79 110   unknown 2.9  140   unknown 2.6  130  
ntdrivers/floppy_false.i.cil.c false(label) 6.2  120   false(label) 3.9  95   false(label) 6.2  270   false(label) 370    2000   false(label) 0.50 24   unknown 0.07 0   unknown 0.85 19   unknown 7.9  230   false(label) 0.86 100   unknown 2.5  120   unknown 2.7  130  
ntdrivers/kbfiltr_false.i.cil.c false(label) 75    91   unknown 46    14000   false(label) 3.7  190   true 1.0  51   false(label) 0.62 38   unknown 0.07 0   unknown 0.56 8.0 unknown 0.39 12   false(label) 1.1  130   unknown 2.3  110   unknown 2.4  120  
ntdrivers/parport_false.i.cil.c false(label) 7.7  81   false(label) 14    400   false(label) 4.9  220   unknown 280    1100   false(label) 9.4  660   unknown 0.07 0   unknown 3.7  19   unknown 16    410   false(label) 28    780   unknown 3.0  170   unknown 3.1  170  
ntdrivers/cdaudio_true.i.cil.c true 540    210   true 27    290   true 5.1  200   true 15    340   true 3.4  44   unknown 0.06 0   unknown 0.84 25   true 12    230   true 1.9  130   unknown 2.9  140   unknown 3.0  150  
ntdrivers/diskperf_true.i.cil.c true 180    370   true 9.2  89   true 34    790   unknown 1.9  80   true 0.60 27   unknown 0.07 0   unknown 0.80 10.0 unknown 0.61 23   true 0.88 99   unknown 2.4  120   unknown 2.5  130  
ntdrivers/floppy2_true.i.cil.c true 0.49 37   true 190    1100   true 45    2800   true 390    3400   true 0.67 33   unknown 0.07 0   unknown 3.4  36   unknown 320    5000   true 0.85 40   unknown 4.3  170   unknown 4.6  180  
ntdrivers/floppy_true.i.cil.c exception (gremlins) 80    160   true 60    340   true 63    1900   true 300    2100   true 0.66 28   unknown 0.06 0   unknown 0.82 19   unknown 8.0  230   true 1.00 100   unknown 2.5  120   unknown 2.7  130  
ntdrivers/parport_true.i.cil.c timeout 920    530   true 850    1600   true 64    2800   unknown 280    1100   timeout 920    15000   unknown 0.07 0   unknown 3.6  21   unknown 16    410   true 230    1700   unknown 3.1  170   unknown 3.1  170  
ssh/s3_clnt.blast.01_false.i.cil.c false(label) 33    44   false(label) 40    1000   false(label) 3.1  170   false(label) 900    1400   false(label) 1.1  29   unknown 0.07 0   unknown 0.12 6.0 true 0.30 5.0 false(label) 4.4  180   unknown 2.2  120   unknown 2.4  130  
ssh/s3_clnt.blast.02_false.i.cil.c false(label) 23    41   false(label) 11    350   false(label) 3.1  160   false(label) 900    1500   false(label) 0.85 29   unknown 0.10 0   unknown 0.12 6.0 true 0.32 6.0 false(label) 2.9  160   unknown 2.2  120   unknown 2.4  130  
ssh/s3_clnt.blast.03_false.i.cil.c false(label) 23    41   false(label) 10    350   false(label) 3.1  160   false(label) 900    1500   false(label) 0.83 29   unknown 0.07 0   unknown 0.12 6.0 true 0.33 6.0 false(label) 2.9  150   unknown 2.2  120   unknown 2.4  130  
ssh/s3_clnt.blast.04_false.i.cil.c false(label) 23    41   false(label) 10    350   false(label) 3.1  160   false(label) 900    1700   false(label) 0.89 29   unknown 0.07 0   unknown 0.12 6.0 true 0.33 6.0 false(label) 2.9  160   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.01_false.i.cil.c false(label) 13    37   false(label) 15    320   false(label) 2.7  160   false(label) 900    1800   false(label) 0.67 30   unknown 0.07 0   unknown 0.18 7.0 unknown 0.34 6.0 false(label) 2.3  150   unknown 2.2  120   unknown 2.8  130  
ssh/s3_srvr.blast.02_false.i.cil.c false(label) 8.5  31   false(label) 15    310   false(label) 2.7  160   false(label) 900    1800   false(label) 0.64 30   unknown 0.07 0   unknown 0.18 7.0 unknown 0.34 7.0 false(label) 2.4  150   unknown 2.3  120   unknown 2.4  130  
ssh/s3_srvr.blast.03_false.i.cil.c false(label) 8.4  31   false(label) 15    310   false(label) 2.7  160   false(label) 900    1800   false(label) 0.59 30   unknown 0.07 0   unknown 0.17 8.0 unknown 0.34 7.0 false(label) 2.2  150   unknown 2.2  120   unknown 2.5  130  
ssh/s3_srvr.blast.04_false.i.cil.c false(label) 8.6  31   false(label) 15    310   false(label) 2.7  150   false(label) 900    1900   false(label) 0.68 30   unknown 0.07 0   unknown 0.17 8.0 unknown 0.35 7.0 false(label) 2.4  150   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.06_false.i.cil.c false(label) 610    230   false(label) 15    310   false(label) 2.9  160   unknown 900    1300   false(label) 2.6  33   unknown 0.10 0   unknown 0.19 7.0 unknown 0.36 8.0 false(label) 12    240   unknown 2.3  120   unknown 2.4  130  
ssh/s3_srvr.blast.07_false.i.cil.c false(label) 330    140   false(label) 15    310   false(label) 2.9  160   false(label) 900    1800   false(label) 1.1  31   unknown 0.09 0   unknown 0.19 8.0 unknown 0.34 7.0 false(label) 6.1  210   unknown 2.3  120   unknown 2.4  130  
ssh/s3_srvr.blast.08_false.i.cil.c timeout 920    300   false(label) 80    770   false(label) 3.5  190   false(label) 900    2400   false(label) 6.6  62   unknown 0.07 0   unknown 0.22 7.0 unknown 0.35 7.0 false(label) 9.1  250   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.09_false.i.cil.c false(label) 340    140   false(label) 15    310   false(label) 2.9  160   false(label) 900    1700   false(label) 1.1  31   unknown 0.06 0   unknown 0.16 8.0 unknown 0.34 8.0 false(label) 8.5  220   unknown 2.3  120   unknown 2.5  130  
ssh/s3_srvr.blast.10_false.i.cil.c timeout 920    290   false(label) 81    770   false(label) 3.4  170   true 900    1900   false(label) 6.9  61   unknown 0.07 0   unknown 0.19 6.0 unknown 0.35 7.0 false(label) 9.0  240   unknown 2.3  120   unknown 2.5  130  
ssh/s3_srvr.blast.11_false.i.cil.c false(label) 140    110   false(label) 15    310   false(label) 17    540   unknown 900    1300   false(label) 0.90 31   unknown 0.07 0   unknown 0.19 10.0 unknown 0.37 7.0 false(label) 6.8  200   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.12_false.i.cil.c false(label) 490    160   false(label) 15    310   false(label) 2.9  160   false(label) 900    1600   false(label) 2.4  31   unknown 0.07 0   unknown 0.21 7.0 unknown 0.36 8.0 false(label) 12    240   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.13_false.i.cil.c false(label) 330    140   false(label) 15    310   false(label) 2.9  160   unknown 900    1300   false(label) 1.0  31   unknown 0.07 0   unknown 0.17 8.0 unknown 0.34 8.0 false(label) 6.1  210   unknown 2.2  120   unknown 2.5  130  
ssh/s3_srvr.blast.14_false.i.cil.c false(label) 500    180   false(label) 15    300   false(label) 2.9  160   false(label) 900    1700   false(label) 2.1  32   unknown 0.10 0   unknown 0.19 7.0 unknown 0.35 8.0 false(label) 11    240   unknown 2.3  120   unknown 2.5  130  
ssh/s3_srvr.blast.15_false.i.cil.c timeout 920    300   false(label) 81    770   false(label) 3.5  190   true 900    1900   false(label) 7.7  62   unknown 0.07 0   unknown 0.18 7.0 unknown 0.37 8.0 false(label) 9.4  250   unknown 2.3  120   unknown 2.4  130  
ssh/s3_srvr.blast.16_false.i.cil.c false(label) 560    230   false(label) 15    310   false(label) 2.9  160   false(label) 900    1800   false(label) 2.7  33   unknown 0.07 0   unknown 0.20 7.0 unknown 0.35 8.0 false(label) 15    240   unknown 2.3  120   unknown 2.4  130  
ssh/s3_clnt.blast.01_true.i.cil.c timeout 920    270   true 460    7500   true 3.8  180   true 900    1800   timeout 920    970   unknown 0.07 0   unknown 0.12 6.0 true 0.30 5.0 true 2.7  150   unknown 2.2  120   unknown 2.3  130  
ssh/s3_clnt.blast.02_true.i.cil.c true 590    150   true 460    7600   true 3.7  180   true 300    1700   timeout 920    1100   unknown 0.07 0   unknown 0.12 6.0 true 0.30 6.0 true 2.5  150   unknown 2.2  120   unknown 2.3  130  
ssh/s3_clnt.blast.03_true.i.cil.c timeout 920    270   true 460    7600   true 3.8  180   true 420    1700   timeout 920    1100   unknown 0.09 0   unknown 0.10 6.0 true 0.30 6.0 true 3.2  160   unknown 2.2  120   unknown 2.5  130  
ssh/s3_clnt.blast.04_true.i.cil.c true 580    230   true 460    7600   true 3.7  180   true 430    1700   timeout 920    1800   unknown 0.07 0   unknown 0.12 6.0 true 0.30 6.0 true 3.2  160   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.01_true.i.cil.c timeout 920    220   true 850    1800   true 4.0  180   true 900    2400   true 5.6  36   unknown 0.07 0   unknown 0.19 7.0 unknown 0.34 6.0 true 3.6  160   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.02_true.i.cil.c timeout 920    210   true 850    1800   true 3.9  180   true 900    1800   timeout 920    810   unknown 0.06 0   unknown 0.18 8.0 unknown 0.36 7.0 true 5.9  190   unknown 2.2  120   unknown 2.5  130  
ssh/s3_srvr.blast.06_true.i.cil.c timeout 920    280   true 850    1800   true 13    600   true 900    1800   timeout 920    950   unknown 0.07 0   unknown 0.16 9.0 unknown 0.38 8.0 true 6.3  190   unknown 2.3  120   unknown 2.5  130  
ssh/s3_srvr.blast.07_true.i.cil.c timeout 920    280   true 850    1800   true 10    440   true 900    2300   timeout 920    760   unknown 0.07 0   unknown 0.17 8.0 unknown 0.37 7.0 true 6.1  200   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.08_true.i.cil.c timeout 920    210   true 850    1800   true 4.0  180   true 900    2400   timeout 920    800   unknown 0.06 0   unknown 0.14 8.0 unknown 0.36 8.0 true 6.0  200   unknown 2.2  120   unknown 2.4  130  
ssh/s3_srvr.blast.09_true.i.cil.c timeout 920    210   true 850    1800   true 10    430   true 900    1800   timeout 920    760   unknown 0.07 0   unknown 0.19 8.0 unknown 0.39 7.0 true 6.5  200   unknown 2.2  120   unknown 2.5  130  
ssh/s3_srvr.blast.10_true.i.cil.c timeout 920    220   true 850    1800   true 4.0  180   true 900    2400   true 28    67   unknown 0.07 0   unknown 0.16 8.0 unknown 0.35 7.0 true 6.3  200   unknown 2.3  120   unknown 2.4  130  
ssh/s3_srvr.blast.11_true.i.cil.c timeout 920    240   true 850    1800   true 10    430   true 900    2400   timeout 920    800   unknown 0.07 0   unknown 0.22 10.0 unknown 0.34 7.0 true 5.4  190   unknown 2.2  120   unknown 2.5  130  
ssh/s3_srvr.blast.12_true.i.cil.c timeout 920    280   true 850    1800   true 13    600   true 900    1800   timeout 920    800   unknown 0.08 0   unknown 0.20 8.0 unknown 0.35 8.0 true 4.7  180   unknown 2.3  120   unknown 2.6  130  
ssh/s3_srvr.blast.13_true.i.cil.c timeout 920    210   true 850    1800   true 9.9  410   true 900    2400   timeout 920    800   unknown 0.06 0   unknown 0.17 8.0 unknown 0.31 7.0 true 6.5  200   unknown 2.2  120   unknown 2.6  130  
ssh/s3_srvr.blast.14_true.i.cil.c timeout 920    210   true 850    1800   true 13    600   true 900    1800   timeout 920    800   unknown 0.07 0   unknown 0.16 8.0 unknown 0.35 8.0 true 6.5  200   unknown 2.2  130   unknown 2.6  130  
ssh/s3_srvr.blast.15_true.i.cil.c timeout 920    220   true 850    1800   true 3.9  180   true 900    2200   true 740    650   unknown 0.07 0   unknown 0.16 8.0 unknown 0.35 8.0 true 6.1  200   unknown 2.2  120   unknown 2.6  130  
ssh/s3_srvr.blast.16_true.i.cil.c timeout 920    280   true 850    1800   true 13    600   true 900    1800   timeout 920    800   unknown 0.07 0   unknown 0.19 8.0 unknown 0.34 8.0 true 6.8  200   unknown 2.2  120   unknown 2.6  130  
../../sv-benchmarks/c/ status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB)
total files 45 23000 8200 45 15000 80000 45 430 19000 45 32000 76000 45 15000 31000 45 3.2 0 45 22 430 45 400 6800 45 480 10000 45 110 5600 45 120 6000
correct results 25 5400 3100 44 15000 66000 45 430 19000 35 27000 66000 30 830 2300 0 0 0 0 0 0 5 13 250 45 480 10000 0 0 0 0 0 0
false negatives 0 0 0 0 0 0 0 0 0 3 1800 3800 0 0 0 0 0 0 0 0 0 4 1.3 23 0 0 0 0 0 0 0 0 0
false positives 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (45 files, max score: 67) 30 66 67 31 37 0 0 -22 67 0 0