Tool CBMC 4.5 CPAchecker 1.2.11-svcomp14b CPAlien ESBMC 1.22.1 LLBMC Predator 2013-10-30 Symbiotic 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-18 23:43 13-11-18 14:59 13-11-19 00:04 13-12-05 20:07 13-11-21 13:28 13-11-19 22:09 13-11-24 22:59 13-11-19 23:49 13-11-21 12:52
Options --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
-witness ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
--propertyfile ${sourcefile_path}/ALL.prp
--trace ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
-m32
${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)
memsafety/960521-1_false-valid-deref.i true 1.2  22   false(valid-deref) 3.6  180   false(valid-deref) 160    470   false(valid-deref) 0.41 19   false(valid-deref) 0.62 22   false(valid-deref) 7.2  33   true 0.19 2.0 unknown 2.4  110   unknown 2.3  110  
memsafety/test-0137_false-valid-deref.i false(valid-deref) 0.75 49   false(valid-deref) 2.1  120   false(valid-deref) 1.9  110   false(valid-deref) 900    660   false(valid-deref) 0.12 2.0 false(valid-deref) 0.14 4.0 true 0.21 2.0 unknown 2.4  110   unknown 2.3  110  
memsafety/test-0235_false-valid-deref.i true 1.3  21   false(valid-deref) 3.5  190   false(valid-deref) 30    650   false(valid-deref) 0.40 21   false(valid-deref) 0.15 4.0 false(valid-deref) 0.35 10.0 true 0.22 2.0 unknown 2.3  110   unknown 2.2  110  
memsafety/960521-1_false-valid-free.i true 1.1  22   false(valid-free) 3.6  180   false(valid-free) 160    470   false(valid-deref) 0.41 18   false(valid-free) 0.59 22   false(valid-free) 7.3  33   true 0.20 2.0 unknown 2.3  110   unknown 2.2  110  
memsafety/test-0158_false-valid-free.i false(valid-free) 0.26 20   false(valid-free) 2.0  120   false(valid-free) 1.9  110   unknown 0.33 18   false(valid-free) 0.10 2.0 false(valid-free) 0.12 4.0 true 0.21 2.0 unknown 2.6  110   unknown 2.2  110  
memsafety/test-0232_false-valid-free.i false(valid-free) 0.28 20   false(valid-free) 2.0  120   false(valid-free) 1.8  110   false(valid-deref) 890    400   false(valid-free) 0.30 8.0 false(valid-free) 0.11 4.0 true 0.21 2.0 unknown 2.2  100   unknown 2.2  110  
memsafety/20020406-1_false-valid-memtrack.i false(valid-memtrack) 0.40 26   error (recursion) 2.2  120   unknown 2.1  110   false(valid-deref) 80    1500   false(valid-memtrack) 0.17 3.0 false(valid-memtrack) 0.11 5.0 true 0.21 2.0 unknown 2.6  110   unknown 2.3  110  
memsafety/20051113-1.c_false-valid-memtrack.i true 1.2  20   false(valid-memtrack) 2.0  120   false(valid-memtrack) 2.0  120   false(valid-deref) 0.36 19   false(valid-memtrack) 0.15 2.0 false(valid-memtrack) 0.10 4.0 true 0.22 2.0 unknown 2.2  100   unknown 2.2  110  
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 3.7  100   false(valid-memtrack) 2.5  140   false(valid-memtrack) 2.9  190   false(valid-deref) 30    110   false(valid-memtrack) 8.4  150   false(valid-memtrack) 0.13 5.0 true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 0.27 20   false(valid-memtrack) 2.0  120   false(valid-memtrack) 1.9  110   false(valid-deref) 15    110   false(valid-memtrack) 0.15 3.0 false(valid-memtrack) 0.11 4.0 true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 3.7  100   false(valid-memtrack) 3.2  190   false(valid-memtrack) 4.9  230   false(valid-deref) 25    110   false(valid-memtrack) 49    430   false(valid-memtrack) 0.14 5.0 true 0.18 2.0 unknown 2.7  100   unknown 2.2  110  
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) 0.26 20   false(valid-memtrack) 1.9  120   false(valid-memtrack) 1.9  110   false(valid-memtrack) 0.36 18   false(valid-memtrack) 0.12 2.0 false(valid-memtrack) 0.11 4.0 true 0.22 2.0 unknown 2.3  110   unknown 2.4  110  
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 0.80 56   false(valid-memtrack) 2.1  120   false(valid-memtrack) 2.2  130   unknown 900    2000   false(valid-memtrack) 0.15 2.0 false(valid-memtrack) 0.11 5.0 true 0.22 2.0 unknown 2.7  110   unknown 2.3  110  
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 0.27 19   false(valid-memtrack) 1.9  110   false(valid-memtrack) 1.9  110   false(valid-memtrack) 0.32 17   false(valid-memtrack) 0.11 2.0 false(valid-memtrack) 0.11 3.0 true 0.20 2.0 unknown 2.3  110   unknown 2.2  110  
memsafety/test-0220_false-valid-memtrack.i true 850    4000   false(valid-memtrack) 2.5  150   false(valid-memtrack) 2.1  120   false(valid-deref) 0.36 20   false(valid-memtrack) 0.47 50   false(valid-memtrack) 0.12 4.0 true 0.21 2.0 unknown 2.6  110   unknown 2.2  110  
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 0.28 20   false(valid-memtrack) 1.9  120   false(valid-memtrack) 1.9  110   false(valid-deref) 3.6  99   false(valid-memtrack) 0.10 2.0 false(valid-memtrack) 0.12 4.0 true 0.20 2.0 unknown 2.3  110   unknown 2.3  110  
memsafety/test-0234_false-valid-memtrack.i true 1.3  21   false(valid-memtrack) 2.4  130   false(valid-memtrack) 2.3  120   false(valid-deref) 0.41 21   false(valid-memtrack) 0.12 4.0 false(valid-memtrack) 0.14 5.0 true 0.21 2.0 unknown 2.7  100   unknown 2.3  110  
memsafety/test-0235_false-valid-memtrack.i true 1.3  21   false(valid-memtrack) 2.5  130   false(valid-memtrack) 2.3  130   false(valid-deref) 0.41 21   false(valid-memtrack) 0.14 4.0 false(valid-memtrack) 0.14 5.0 true 0.22 2.0 unknown 2.5  110   unknown 2.2  110  
memsafety/960521-1_true.i true 4.2  890   true 110    300   unknown 900    470   false(valid-deref) 0.38 19   true 0.31 6.0 timeout 900    530   true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety/lockfree-3.0_true.i true 850    1900   true 4.0  210   unknown 900    690   false(valid-deref) 13    120   timeout 920    1200   true 17    37   true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety/test-0019_true.i true 1.1  20   true 1.9  110   true 1.9  110   false(valid-memtrack) 0.33 18   true 0.21 2.0 true 0.13 3.0 true 0.20 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety/test-0102_true.i true 320    13000   true 6.2  310   unknown 900    1200   unknown 900    2600   timeout 920    1100   true 0.16 5.0 true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety/test-0134_true.i false(valid-deref) 0.78 49   true 12    1100   timeout 900    750   false(valid-deref) 900    690   timeout 920    5500   true 0.14 5.0 true 0.21 2.0 unknown 2.8  110   unknown 2.4  110  
memsafety/test-0158_true.i true 1.0  20   true 1.9  110   true 1.8  110   unknown 0.32 17   true 0.21 2.0 true 0.12 3.0 true 0.21 2.0 unknown 2.4  110   unknown 2.9  110  
memsafety/test-0214_true.i unknown 0.26 21   true 4.7  230   false(valid-free) 2.0  110   unknown 95    5000   timeout 910    290   true 0.14 4.0 true 0.22 2.0 unknown 2.6  110   unknown 2.3  110  
memsafety/test-0217_true.i unknown 0.27 21   true 4.7  230   false(valid-free) 2.0  110   unknown 670    15000   timeout 920    1200   true 0.15 5.0 true 0.22 2.0 unknown 2.7  110   unknown 2.3  110  
memsafety/test-0218_true.i unknown 0.27 21   true 5.2  220   false(valid-free) 2.0  110   unknown 140    15000   timeout 920    1100   true 0.15 5.0 true 0.22 2.0 unknown 2.5  110   unknown 2.2  110  
memsafety/test-0219_true.i true 850    5200   true 11    1100   unknown 900    920   false(valid-deref) 0.37 20   timeout 920    15000   true 0.14 4.0 true 0.21 2.0 unknown 2.5  110   unknown 2.2  110  
memsafety/test-0232_true.i true 17    110   timeout 900    1700   unknown 900    470   false(valid-deref) 96    160   timeout 920    7900   true 0.13 3.0 true 0.19 2.0 unknown 2.6  110   unknown 2.3  110  
memsafety/test-0234_true.i true 1.3  21   true 6.1  380   unknown 900    1400   false(valid-deref) 0.41 21   unknown 170    15000   true 0.17 6.0 true 0.22 2.0 unknown 2.7  110   unknown 2.2  110  
memsafety/test-0235_true.i true 1.3  21   true 5.8  280   unknown 900    1400   false(valid-deref) 0.40 21   unknown 240    15000   true 1.2  17   true 0.22 2.0 unknown 2.3  110   unknown 2.2  110  
memsafety/test-0236_true.i true 1.3  21   true 6.1  380   unknown 900    1400   false(valid-deref) 0.40 21   unknown 180    15000   true 0.28 9.0 true 0.22 2.0 unknown 2.5  110   unknown 2.2  110  
memsafety/test-0237_true.i true 1.4  21   true 6.4  390   unknown 900    1400   false(valid-deref) 0.40 21   unknown 180    15000   true 0.27 10.0 true 0.22 2.0 unknown 3.0  110   unknown 2.2  110  
memsafety/test-0504_true.i true 850    6900   true 16    1100   unknown 900    460   unknown 900    420   timeout 920    5300   true 0.22 5.0 true 0.20 2.0 unknown 2.6  100   unknown 2.3  110  
memsafety/test-0513_true.i true 850    4800   true 2.0  120   unknown 900    510   unknown 900    360   timeout 920    3700   true 0.21 6.0 true 0.21 2.0 unknown 2.5  110   unknown 2.4  110  
memsafety/test-0521_true.i false(valid-deref) 91    2500   true 64    1100   timeout 900    510   unknown 900    1700   timeout 920    3500   true 0.32 7.0 true 0.22 2.0 unknown 2.2  110   unknown 2.2  110  
memsafety-ext/dll_extends_pointer_true.i true 41    260   true 77    1700   unknown 1.9  110   false(valid-deref) 210    220   timeout 920    370   timeout 900    120   true 0.21 2.0 unknown 2.1  110   unknown 2.3  110  
memsafety-ext/skiplist_2lvl_true.i true 850    1300   true 2.0  120   timeout 900    910   false(valid-deref) 900    340   timeout 910    920   timeout 900    180   true 0.22 2.0 unknown 2.6  110   unknown 2.3  110  
memsafety-ext/skiplist_3lvl_true.i true 850    2200   true 2.0  120   timeout 900    900   false(valid-deref) 900    300   timeout 920    1900   timeout 900    170   true 0.21 2.0 unknown 2.5  110   unknown 2.2  110  
memsafety-ext/tree_cnstr_true.i true 850    1800   true 2.4  140   unknown 900    590   false(valid-deref) 900    440   timeout 920    1100   false(valid-memtrack) 2.5  17   true 0.20 2.0 unknown 2.5  110   unknown 2.2  110  
memsafety-ext/tree_dsw_true.i true 850    1700   true 2.8  190   unknown 900    610   unknown 900    230   timeout 920    2000   false(valid-memtrack) 4.5  20   true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety-ext/tree_of_cslls_true.i true 850    150   true 4.4  230   unknown 900    560   unknown 900    1000   timeout 920    2300   false(valid-deref) 0.22 7.0 true 0.21 2.0 unknown 2.4  110   unknown 2.2  110  
memsafety-ext/tree_parent_ptr_true.i true 850    2200   true 3.2  190   unknown 900    520   unknown 900    220   timeout 920    1000   false(valid-memtrack) 0.24 8.0 true 0.20 2.0 unknown 3.2  110   unknown 2.3  110  
memsafety-ext/tree_stack_true.i true 850    1500   true 3.1  190   unknown 900    610   false(valid-memtrack) 900    360   timeout 920    1500   false(valid-deref) 0.10 4.0 true 0.21 2.0 unknown 2.6  110   unknown 2.2  110  
list-ext-properties/960521-1_1_false-valid-deref.i true 5.0  350   false(valid-deref) 2.0  120   false(valid-deref) 1.9  110   false(valid-deref) 0.68 26   false(valid-deref) 0.23 2.0 false(valid-deref) 0.10 4.0 true 0.21 2.0 unknown 2.8  110   unknown 2.2  110  
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 0.27 20   false(valid-free) 2.0  120   false(valid-free) 1.9  110   false(valid-deref) 0.73 25   false(valid-free) 0.12 2.0 false(valid-free) 0.14 4.0 true 0.21 2.0 unknown 2.6  110   unknown 2.2  110  
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 0.28 20   false(valid-free) 1.9  110   false(valid-free) 1.9  110   unknown 0.34 17   false(valid-free) 0.14 2.0 false(valid-free) 0.11 4.0 true 0.19 2.0 unknown 2.4  110   unknown 2.6  110  
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) 0.26 20   false(valid-memtrack) 1.9  110   false(valid-memtrack) 1.9  110   false(valid-deref) 0.34 18   false(valid-memtrack) 0.11 2.0 false(valid-memtrack) 0.12 4.0 true 0.20 2.0 unknown 2.5  110   unknown 2.2  110  
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) 0.25 20   false(valid-memtrack) 1.9  110   false(valid-memtrack) 1.9  110   unknown 0.31 17   false(valid-memtrack) 0.11 2.0 false(valid-memtrack) 0.11 3.0 true 0.25 2.0 unknown 2.9  110   unknown 2.3  110  
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) 0.27 20   false(valid-memtrack) 2.0  120   false(valid-memtrack) 1.9  110   false(valid-deref) 260    200   false(valid-memtrack) 0.11 2.0 false(valid-memtrack) 0.11 4.0 true 0.21 2.0 unknown 2.2  110   unknown 2.2  110  
list-ext-properties/960521-1_1_true.i true 38    610   true 3.8  190   true 11    480   false(valid-deref) 0.49 21   true 10    28   unknown 0.10 4.0 true 0.20 2.0 unknown 2.5  110   unknown 2.2  110  
list-ext-properties/list-ext_1_true.i true 87    310   true 3.9  220   unknown 900    550   false(valid-deref) 45    97   timeout 920    1600   false(valid-memtrack) 0.12 4.0 false(label) 0.26 3.0 unknown 2.4  110   unknown 2.2  110  
list-ext-properties/list-ext_flag_1_true.i true 46    190   true 4.0  210   unknown 900    540   false(valid-deref) 9.4  67   timeout 920    1100   false(valid-memtrack) 0.12 4.0 false(label) 0.22 3.0 unknown 2.3  110   unknown 2.2  110  
list-ext-properties/simple-ext_1_true.i true 26    220   true 4.6  230   true 260    470   false(valid-deref) 24    86   timeout 920    1200   false(valid-memtrack) 0.86 6.0 true 0.32 5.0 unknown 2.3  110   unknown 2.2  110  
list-ext-properties/test-0019_1_true.i true 1.1  20   true 1.9  110   true 1.8  110   false(valid-deref) 0.34 17   true 0.28 2.0 true 0.12 3.0 true 0.21 2.0 unknown 2.3  110   unknown 2.2  110  
list-ext-properties/test-0158_1_true.i true 1.1  20   true 1.9  110   true 1.8  110   unknown 0.31 17   true 0.12 2.0 true 0.12 3.0 true 0.19 2.0 unknown 2.7  110   unknown 2.2  110  
list-ext-properties/test-0214_1_true.i unknown 0.27 21   true 4.1  220   false(valid-free) 2.1  110   unknown 1.3  33   timeout 920    1900   false(valid-deref) 0.17 6.0 true 0.22 2.0 unknown 2.8  110   unknown 2.2  110  
list-ext-properties/test-0217_1_true.i unknown 0.27 21   true 4.1  220   false(valid-free) 2.0  110   unknown 1.7  39   timeout 920    700   false(valid-deref) 2.8  12   true 0.22 2.0 unknown 2.9  110   unknown 2.2  110  
list-ext-properties/test-0232_1_true.i true 4.2  44   true 3.2  180   true 17    480   false(valid-deref) 170    200   true 94    340   false(valid-memtrack) 0.13 4.0 true 0.20 2.0 unknown 2.1  110   unknown 2.5  110  
list-ext-properties/test-0504_1_true.i true 340    12000   true 4.0  220   false(valid-memtrack) 3.4  200   true 570    200   timeout 920    1900   timeout 900    180   true 0.21 2.0 unknown 2.8  110   unknown 2.3  110  
list-ext-properties/test-0513_1_true.i true 850    6500   true 2.4  140   false(valid-memtrack) 2.0  120   false(valid-deref) 900    490   timeout 920    4500   false(valid-memtrack) 0.14 4.0 true 0.22 2.0 unknown 2.7  110   unknown 2.2  110  
../../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)
total files 61 12000 72000 61 1400 17000 61 20000 24000 61 17000 52000 61 25000 130000 61 4600 1600 61 13 130 61 150 6400 61 140 6700
correct results 46 11000 65000 59 460 16000 30 690 5800 7 1500 970 31 170 1100 43 39 310 35 7.5 73 0 0 0 0 0 0
false negatives 8 860 4500 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 24 5.0 48 0 0 0 0 0 0
false positives 2 92 2500 0 0 0 7 16 870 36 7200 6400 0 0 0 12 12 96 2 0.48 6.0 0 0 0 0 0 0
score (61 files, max score: 98) 4 95 9 -136 38 14 -130 0 0