Tool Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Forester Map2Check PredatorHP Seahorn Ultimate Automizer r12950 Ultimate Kojak r12950
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host cayman[1-8]
OS Linux 3.13.0
System CPU: Intel Core i7-4770 @ 3.40 GHz with 8 cores, frequency: 3.4 GHz; RAM: 33 GB
Date of execution 14-12-18 12:10 14-12-18 12:14 14-12-18 11:26 14-12-18 12:14 14-12-19 14:06 14-12-18 11:27 14-12-19 14:06 14-12-20 18:50 14-12-18 11:19
Options -trace --32 -sv-comp15 -disable-java-assertions -heap 10000m --trace witness.graphml witness.graphml --witness ./witness.graphml --cex=witness.graphml 32bit precise 32bit precise
../../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)
memsafety/960521-1_false-valid-deref.i true 140    6300 true 1.2  32 false(valid-deref) 2.7  220 true 0.078 17 unknown 0.077 9.0 false(valid-deref) 5.5  54 false(valid-deref) 98    2800 unknown 0.051 5.0 timeout 920    570 timeout 920    860
memsafety/test-0137_false-valid-deref.i unknown 850    300 unknown 0.74 63 false(valid-deref) 1.8  160 timeout 920    1900 unknown 0.14 10.0 false(valid-deref) 5.9  55 false(valid-deref) 1.0  22 unknown 0.040 5.0 unknown 490    1100 timeout 920    950
memsafety/test-0235_false-valid-deref.i unknown 850    520 true 850    1000 false(valid-deref) 7.1  480 true 0.092 20 unknown 0.048 8.0 false(valid-deref) 6.3  57 timeout 920    390 unknown 0.039 5.0 unknown 5.6  250 unknown 5.8  250
memsafety/960521-1_false-valid-free.i true 140    6300 true 1.3  32 false(valid-free) 2.7  220 true 0.11 17 unknown 0.074 8.0 false(valid-free) 5.5  54 false(valid-free) 99    3000 unknown 0.046 5.0 timeout 920    560 timeout 920    880
memsafety/test-0158_false-valid-free.i false(valid-free) 1.4  100 false(valid-free) 0.23 28 false(valid-free) 1.8  160 unknown 0.098 18 unknown 0.043 8.0 false(valid-deref) 5.8  55 false(valid-free) 1.0  20 unknown 0.038 5.0 false(valid-free) 7.8  280 false(valid-free) 9.4  300
memsafety/test-0232_false-valid-free.i true 850    350 false(valid-free) 0.23 27 false(valid-free) 1.8  160 unknown 0.11 20 unknown 0.057 8.0 false(valid-free) 19    54 false(valid-free) 1.0  19 unknown 0.035 5.0 unknown 490    2900 timeout 920    960
memsafety/20020406-1_false-valid-memtrack.i unknown 190    3200 false(valid-memtrack) 0.41 37 error (recursion) 1.9  160 false(reach) 230    3000 unknown 0.042 8.0 true 6.5  54 false(valid-memtrack) 1.1  22 unknown 0.048 5.0 false(valid-deref) 9.1  280 false(valid-deref) 8.9  280
memsafety/20051113-1.c_false-valid-memtrack.i out of memory 47    15000 true 1.5  35 false(valid-memtrack) 1.8  160 true 0.077 18 unknown 0.033 8.0 false(valid-deref) 5.6  54 false(valid-memtrack) 1.0  20 unknown 0.034 5.0 false(valid-memtrack) 79    710 false(valid-memtrack) 220    1200
memsafety/lockfree-3.1_false-valid-memtrack.i out of memory 620    15000 false(valid-memtrack) 3.6  130 false(valid-memtrack) 3.4  210 false(reach) 240    230 unknown 0.082 8.0 out of memory 720    15000 false(valid-memtrack) 1.4  22 unknown 0.035 5.0 unknown 170    440 timeout 920    1300
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 1.6  110 unknown 0.24 27 false(valid-memtrack) 1.8  160 false(reach) 260    270 unknown 0.090 8.0 false(valid-memtrack) 260    57 false(valid-memtrack) 1.1  20 unknown 0.033 5.0 false(valid-memtrack) 130    700 timeout 920    1600
memsafety/lockfree-3.3_false-valid-memtrack.i true 850    430 false(valid-memtrack) 3.8  130 false(valid-memtrack) 10    790 false(reach) 390    240 unknown 0.070 8.0 out of memory 540    15000 false(valid-memtrack) 1.0  21 unknown 0.046 5.0 timeout 920    590 timeout 920    1600
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) 1.3  100 false(valid-memtrack) 0.21 27 false(valid-memtrack) 1.7  160 false(reach) 1.4  18 unknown 0.034 8.0 false(valid-memtrack) 5.6  56 false(valid-memtrack) 1.0  29 unknown 0.038 5.0 false(valid-memtrack) 9.8  290 false(valid-memtrack) 12    400
memsafety/test-0102_false-valid-memtrack.i unknown 850    340 false(valid-memtrack) 0.74 66 false(valid-memtrack) 2.1  170 out of memory 130    15000 timeout 920    38 false(valid-memtrack) 5.7  55 false(valid-memtrack) 9.8  130 unknown 0.044 5.0 timeout 920    640 timeout 920    480
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 1.2  100 false(valid-memtrack) 0.23 27 false(valid-memtrack) 1.7  160 unknown 0.070 17 unknown 0.027 8.0 false(valid-memtrack) 5.4  54 false(valid-memtrack) 1.0  19 unknown 0.042 5.0 false(valid-memtrack) 6.3  260 false(valid-memtrack) 7.7  280
memsafety/test-0220_false-valid-memtrack.i true 850    420 true 850    6200 false(valid-memtrack) 2.0  170 true 0.077 19 unknown 0.055 8.0 false(valid-deref) 6.1  55 false(valid-memtrack) 1.1  20 unknown 0.029 5.0 unknown 5.4  250 unknown 5.5  250
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 1.2  110 false(valid-memtrack) 0.23 27 false(valid-memtrack) 1.8  160 false(reach) 94    170 unknown 0.067 8.0 false(valid-memtrack) 11    54 false(valid-memtrack) 1.0  20 unknown 0.036 5.0 false(valid-memtrack) 120    670 false(valid-memtrack) 850    950
memsafety/test-0234_false-valid-memtrack.i unknown 850    520 true 850    1000 false(valid-memtrack) 2.2  180 true 0.11 20 unknown 0.054 8.0 false(valid-deref) 15    56 false(valid-memtrack) 4.9  70 unknown 0.041 5.0 unknown 5.7  240 unknown 5.9  250
memsafety/test-0235_false-valid-memtrack.i unknown 850    510 true 850    1000 false(valid-memtrack) 2.4  180 true 0.11 20 unknown 0.061 8.0 false(valid-deref) 8.3  57 false(valid-memtrack) 4.9  69 unknown 0.046 5.0 unknown 5.6  250 unknown 5.8  240
memsafety/960521-1_true-valid-memsafety.i true 140    6300 true 5.4  1600 true 2.2  180 true 0.085 17 unknown 0.081 9.0 false(valid-deref) 36    54 timeout 920    10000 unknown 0.047 5.0 timeout 920    580 timeout 920    890
memsafety/lockfree-3.0_true-valid-memsafety.i true 850    650 true 850    2300 true 10    820 true 490    280 unknown 0.076 8.0 out of memory 350    15000 true 21    61 unknown 0.020 5.0 unknown 77    430 timeout 920    1300
memsafety/test-0019_true-valid-memsafety.i true 1.8  120 true 1.1  27 true 1.7  150 true 0.10 17 unknown 0.054 8.0 true 6.8  54 true 1.0  19 unknown 0.036 5.0 unknown 510    2500 true 420    990
memsafety/test-0102_true-valid-memsafety.i unknown 850    350 true 200    13000 true 17    930 out of memory 89    15000 timeout 920    46 true 20    55 true 2.8  90 unknown 0.044 5.0 timeout 920    540 timeout 920    530
memsafety/test-0134_true-valid-memsafety.i unknown 850    300 false(valid-deref) 0.74 63 true 11    950 timeout 920    1900 unknown 0.18 11 false(valid-deref) 5.9  55 true 3.4  96 unknown 0.041 5.0 timeout 920    1100 timeout 920    680
memsafety/test-0158_true-valid-memsafety.i true 0.90 83 true 1.1  27 true 1.7  150 unknown 0.098 17 unknown 0.044 8.0 true 6.8  54 true 1.0  18 unknown 0.035 5.0 true 340    400 true 9.1  290
memsafety/test-0214_true-valid-memsafety.i true 850    340 true 65    13000 true 11    880 unknown 52    9800 unknown 0.058 8.0 true 37    56 true 1.8  26 unknown 0.038 5.0 unknown 5.0  240 unknown 5.3  240
memsafety/test-0217_true-valid-memsafety.i true 850    600 false(valid-deref) 24    900 true 11    860 out of memory 330    15000 unknown 0.036 8.0 false(valid-deref) 6.2  56 true 1.3  23 unknown 0.029 5.0 unknown 5.3  240 unknown 5.1  240
memsafety/test-0218_true-valid-memsafety.i true 850    610 false(valid-deref) 0.69 52 true 12    850 out of memory 36    15000 unknown 0.058 8.0 false(valid-deref) 6.3  56 true 1.3  23 unknown 0.032 5.0 unknown 5.2  240 unknown 5.2  240
memsafety/test-0219_true-valid-memsafety.i true 850    390 true 850    7200 true 17    1100 true 0.088 19 unknown 0.030 8.0 false(valid-deref) 7.8  55 true 3.2  93 unknown 0.043 5.0 unknown 5.4  240 unknown 5.6  240
memsafety/test-0232_true-valid-memsafety.i true 850    350 true 14    160 true 23    1100 unknown 0.12 17 unknown 0.089 9.0 true 58    54 true 1.0  20 unknown 0.043 5.0 unknown 180    430 timeout 920    970
memsafety/test-0234_true-valid-memsafety.i unknown 850    520 true 850    1000 true 21    1200 true 0.10 20 unknown 0.041 8.0 false(valid-deref) 7.0  56 true 2.1  68 unknown 0.035 5.0 unknown 5.6  240 unknown 5.6  250
memsafety/test-0235_true-valid-memsafety.i unknown 850    520 true 850    1000 true 20    1000 true 0.094 20 unknown 0.046 8.0 false(valid-deref) 8.7  57 true 5.1  89 unknown 0.029 5.0 unknown 5.7  240 unknown 5.4  240
memsafety/test-0236_true-valid-memsafety.i unknown 850    530 true 850    1000 true 21    1300 true 0.11 20 unknown 0.054 8.0 true 24    57 true 2.1  60 unknown 0.034 5.0 unknown 5.7  240 unknown 5.6  250
memsafety/test-0237_true-valid-memsafety.i unknown 850    640 true 850    1000 true 21    1300 true 0.11 20 unknown 0.049 8.0 true 7.8  57 true 2.2  61 unknown 0.033 5.0 unknown 5.5  250 unknown 5.5  240
memsafety/test-0504_true-valid-memsafety.i true 850    390 true 530    12000 true 13    1200 timeout 920    9900 true 1.7  17 true 230    54 true 3.8  39 unknown 0.040 5.0 unknown 540    590 unknown 22    1100
memsafety/test-0513_true-valid-memsafety.i true 850    750 true 850    5700 true 34    2000 timeout 920    980 true 0.18 10.0 true 7.1  54 true 2.4  28 unknown 0.040 5.0 timeout 920    620 timeout 920    750
memsafety/test-0521_true-valid-memsafety.i true 850    410 false(valid-deref) 120    3500 true 15    1600 timeout 920    4200 true 0.85 29 true 12    55 true 2.4  31 unknown 0.044 5.0 timeout 920    780 timeout 920    1600
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i true 850    770 true 37    280 true 34    3100 unknown 0.15 23 true 0.19 10.0 false(valid-deref) 9.9  54 timeout 920    670 unknown 0.044 5.0 timeout 920    590 timeout 920    680
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i true 850    4700 true 850    2300 true 31    2300 timeout 920    3300 true 0.38 12 timeout 900    66 timeout 920    510 unknown 0.035 5.0 unknown 77    690 timeout 920    670
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i true 850    650 true 850    2300 true 34    2500 timeout 920    4000 true 20    65 timeout 900    54 timeout 920    930 unknown 0.035 5.0 timeout 920    1600 timeout 920    720
memsafety-ext/tree_cnstr_true-valid-memsafety.i true 850    410 true 850    2300 true 18    1600 timeout 920    8900 true 0.13 10.0 timeout 900    96 timeout 920    290 unknown 0.036 5.0 timeout 920    700 unknown 9.0  280
memsafety-ext/tree_dsw_true-valid-memsafety.i true 850    1000 true 850    2000 true 20    2000 timeout 920    5900 true 0.54 13 timeout 900    55 timeout 920    120 unknown 0.034 5.0 timeout 920    2100 timeout 920    760
memsafety-ext/tree_of_cslls_true-valid-memsafety.i true 850    330 true 850    190 true 20    1500 timeout 920    6700 true 0.26 10.0 true 370    55 timeout 920    310 unknown 0.021 5.0 timeout 920    730 unknown 9.6  300
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i true 850    350 true 850    2400 true 21    2100 timeout 920    2900 true 0.32 11 true 7.1  54 timeout 920    210 unknown 0.037 5.0 timeout 920    760 unknown 7.6  270
memsafety-ext/tree_stack_true-valid-memsafety.i true 850    380 true 850    1900 true 20    2400 timeout 920    2900 true 0.096 10.0 timeout 900    54 timeout 920    220 unknown 0.043 5.0 timeout 920    680 unknown 7.7  270
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 1.5  110 false(valid-deref) 0.23 28 false(valid-deref) 1.7  160 false(reach) 1.8  20 unknown 0.058 8.0 false(valid-deref) 5.6  54 false(valid-deref) 1.0  19 unknown 0.039 5.0 timeout 920    640 timeout 920    900
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 1.5  110 false(valid-free) 0.27 28 false(valid-free) 1.8  150 true 0.14 18 unknown 0.083 8.0 false(valid-free) 5.6  54 false(valid-free) 1.0  20 unknown 0.021 5.0 false(valid-free) 120    300 false(valid-free) 24    420
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 1.3  110 false(valid-free) 0.22 27 false(valid-free) 1.7  150 unknown 0.10 17 unknown 0.035 8.0 false(valid-deref) 5.5  54 false(valid-free) 1.0  20 unknown 0.030 5.0 false(valid-free) 6.1  250 false(valid-free) 5.9  250
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) 1.4  110 false(valid-memtrack) 0.19 27 false(valid-memtrack) 1.7  150 false(reach) 1.6  18 unknown 0.047 8.0 false(valid-memtrack) 5.6  56 false(valid-memtrack) 1.0  19 unknown 0.033 5.0 false(valid-memtrack) 92    660 false(valid-memtrack) 570    540
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) 1.3  100 unknown 0.19 27 false(valid-memtrack) 1.7  150 unknown 0.099 17 unknown 0.032 8.0 false(valid-memtrack) 5.4  54 false(valid-memtrack) 1.0  20 unknown 0.046 5.0 false(valid-memtrack) 5.8  250 false(valid-memtrack) 5.6  250
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) 1.7  140 false(valid-memtrack) 0.24 27 false(valid-memtrack) 1.7  160 unknown 0.098 17 unknown 0.033 8.0 false(valid-memtrack) 5.6  54 false(valid-memtrack) 1.0  19 unknown 0.038 5.0 false(valid-memtrack) 100    430 timeout 920    960
list-ext-properties/960521-1_1_true-valid-memsafety.i false(valid-memtrack) 1.6  120 true 49    1300 true 3.7  210 true 0.16 18 unknown 0.080 8.0 true 7.0  54 unknown 2.1  19 unknown 0.037 5.0 unknown 840    710 timeout 920    870
list-ext-properties/list-ext_1_true-valid-memsafety.i true 850    310 true 66    370 true 6.6  450 false(reach) 170    100 unknown 0.048 8.0 true 7.0  54 true 14    57 unknown 0.043 5.0 timeout 920    650 timeout 920    1100
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 850    740 true 36    230 true 15    1400 false(reach) 76    69 unknown 0.038 8.0 true 7.0  54 false(valid-memtrack) 8.0  59 unknown 0.026 5.0 timeout 920    560 timeout 920    750
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 850    600 true 21    250 true 4.4  270 false(reach) 72    61 unknown 0.049 8.0 true 6.9  54 timeout 920    4500 unknown 0.044 5.0 timeout 920    1400 timeout 920    800
list-ext-properties/test-0019_1_true-valid-memsafety.i true 3.9  170 true 1.1  27 true 1.7  150 true 0.11 17 unknown 0.047 8.0 true 6.9  54 true 1.0  19 unknown 0.038 5.0 unknown 760    3000 true 640    1100
list-ext-properties/test-0158_1_true-valid-memsafety.i true 2.0  100 true 1.1  27 true 1.7  150 unknown 0.080 17 unknown 0.050 8.0 true 6.9  54 true 1.0  18 unknown 0.035 5.0 false(valid-free) 5.5  240 false(valid-memtrack) 6.0  250
list-ext-properties/test-0214_1_true-valid-memsafety.i true 850    330 true 760    12000 true 14    1000 unknown 0.45 57 unknown 0.046 8.0 true 7.1  56 true 18    490 unknown 0.042 5.0 unknown 5.2  240 unknown 5.2  240
list-ext-properties/test-0217_1_true-valid-memsafety.i true 850    380 true 270    12000 true 18    1500 unknown 780    2900 unknown 0.035 8.0 false(valid-deref) 6.2  56 true 24    290 unknown 0.030 5.0 unknown 5.3  240 unknown 5.2  240
list-ext-properties/test-0232_1_true-valid-memsafety.i true 850    330 true 5.1  66 true 3.0  210 unknown 0.12 17 unknown 0.045 8.0 false(valid-deref) 5.6  54 true 3.1  20 unknown 0.036 5.0 unknown 140    370 unknown 540    650
list-ext-properties/test-0504_1_true-valid-memsafety.i true 850    370 true 180    12000 true 15    1100 timeout 920    2100 unknown 0.066 8.0 true 7.0  54 timeout 920    4800 unknown 0.021 5.0 unknown 5.6  240 unknown 5.6  250
list-ext-properties/test-0513_1_true-valid-memsafety.i true 850    820 true 300    13000 true 2.3  170 timeout 920    1200 unknown 0.078 9.0 true 7.1  55 true 1.0  22 unknown 0.047 5.0 timeout 920    570 timeout 920    770
memory-alloca/add_last_unsafe_false-valid-deref.i false(valid-deref) 1.2  100 false(valid-deref) 0.13 26 false(valid-deref) 1.7  160 false(reach) 1.3  17 unknown 0.032 8.0 true 6.8  54 unknown 2.1  19 unknown 0.034 5.0 false(valid-deref) 6.1  250 false(valid-deref) 5.8  240
memory-alloca/bubble_sort_unsafe_false-valid-deref.i false(valid-deref) 1.0  94 false(valid-deref) 0.38 41 false(valid-deref) 1.4  140 false(reach) 0.80 54 unknown 0.044 7.0 false(valid-deref) 3.7  54 false(valid-deref) 1.0  18 unknown 0.029 5.0 false(valid-deref) 5.4  250 false(valid-deref) 5.6  250
memory-alloca/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 0.98 93 false(valid-deref) 0.37 39 false(valid-deref) 1.4  150 false(reach) 0.79 53 unknown 0.065 8.0 false(valid-deref) 3.7  54 false(valid-deref) 1.0  18 unknown 0.031 5.0 false(valid-deref) 5.6  240 false(valid-deref) 5.5  250
memory-alloca/count_down_unsafe_false-valid-deref.i false(valid-deref) 1.4  110 unknown 0.12 28 false(valid-deref) 1.8  160 false(reach) 1.6  24 unknown 0.038 8.0 true 6.9  54 unknown 2.1  17 unknown 0.044 5.0 false(valid-deref) 6.1  250 false(valid-deref) 6.2  250
memory-alloca/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 0.92 92 unknown 0.11 24 false(valid-deref) 1.4  140 false(reach) 0.095 11 unknown 0.033 7.0 true 6.7  54 false(valid-deref) 1.1  17 unknown 0.046 5.0 false(valid-deref) 5.5  250 false(valid-deref) 5.4  250
memory-alloca/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1.4  110 false(valid-deref) 0.15 26 false(valid-deref) 1.8  160 false(reach) 0.77 17 unknown 0.068 8.0 true 7.0  54 false(valid-deref) 1.0  19 unknown 0.021 5.0 unknown 5.2  240 unknown 4.9  240
memory-alloca/cstrcpy_unsafe_false-valid-deref.i false(valid-deref) 0.92 92 unknown 0.10 24 false(valid-deref) 1.4  140 false(reach) 0.094 11 unknown 0.056 7.0 true 6.7  54 false(valid-deref) 1.0  17 unknown 0.037 5.0 false(valid-deref) 5.6  240 false(valid-deref) 5.7  250
memory-alloca/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1.4  110 unknown 0.19 27 false(valid-deref) 1.7  150 false(reach) 1.3  17 unknown 0.043 8.0 true 7.0  54 false(valid-deref) 1.1  19 unknown 0.020 5.0 false(valid-deref) 7.0  270 false(valid-deref) 6.9  270
memory-alloca/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 0.91 92 false(valid-deref) 0.13 24 false(valid-deref) 1.4  150 false(reach) 0.13 12 unknown 0.026 7.0 true 6.7  54 false(valid-deref) 1.0  18 unknown 0.050 5.0 false(valid-deref) 5.7  250 false(valid-deref) 5.4  240
memory-alloca/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 0.87 96 false(valid-deref) 0.13 26 false(valid-deref) 1.5  150 false(reach) 0.31 22 unknown 0.061 7.0 true 6.7  54 false(valid-deref) 1.1  18 unknown 0.047 5.0 false(valid-deref) 6.0  250 false(valid-deref) 6.7  250
memory-alloca/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1.6  120 false(valid-deref) 0.15 27 false(valid-deref) 1.8  160 false(reach) 1.8  33 unknown 0.077 8.0 false(valid-deref) 5.4  54 false(valid-deref) 1.0  19 unknown 0.021 5.0 unknown 4.9  240 unknown 5.2  240
memory-alloca/diff_usafe_false-valid-deref.i false(valid-deref) 1.0  94 false(valid-deref) 0.13 24 false(valid-deref) 1.5  140 false(reach) 1.1  61 unknown 0.039 7.0 false(valid-deref) 3.8  54 false(valid-deref) 1.0  17 unknown 0.036 5.0 false(valid-deref) 5.6  250 false(valid-deref) 6.1  250
memory-alloca/insertion_sort_unsafe_false-valid-deref.i false(valid-deref) 0.98 90 unknown 0.14 26 false(valid-deref) 1.4  150 false(reach) 0.54 26 unknown 0.042 7.0 false(valid-deref) 6.8  54 false(valid-deref) 1.0  18 unknown 0.040 5.0 false(valid-deref) 5.8  250 false(valid-deref) 5.9  250
memory-alloca/insertionsort_unsafe_false-valid-deref.i false(valid-deref) 0.96 94 unknown 0.12 24 false(valid-deref) 1.4  140 false(reach) 0.52 23 unknown 0.044 7.0 false(valid-deref) 3.7  54 false(valid-deref) 1.0  18 unknown 0.038 5.0 false(valid-deref) 5.4  250 false(valid-deref) 5.8  250
memory-alloca/java_BubbleSort_unsafe_false-valid-deref.i false(valid-deref) 0.97 95 false(valid-deref) 0.34 37 false(valid-deref) 1.4  140 false(reach) 0.89 62 unknown 0.059 7.0 false(valid-deref) 6.8  54 false(valid-deref) 1.0  19 unknown 0.042 5.0 false(valid-deref) 5.8  250 false(valid-deref) 5.4  250
memory-alloca/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1.5  110 unknown 0.30 43 false(valid-deref) 1.8  150 false(reach) 5.2  200 unknown 0.055 8.0 true 6.9  54 unknown 2.1  19 unknown 0.026 5.0 false(valid-deref) 6.0  250 false(valid-deref) 6.3  240
memory-alloca/knapsack_unsafe_false-valid-deref.i false(valid-deref) 0.98 94 false(valid-deref) 0.15 26 false(valid-deref) 1.4  150 false(reach) 2.0  190 unknown 0.043 7.0 false(valid-deref) 3.8  54 false(valid-deref) 1.0  22 unknown 0.031 5.0 false(valid-deref) 5.8  250 false(valid-deref) 5.6  250
memory-alloca/lis_unsafe_false-valid-deref.i false(valid-deref) 1.4  110 false(valid-deref) 0.26 30 false(valid-deref) 1.8  160 timeout 920    170 unknown 0.089 9.0 true 7.0  54 unknown 2.1  20 unknown 0.033 5.0 false(valid-deref) 330    430 timeout 920    730
memory-alloca/mult_array_unsafe_false-valid-deref.i false(valid-deref) 2.0  170 false(valid-deref) 0.15 30 false(valid-deref) 1.8  160 false(reach) 1.4  21 unknown 0.046 8.0 false(valid-deref) 5.3  54 unknown 2.0  20 unknown 0.047 5.0 unknown 5.2  240 unknown 5.5  240
memory-alloca/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1.4  120 false(valid-deref) 0.23 34 false(valid-deref) 1.8  160 false(reach) 1.3  18 unknown 0.043 8.0 true 6.8  54 unknown 2.1  19 unknown 0.046 5.0 false(valid-deref) 6.5  250 false(valid-deref) 8.3  270
memory-alloca/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1.4  120 false(valid-deref) 0.22 35 false(valid-deref) 1.8  160 false(reach) 1.2  18 unknown 0.045 8.0 true 6.9  54 unknown 2.0  20 unknown 0.036 5.0 false(valid-deref) 5.9  250 false(valid-deref) 6.2  250
memory-alloca/selection_sort_unsafe_false-valid-deref.i false(valid-deref) 0.98 94 false(valid-deref) 0.13 24 false(valid-deref) 1.4  140 false(reach) 0.73 58 unknown 0.090 8.0 false(valid-deref) 6.8  54 false(valid-deref) 1.0  18 unknown 0.033 5.0 false(valid-deref) 5.8  250 false(valid-deref) 6.0  250
memory-alloca/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 0.98 94 unknown 0.12 24 false(valid-deref) 1.4  140 false(reach) 0.71 59 unknown 0.079 8.0 false(valid-deref) 3.8  54 false(valid-deref) 1.0  18 unknown 0.043 5.0 false(valid-deref) 5.7  250 false(valid-deref) 6.0  250
memory-alloca/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 0.96 94 unknown 0.13 23 false(valid-deref) 1.4  140 false(reach) 0.097 11 unknown 0.041 7.0 true 6.7  54 false(valid-deref) 1.0  18 unknown 0.034 5.0 false(valid-deref) 6.4  240 false(valid-deref) 5.8  250
memory-alloca/stroeder2_unsafe_false-valid-deref.i false(valid-deref) 0.99 94 unknown 0.10 26 false(valid-deref) 1.5  150 false(reach) 0.26 21 unknown 0.051 8.0 true 6.7  54 false(valid-deref) 1.0  17 unknown 0.034 5.0 false(valid-deref) 5.2  250 false(valid-deref) 5.8  250
memory-alloca/Avery-2006FLOPS-Tabel1_true-alloca_true-valid-memsafety.i out of memory 350    15000 unknown 0.13 28 true 78    4200 false(reach) 1.4  18 unknown 0.038 8.0 true 6.8  54 timeout 920    2300 unknown 0.034 5.0 unknown 730    2500 timeout 920    2500
memory-alloca/Ben-Amram-2010LMCS-Ex2.3-alloca_true-valid-memsafety.i true 860    5600 false(valid-deref) 0.14 26 true 360    3500 false(reach) 1.4  18 unknown 0.056 8.0 true 6.8  54 true 1.1  19 unknown 0.038 5.0 unknown 790    2300 true 18    670
memory-alloca/BrockschmidtCookFuhs-2013CAV-Fig1-alloca_true-valid-memsafety.i out of memory 50    15000 false(valid-deref) 0.14 26 true 67    3600 false(reach) 1.7  28 unknown 0.052 8.0 out of memory 8.8  15000 true 2.2  26 unknown 0.034 5.0 true 670    2400 timeout 920    850
memory-alloca/BrockschmidtCookFuhs-2013CAV-Introduction-alloca_true-valid-memsafety.i true 150    1800 false(valid-deref) 0.12 26 true 3.0  210 false(reach) 1.1  17 unknown 0.042 8.0 true 6.9  54 true 1.0  19 unknown 0.037 5.0 true 220    420 timeout 920    1100
memory-alloca/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca_true-valid-memsafety.i true 410    2200 false(valid-deref) 0.12 26 true 2.9  210 false(reach) 1.3  17 unknown 0.076 9.0 true 6.8  54 true 1.1  18 unknown 0.041 5.0 unknown 650    2300 timeout 920    1100
memory-alloca/CookSeeZuleger-2013TACAS-Fig3-alloca_true-valid-memsafety.i true 870    9900 false(valid-deref) 0.14 26 true 120    3600 false(reach) 1.3  17 unknown 0.039 8.0 true 6.9  54 true 1.0  19 unknown 0.034 5.0 true 180    380 true 10    400
memory-alloca/CookSeeZuleger-2013TACAS-Fig7a-alloca_true-valid-memsafety.i true 870    8400 false(valid-deref) 0.14 26 true 220    3900 false(reach) 1.3  18 unknown 0.030 8.0 true 6.9  54 true 1.0  19 unknown 0.034 5.0 true 750    2200 true 20    680
memory-alloca/CookSeeZuleger-2013TACAS-Fig7b-alloca_true-valid-memsafety.i true 870    7500 false(valid-deref) 0.14 26 true 130    3600 false(reach) 1.2  18 unknown 0.057 8.0 true 6.8  54 true 1.0  19 unknown 0.021 5.0 true 780    2300 true 39    700
memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-valid-memsafety.i out of memory 590    15000 false(valid-deref) 0.11 28 true 110    3600 false(reach) 1.3  18 unknown 0.053 8.0 true 6.8  54 true 1.1  19 unknown 0.042 5.0 timeout 920    1400 timeout 920    920
memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig1-alloca_true-valid-memsafety.i true 660    5700 false(valid-deref) 0.16 27 true 1.8  160 false(reach) 1.6  20 unknown 0.033 8.0 true 6.8  54 true 1.0  19 unknown 0.036 5.0 timeout 920    580 timeout 920    2000
memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-valid-memsafety.i out of memory 27    15000 false(valid-deref) 0.13 26 true 45    3600 false(reach) 0.92 17 unknown 0.083 8.0 true 6.8  54 true 1.0  19 unknown 0.021 5.0 true 120    340 true 8.8  270
memory-alloca/KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1-alloca_true-valid-memsafety.i out of memory 460    15000 false(valid-deref) 0.13 26 true 120    2900 false(reach) 1.4  17 unknown 0.037 8.0 true 6.9  54 true 1.0  17 unknown 0.037 5.0 true 250    430 timeout 920    740
memory-alloca/NoriSharma-2013FSE-Fig7-alloca_true-valid-memsafety.i out of memory 43    15000 false(valid-deref) 0.13 27 true 270    3600 false(reach) 1.4  18 unknown 0.058 8.0 true 6.9  54 true 3.1  45 unknown 0.037 5.0 timeout 920    1300 timeout 920    700
memory-alloca/NoriSharma-2013FSE-Fig8-alloca_true-valid-memsafety.i true 860    9300 false(valid-deref) 0.15 27 true 320    3500 false(reach) 1.4  18 unknown 0.042 8.0 true 6.9  54 true 1.0  21 unknown 0.041 5.0 timeout 920    640 timeout 920    510
memory-alloca/TelAviv-Amir-Minimum-alloca_true-valid-memsafety.i out of memory 39    15000 false(valid-deref) 0.14 26 true 120    3600 false(reach) 1.6  18 unknown 0.038 8.0 true 6.8  54 true 1.1  19 unknown 0.027 5.0 true 330    500 true 18    660
memory-alloca/Toulouse-BranchesToLoop-alloca_true-valid-memsafety.i out of memory 310    15000 false(valid-deref) 0.13 26 true 4.0  240 false(reach) 1.3  17 unknown 0.056 8.0 true 6.8  54 true 1.0  19 unknown 0.027 5.0 unknown 790    2900 timeout 920    890
memory-alloca/Toulouse-MultiBranchesToLoop-alloca_true-valid-memsafety.i out of memory 390    15000 unknown 0.14 27 true 3.9  270 false(reach) 1.4  18 unknown 0.043 8.0 true 6.9  54 true 1.0  20 unknown 0.044 5.0 timeout 920    950 timeout 920    1200
memory-alloca/Urban-2013WST-Fig2-alloca_true-valid-memsafety.i true 640    12000 false(valid-deref) 0.13 26 true 4.3  290 false(reach) 1.4  24 unknown 0.053 8.0 true 6.8  54 true 1.0  18 unknown 0.046 5.0 true 170    390 true 43    690
memory-alloca/Urban-2013WST-Fig2-modified1000-alloca_true-valid-memsafety.i true 880    2300 false(valid-deref) 0.13 26 true 2.1  170 false(reach) 0.79 24 unknown 0.046 8.0 true 6.9  54 true 1.0  18 unknown 0.041 5.0 true 230    430 timeout 920    900
memory-alloca/Urban-alloca_true-valid-memsafety.i crash 30    900 false(valid-deref) 0.14 26 true 77    3600 false(reach) 1.4  18 unknown 0.030 8.0 true 6.9  54 true 1.0  19 unknown 0.036 5.0 true 280    520 true 15    500
memory-alloca/a.01-alloca_true-valid-memsafety.i true 870    3900 unknown 0.13 26 true 14    980 false(reach) 2.3  47 unknown 0.037 8.0 true 6.8  54 true 3.9  37 unknown 0.033 5.0 timeout 920    2300 unknown 270    2800
memory-alloca/a.04-alloca_true-valid-memsafety.i true 90    1800 unknown 0.13 26 true 2.9  210 false(reach) 1.4  18 unknown 0.035 8.0 true 6.9  54 true 1.1  30 unknown 0.040 5.0 true 840    1800 timeout 920    2900
memory-alloca/a.05-alloca_true-valid-memsafety.i true 90    1800 unknown 0.11 26 true 2.9  210 false(reach) 1.2  18 unknown 0.044 8.0 true 6.8  54 true 1.1  20 unknown 0.020 5.0 timeout 920    2200 unknown 820    2800
memory-alloca/a.06-alloca_true-valid-memsafety.i true 98    12000 unknown 0.13 26 true 3.2  210 false(reach) 1.4  19 unknown 0.050 8.0 true 6.8  54 true 1.1  21 unknown 0.024 5.0 timeout 920    2700 timeout 920    2800
memory-alloca/a.07-alloca_true-valid-memsafety.i out of memory 27    15000 false(valid-deref) 0.14 26 true 3.1  210 false(reach) 1.4  18 unknown 0.047 8.0 true 6.8  54 true 1.0  21 unknown 0.041 5.0 unknown 750    2500 unknown 190    1800
memory-alloca/a.08-alloca_true-valid-memsafety.i true 280    3300 unknown 0.13 26 true 3.0  210 false(reach) 1.4  18 unknown 0.046 8.0 true 6.8  54 true 1.0  20 unknown 0.044 5.0 unknown 680    2400 unknown 86    2800
memory-alloca/a.09_assume-alloca_true-valid-memsafety.i true 100    2100 false(valid-deref) 0.13 26 true 3.6  230 false(reach) 1.4  18 unknown 0.057 8.0 true 6.8  54 true 1.0  19 unknown 0.029 5.0 unknown 460    2600 unknown 850    3000
memory-alloca/a.10-alloca_true-valid-memsafety.i out of memory 69    15000 false(valid-deref) 0.14 26 true 270    3500 false(reach) 1.4  18 unknown 0.050 8.0 true 6.8  54 true 1.0  20 unknown 0.042 5.0 timeout 920    2000 unknown 150    2800
memory-alloca/add_last-alloca_true-valid-memsafety.i true 850    1400 false(valid-deref) 0.15 28 true 1.7  160 false(reach) 1.3  18 unknown 0.045 8.0 true 6.8  54 unknown 2.0  19 unknown 0.037 5.0 timeout 920    620 timeout 920    410
memory-alloca/array01-alloca_true-valid-memsafety.i true 850    2600 false(valid-deref) 0.14 26 true 45    3500 false(reach) 1.5  28 unknown 0.045 8.0 true 6.8  54 unknown 2.1  19 unknown 0.035 5.0 true 120    380 true 8.2  270
memory-alloca/array02-alloca_true-valid-memsafety.i true 850    2400 false(valid-deref) 0.13 26 true 76    4000 false(reach) 2.0  47 unknown 0.046 8.0 true 11    54 unknown 2.1  19 unknown 0.039 5.0 true 120    400 true 8.7  270
memory-alloca/array03-alloca_true-valid-memsafety.i true 850    5600 false(valid-deref) 0.15 28 true 260    3500 false(reach) 2.2  36 unknown 0.047 8.0 true 14    54 unknown 2.1  19 unknown 0.037 5.0 unknown 5.7  240 unknown 5.5  250
memory-alloca/aviad_true-alloca_true-valid-memsafety.i out of memory 360    15000 false(valid-deref) 0.15 27 true 190    3500 false(reach) 0.68 17 unknown 0.053 8.0 true 6.8  54 true 1.0  26 unknown 0.044 5.0 timeout 920    2000 unknown 760    2800
memory-alloca/b.01-alloca_true-valid-memsafety.i true 89    1800 false(valid-deref) 0.13 26 true 2.9  210 false(reach) 1.3  17 unknown 0.041 8.0 true 6.8  54 true 1.0  30 unknown 0.037 5.0 true 820    2600 unknown 78    2400
memory-alloca/b.02-alloca_true-valid-memsafety.i out of memory 38    15000 unknown 0.11 26 true 3.1  210 false(reach) 1.4  18 unknown 0.035 8.0 true 6.9  54 true 1.0  20 unknown 0.045 5.0 timeout 900    1800 unknown 210    2900
memory-alloca/b.03-no-inv_assume-alloca_true-valid-memsafety.i true 49    1100 false(valid-deref) 0.14 26 true 2.3  200 false(reach) 1.9  21 unknown 0.051 8.0 true 6.8  54 true 1.1  19 unknown 0.036 5.0 true 290    470 timeout 920    1000
memory-alloca/b.03_assume-alloca_true-valid-memsafety.i true 96    1900 false(valid-deref) 0.12 26 true 3.3  240 false(reach) 1.3  18 unknown 0.040 8.0 true 6.8  54 true 1.0  19 unknown 0.045 5.0 true 400    430 timeout 920    1000
memory-alloca/b.04-alloca_true-valid-memsafety.i crash 58    1300 false(valid-deref) 0.14 28 true 2.6  210 false(reach) 1.4  17 unknown 0.029 8.0 true 6.9  56 true 1.0  19 unknown 0.035 5.0 unknown 240    310 unknown 120    2400
memory-alloca/b.05-alloca_true-valid-memsafety.i out of memory 30    15000 false(valid-deref) 0.15 26 true 3.8  270 false(reach) 1.3  17 unknown 0.039 8.0 true 6.9  54 true 1.0  19 unknown 0.040 5.0 true 360    440 timeout 920    950
memory-alloca/b.06-alloca_true-valid-memsafety.i true 790    3600 false(valid-deref) 0.15 26 true 3.2  210 false(reach) 1.3  17 unknown 0.044 8.0 true 6.9  56 true 1.1  21 unknown 0.021 5.0 unknown 680    2600 unknown 270    2900
memory-alloca/b.07-alloca_true-valid-memsafety.i true 880    4200 unknown 0.13 26 true 3.3  210 false(reach) 1.4  18 unknown 0.050 8.0 true 6.8  54 true 1.0  22 unknown 0.047 5.0 unknown 820    3000 unknown 410    3000
memory-alloca/b.09-no-inv_assume-alloca_true-valid-memsafety.i true 190    14000 unknown 0.11 26 true 97    3600 false(reach) 0.71 18 unknown 0.034 8.0 true 6.8  54 true 1.0  21 unknown 0.036 5.0 timeout 910    2400 unknown 490    2500
memory-alloca/b.09_assume-alloca_true-valid-memsafety.i crash 710    14000 unknown 0.14 26 true 120    3600 false(reach) 0.76 18 unknown 0.036 8.0 true 6.9  54 true 1.0  21 unknown 0.034 5.0 timeout 920    2200 unknown 82    2900
memory-alloca/b.10-alloca_true-valid-memsafety.i out of memory 510    15000 unknown 0.12 26 true 72    4000 false(reach) 1.3  18 unknown 0.038 8.0 true 6.8  54 true 1.0  23 unknown 0.021 5.0 unknown 830    2500 unknown 370    2900
memory-alloca/b.11-alloca_true-valid-memsafety.i true 860    3900 unknown 0.13 26 true 110    3600 false(reach) 1.5  19 unknown 0.033 8.0 true 6.9  54 true 1.0  20 unknown 0.046 5.0 timeout 920    2200 unknown 140    3000
memory-alloca/b.12-alloca_true-valid-memsafety.i true 120    13000 unknown 0.12 26 true 170    3500 false(reach) 1.4  18 unknown 0.031 8.0 true 6.8  54 true 1.0  22 unknown 0.033 5.0 unknown 690    2900 unknown 92    2500
memory-alloca/b.13-alloca_true-valid-memsafety.i true 870    13000 false(valid-deref) 0.14 26 true 160    3500 false(reach) 1.5  20 unknown 0.033 8.0 true 6.8  54 true 1.1  24 unknown 0.041 5.0 timeout 920    2400 timeout 920    3000
memory-alloca/b.14-alloca_true-valid-memsafety.i true 860    4000 unknown 0.13 27 true 62    4000 false(reach) 2.2  42 unknown 0.046 8.0 true 6.8  54 true 1.0  22 unknown 0.041 5.0 unknown 620    2800 unknown 220    3000
memory-alloca/b.15-alloca_true-valid-memsafety.i true 870    4100 unknown 0.13 27 true 62    3900 false(reach) 2.4  56 unknown 0.050 8.0 true 6.8  54 true 1.0  23 unknown 0.028 5.0 unknown 650    2600 unknown 98    2800
memory-alloca/b.16-alloca_true-valid-memsafety.i true 870    4800 unknown 0.12 26 true 62    3300 false(reach) 1.9  33 unknown 0.034 8.0 true 6.8  54 true 1.0  24 unknown 0.035 5.0 unknown 730    2400 unknown 200    2800
memory-alloca/b.17-alloca_true-valid-memsafety.i true 870    4600 unknown 0.14 28 true 61    3400 false(reach) 2.3  48 unknown 0.038 8.0 true 6.8  54 true 1.1  23 unknown 0.036 5.0 unknown 710    2700 unknown 210    2500
memory-alloca/b.18-alloca_true-valid-memsafety.i true 860    11000 false(valid-deref) 0.14 27 true 24    1600 false(reach) 2.0  39 unknown 0.038 8.0 true 6.8  54 true 1.0  19 unknown 0.045 5.0 true 610    510 timeout 920    670
memory-alloca/bubblesort-alloca_true-valid-memsafety.i true 850    2400 false(valid-deref) 0.33 40 true 1.7  150 false(reach) 2.5  60 unknown 0.038 8.0 true 6.8  54 unknown 2.0  19 unknown 0.027 5.0 true 120    410 timeout 920    880
memory-alloca/c.01-no-inv-alloca_true-valid-memsafety.i true 710    13000 unknown 0.12 26 true 51    3800 false(reach) 2.2  47 unknown 0.049 8.0 true 6.9  54 true 1.9  41 unknown 0.037 5.0 unknown 630    2500 unknown 120    2900
memory-alloca/c.01_assume-alloca_true-valid-memsafety.i true 870    3900 false(valid-deref) 0.12 26 true 84    3600 false(reach) 2.4  50 unknown 0.041 8.0 true 6.8  54 true 1.9  22 unknown 0.044 5.0 true 440    510 timeout 920    870
memory-alloca/c.02-alloca_true-valid-memsafety.i out of memory 43    15000 unknown 0.13 26 true 48    3800 false(reach) 2.3  48 unknown 0.046 8.0 true 6.8  54 true 3.9  37 unknown 0.028 5.0 timeout 920    1800 unknown 240    2800
memory-alloca/c.03-alloca_true-valid-memsafety.i out of memory 52    15000 unknown 0.12 26 true 260    3500 false(reach) 1.4  18 unknown 0.042 8.0 true 6.8  54 true 1.0  21 unknown 0.040 5.0 unknown 650    2500 timeout 920    2700
memory-alloca/c.07-alloca_true-valid-memsafety.i true 880    3700 unknown 0.12 27 true 3.2  210 false(reach) 0.94 18 unknown 0.047 8.0 true 6.9  54 true 1.0  30 unknown 0.035 5.0 timeout 920    610 timeout 920    1300
memory-alloca/c.08-alloca_true-valid-memsafety.i out of memory 50    15000 unknown 0.12 26 true 42    3700 false(reach) 2.3  50 unknown 0.043 8.0 true 6.8  54 true 4.6  42 unknown 0.021 5.0 timeout 920    2100 unknown 100    2400
memory-alloca/count_down-alloca_true-valid-memsafety.i true 850    2200 false(valid-deref) 0.11 26 true 1.8  160 false(reach) 1.6  27 unknown 0.048 8.0 true 6.8  54 unknown 2.0  18 unknown 0.042 5.0 timeout 920    610 timeout 920    420
memory-alloca/cstrcat-alloca_true-valid-memsafety.i true 850    1200 false(valid-deref) 0.16 27 false(valid-deref) 1.9  170 false(reach) 1.4  18 unknown 0.037 8.0 true 6.9  54 unknown 2.0  19 unknown 0.023 5.0 unknown 62    440 unknown 16    400
memory-alloca/cstrchr-alloca_true-valid-memsafety.i true 850    880 unknown 0.10 26 true 1.8  160 false(reach) 1.4  17 unknown 0.084 8.0 true 6.8  54 unknown 2.0  20 unknown 0.038 5.0 unknown 5.4  240 unknown 5.4  240
memory-alloca/cstrcmp-alloca_true-valid-memsafety.i true 850    1000 unknown 0.13 27 true 1.8  160 false(reach) 1.3  18 unknown 0.10 9.0 true 6.9  54 unknown 2.1  18 unknown 0.038 5.0 unknown 5.0  240 unknown 5.2  240
memory-alloca/cstrcpy-alloca_true-valid-memsafety.i true 850    1400 false(valid-deref) 0.14 29 true 1.7  160 false(reach) 1.3  17 unknown 0.047 8.0 true 6.9  54 unknown 2.1  19 unknown 0.038 5.0 timeout 920    650 timeout 920    840
memory-alloca/cstrcspn-alloca_true-valid-memsafety.i true 850    1800 unknown 0.14 28 true 1.8  160 false(reach) 1.8  33 unknown 0.041 8.0 true 6.8  54 unknown 2.0  19 unknown 0.034 5.0 timeout 920    1200 unknown 600    1300
memory-alloca/cstrlen-alloca_true-valid-memsafety.i true 850    2200 unknown 0.11 26 true 1.7  160 false(reach) 1.3  17 unknown 0.044 8.0 true 6.9  56 unknown 2.1  19 unknown 0.037 5.0 true 110    370 true 7.8  270
memory-alloca/cstrncat-alloca_true-valid-memsafety.i true 850    830 false(valid-deref) 0.15 28 false(valid-deref) 1.8  160 false(reach) 1.4  18 unknown 0.044 8.0 true 7.0  54 unknown 2.0  20 unknown 0.045 5.0 unknown 160    470 timeout 920    1000
memory-alloca/cstrncmp-alloca_true-valid-memsafety.i true 850    2100 unknown 0.14 27 true 1.9  160 false(reach) 1.3  19 unknown 0.086 8.0 true 6.9  54 unknown 2.1  18 unknown 0.043 5.0 unknown 5.2  240 unknown 5.0  240
memory-alloca/cstrncpy-alloca_true-valid-memsafety.i true 850    1200 unknown 0.14 27 true 1.8  160 false(reach) 1.6  28 unknown 0.065 8.0 true 6.8  54 unknown 2.1  19 unknown 0.027 5.0 timeout 920    2000 timeout 920    550
memory-alloca/cstrpbrk-alloca_true-valid-memsafety.i true 850    1300 unknown 0.14 28 true 1.8  150 false(reach) 1.8  33 unknown 0.089 8.0 true 6.9  54 unknown 2.0  20 unknown 0.038 5.0 unknown 5.2  240 unknown 5.1  240
memory-alloca/cstrspn-alloca_true-valid-memsafety.i true 850    1300 unknown 0.15 29 true 1.8  150 false(reach) 1.8  33 unknown 0.049 8.0 true 6.8  54 unknown 2.1  20 unknown 0.034 5.0 timeout 920    1200 timeout 920    1300
memory-alloca/diff-alloca_true-valid-memsafety.i true 850    7000 false(valid-deref) 0.15 29 true 2.3  170 false(reach) 2.9  67 unknown 0.077 9.0 true 6.8  54 unknown 2.1  30 unknown 0.040 5.0 timeout 920    2100 timeout 920    930
memory-alloca/easySum-alloca_true-valid-memsafety.i out of memory 29    15000 false(valid-deref) 0.14 26 true 2.9  210 false(reach) 1.3  17 unknown 0.031 8.0 true 6.8  54 true 1.0  20 unknown 0.021 5.0 unknown 580    2600 unknown 130    2800
memory-alloca/ex1-alloca_true-valid-memsafety.i true 86    1800 unknown 0.13 27 true 3.4  230 false(reach) 0.95 17 unknown 0.032 8.0 true 6.8  54 true 1.0  19 unknown 0.038 5.0 unknown 5.5  240 unknown 5.6  250
memory-alloca/ex2-alloca_true-valid-memsafety.i out of memory 92    15000 false(valid-deref) 0.19 30 true 250    3600 false(reach) 1.6  19 unknown 0.044 8.0 true 6.8  54 true 1.0  23 unknown 0.032 5.0 unknown 5.7  240 unknown 5.3  250
memory-alloca/ex3a-alloca_true-valid-memsafety.i out of memory 260    15000 unknown 0.16 31 true 2.9  210 false(reach) 0.78 17 unknown 0.035 8.0 true 6.9  54 true 1.0  20 unknown 0.029 5.0 unknown 5.4  240 unknown 5.5  240
memory-alloca/ex3b-alloca_true-valid-memsafety.i out of memory 310    15000 unknown 0.16 30 true 3.5  220 false(reach) 1.3  17 unknown 0.049 8.0 true 6.8  54 true 1.0  20 unknown 0.043 5.0 unknown 5.4  240 unknown 5.7  250
memory-alloca/fermat-alloca_true-valid-memsafety.i true 880    4300 unknown 0.13 26 true 2.9  210 false(reach) 2.0  47 unknown 0.039 8.0 true 16    180 timeout 920    530 unknown 0.046 5.0 unknown 5.5  240 unknown 5.4  240
memory-alloca/flag-alloca_true-valid-memsafety.i true 300    3200 false(valid-deref) 0.12 26 true 3.0  210 false(reach) 1.3  17 unknown 0.036 8.0 true 6.9  54 true 1.0  20 unknown 0.020 5.0 unknown 790    2500 timeout 920    2100
memory-alloca/gcd1-alloca_true-valid-memsafety.i out of memory 190    15000 false(valid-deref) 0.13 27 true 110    3600 false(reach) 2.1  42 unknown 0.047 8.0 true 6.8  54 true 1.0  19 unknown 0.033 5.0 unknown 640    2700 unknown 380    2900
memory-alloca/genady-alloca_true-valid-memsafety.i true 140    1700 false(valid-deref) 0.13 26 true 2.5  200 false(reach) 1.3  17 unknown 0.049 8.0 true 6.8  54 true 1.0  20 unknown 0.037 5.0 true 270    540 timeout 920    580
memory-alloca/insertionsort-alloca_true-valid-memsafety.i true 850    960 false(valid-deref) 0.15 27 true 1.7  160 false(reach) 1.9  29 unknown 0.074 8.0 true 6.8  54 unknown 2.0  19 unknown 0.035 5.0 true 130    400 true 8.4  270
memory-alloca/java_AG313-alloca_true-valid-memsafety.i out of memory 55    15000 unknown 0.12 26 true 3.3  210 false(reach) 1.3  17 unknown 0.046 8.0 true 6.8  54 true 1.1  21 unknown 0.039 5.0 unknown 620    2900 unknown 140    2800
memory-alloca/java_Break-alloca_true-valid-memsafety.i true 120    12000 false(valid-deref) 0.13 26 true 1.8  150 false(reach) 1.3  17 unknown 0.047 8.0 true 6.8  54 true 1.0  29 unknown 0.027 5.0 true 300    440 true 94    370
memory-alloca/java_BubbleSort-alloca_true-valid-memsafety.i true 850    2400 unknown 0.29 39 true 1.7  160 false(reach) 2.7  68 unknown 0.047 8.0 true 6.8  54 unknown 2.0  20 unknown 0.047 5.0 true 120    370 true 14    390
memory-alloca/java_Continue1-alloca_true-valid-memsafety.i true 230    2500 false(valid-deref) 0.12 26 true 1.8  160 false(reach) 1.2  17 unknown 0.029 8.0 true 6.8  54 true 1.0  20 unknown 0.041 5.0 true 230    390 true 480    490
memory-alloca/java_LogBuiltIn-alloca_true-valid-memsafety.i out of memory 310    15000 unknown 0.12 28 true 3.0  210 false(reach) 1.1  17 unknown 0.049 8.0 true 6.8  54 true 1.0  20 unknown 0.021 5.0 true 600    560 timeout 920    900
memory-alloca/java_Nested-alloca_true-valid-memsafety.i true 880    1500 false(valid-deref) 0.14 26 true 2.2  170 false(reach) 2.0  39 unknown 0.039 8.0 true 6.8  54 true 1.0  20 unknown 0.038 5.0 unknown 590    2400 timeout 920    840
memory-alloca/java_Sequence-alloca_true-valid-memsafety.i true 650    3700 false(valid-deref) 0.14 26 true 2.1  170 false(reach) 1.1  17 unknown 0.053 8.0 true 6.8  54 true 1.0  20 unknown 0.031 5.0 unknown 820    2800 timeout 920    1000
memory-alloca/lis-alloca_true-valid-memsafety.i true 850    1800 false(valid-deref) 0.15 29 true 1.8  160 false(reach) 2.6  72 unknown 0.041 8.0 true 6.8  54 unknown 2.0  20 unknown 0.037 5.0 timeout 920    2100 unknown 350    720
memory-alloca/min_rf-alloca_true-valid-memsafety.i true 860    4600 false(valid-deref) 0.13 27 true 130    3600 false(reach) 1.6  18 unknown 0.056 8.0 true 6.9  54 true 2.8  39 unknown 0.023 5.0 timeout 920    1800 timeout 920    990
memory-alloca/mult_array-alloca_true-valid-memsafety.i true 850    10000 false(valid-deref) 0.16 31 true 1.8  160 false(reach) 1.4  21 unknown 0.054 8.0 true 7.0  54 unknown 2.1  20 unknown 0.039 5.0 unknown 5.2  240 unknown 5.3  240
memory-alloca/openbsd_cbzero-alloca_true-valid-memsafety.i true 76    860 false(valid-deref) 0.13 26 true 1.7  160 false(reach) 0.95 17 unknown 0.082 8.0 true 6.8  54 unknown 2.0  19 unknown 0.036 5.0 timeout 920    2200 timeout 920    820
memory-alloca/openbsd_cmemchr-alloca_true-valid-memsafety.i true 850    3000 false(valid-deref) 0.13 26 true 1.8  150 false(reach) 1.1  17 unknown 0.083 8.0 true 6.9  54 unknown 2.1  18 unknown 0.032 5.0 timeout 920    530 timeout 920    560
memory-alloca/openbsd_cmemrchr-alloca_true-valid-memsafety.i true 850    3100 false(valid-deref) 0.13 26 true 1.8  150 false(reach) 0.67 17 unknown 0.048 8.0 true 6.8  54 unknown 2.0  20 unknown 0.021 5.0 true 110    360 timeout 920    1000
memory-alloca/openbsd_cmemset-alloca_true-valid-memsafety.i true 77    770 false(valid-deref) 0.13 26 true 1.8  150 false(reach) 1.4  17 unknown 0.081 8.0 true 6.8  54 unknown 2.1  19 unknown 0.043 5.0 timeout 920    590 timeout 920    1000
memory-alloca/openbsd_cstpcpy-alloca_true-valid-memsafety.i true 850    1400 false(valid-deref) 0.14 26 true 1.7  160 false(reach) 1.8  23 unknown 0.032 8.0 true 6.8  54 unknown 2.0  29 unknown 0.046 5.0 timeout 920    710 timeout 920    780
memory-alloca/openbsd_cstpncpy-alloca_true-valid-memsafety.i true 850    1600 unknown 0.13 27 true 1.8  160 false(reach) 1.6  26 unknown 0.089 8.0 true 6.8  54 unknown 2.0  19 unknown 0.035 5.0 timeout 920    1300 timeout 920    640
memory-alloca/openbsd_cstrcat-alloca_true-valid-memsafety.i true 850    1300 false(valid-deref) 0.16 29 false(valid-deref) 2.0  160 false(reach) 1.3  19 unknown 0.043 8.0 true 6.8  54 unknown 2.1  19 unknown 0.037 5.0 unknown 140    430 timeout 920    870
memory-alloca/openbsd_cstrcmp-alloca_true-valid-memsafety.i true 850    1500 unknown 0.15 27 true 1.8  150 false(reach) 1.3  18 unknown 0.048 8.0 true 6.9  54 unknown 2.1  19 unknown 0.036 5.0 unknown 5.0  240 unknown 5.2  240
memory-alloca/openbsd_cstrcpy-alloca_true-valid-memsafety.i true 850    1400 false(valid-deref) 0.13 27 true 1.7  150 false(reach) 1.4  18 unknown 0.042 8.0 true 6.9  56 unknown 2.1  19 unknown 0.025 5.0 timeout 920    620 timeout 920    730
memory-alloca/openbsd_cstrcspn-alloca_true-valid-memsafety.i true 850    1300 unknown 0.15 27 true 1.8  160 false(reach) 1.8  39 unknown 0.034 8.0 true 6.9  54 unknown 2.1  19 unknown 0.034 5.0 unknown 430    410 timeout 920    530
memory-alloca/openbsd_cstrlcpy-alloca_true-valid-memsafety.i true 850    940 unknown 0.14 28 true 1.8  150 false(reach) 0.69 18 unknown 0.048 8.0 true 6.8  54 unknown 2.1  19 unknown 0.036 5.0 timeout 920    600 timeout 920    670
memory-alloca/openbsd_cstrlen-alloca_true-valid-memsafety.i true 850    2200 unknown 0.12 26 true 1.7  160 false(reach) 1.3  17 unknown 0.040 8.0 true 6.8  54 unknown 2.1  20 unknown 0.044 5.0 true 560    490 timeout 920    710
memory-alloca/openbsd_cstrncat-alloca_true-valid-memsafety.i true 850    770 false(valid-deref) 0.17 28 false(valid-deref) 1.8  160 false(reach) 1.0  18 unknown 0.035 8.0 true 6.9  54 unknown 2.1  19 unknown 0.032 5.0 unknown 350    610 timeout 920    700
memory-alloca/openbsd_cstrncmp-alloca_true-valid-memsafety.i true 850    1600 unknown 0.13 27 true 1.9  160 false(reach) 1.4  18 unknown 0.036 8.0 true 6.9  54 unknown 2.0  19 unknown 0.043 5.0 unknown 5.2  240 unknown 5.0  240
memory-alloca/openbsd_cstrncpy-alloca_true-valid-memsafety.i true 850    1600 unknown 0.14 27 true 1.8  150 false(reach) 1.6  25 unknown 0.076 8.0 true 6.8  54 unknown 2.0  19 unknown 0.033 5.0 timeout 920    590 timeout 920    660
memory-alloca/openbsd_cstrnlen-alloca_true-valid-memsafety.i true 850    2500 false(valid-deref) 0.13 26 true 1.8  150 false(reach) 1.3  17 unknown 0.040 8.0 true 6.8  54 unknown 2.0  19 unknown 0.024 5.0 true 630    480 true 690    580
memory-alloca/openbsd_cstrpbrk-alloca_true-valid-memsafety.i true 850    2100 unknown 0.13 29 true 1.8  160 false(reach) 1.8  38 unknown 0.071 8.0 true 6.9  54 unknown 2.1  20 unknown 0.032 5.0 unknown 5.0  240 unknown 5.2  240
memory-alloca/openbsd_cstrspn-alloca_true-valid-memsafety.i true 850    1200 unknown 0.15 28 true 1.8  150 false(reach) 2.2  52 unknown 0.035 8.0 true 6.8  54 unknown 2.0  19 unknown 0.030 5.0 timeout 920    1500 timeout 920    670
memory-alloca/openbsd_cstrstr-alloca_true-valid-memsafety.i true 850    1000 false(valid-deref) 0.19 32 true 1.8  160 false(reach) 8.6  140 unknown 0.051 8.0 true 6.9  54 unknown 2.0  21 unknown 0.020 5.0 unknown 5.4  240 unknown 5.0  240
memory-alloca/rec_strlen-alloca_true-valid-memsafety.i unknown 0.83 81 unknown 0.13 26 error (recursion) 1.7  150 false(reach) 0.74 17 unknown 0.060 9.0 true 6.8  54 unknown 2.1  19 unknown 0.021 5.0 true 130    370 true 8.7  270
memory-alloca/selectionsort-alloca_true-valid-memsafety.i true 850    11000 false(valid-deref) 0.13 27 true 1.7  160 false(reach) 2.3  65 unknown 0.084 8.0 true 6.8  54 unknown 2.0  19 unknown 0.046 5.0 true 120    360 timeout 920    770
memory-alloca/stroeder1-alloca_true-valid-memsafety.i true 98    1600 false(valid-deref) 0.13 26 true 1.7  160 false(reach) 0.90 17 unknown 0.044 8.0 true 6.9  54 unknown 2.1  19 unknown 0.032 5.0 true 110    370 true 6.9  270
memory-alloca/stroeder2-alloca_true-valid-memsafety.i true 850    3600 false(valid-deref) 0.14 26 true 39    3500 false(reach) 1.5  27 unknown 0.028 8.0 true 6.8  54 unknown 2.0  19 unknown 0.032 5.0 true 120    390 true 8.7  280
memory-alloca/strreplace-alloca_true-valid-memsafety.i true 850    690 unknown 0.14 26 true 1.7  150 false(reach) 1.3  17 unknown 0.071 8.0 true 6.8  54 unknown 2.0  20 unknown 0.039 5.0 true 120    380 true 8.6  270
memory-alloca/subseq-alloca_true-valid-memsafety.i true 850    1300 false(valid-deref) 0.15 27 true 1.8  160 false(reach) 1.4  19 unknown 0.062 8.0 true 6.8  54 unknown 2.1  20 unknown 0.042 5.0 unknown 150    310 true 430    550
memory-alloca/substring-alloca_true-valid-memsafety.i false(valid-deref) 2.4  140 false(valid-deref) 0.17 28 true 1.8  160 false(reach) 2.0  41 unknown 0.083 8.0 true 6.9  54 unknown 2.1  19 unknown 0.041 5.0 unknown 440    540 timeout 920    1000
memory-alloca/twisted-alloca_true-valid-memsafety.i out of memory 560    15000 false(valid-deref) 0.16 26 true 1.8  160 false(reach) 38    790 unknown 0.045 8.0 true 6.9  56 true 1.1  20 unknown 0.044 5.0 unknown 710    2800 timeout 920    2600
../../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)
total files 205 100000 810000 205 18000 140000 205 5700 200000 205 17000 140000 205 1900 1800 205 8400 70000 205 13000 37000 205 7.4 1000 205 89000 190000 205 87000 190000
correct results 154 82000 360000 62 14000 120000 199 5700 200000 10 490 440 11 25 200 165 2100 9100 134 460 10000 0 - - 70 13000 35000 54 4800 21000
false negatives 5 2800 14000 7 3400 9300 0 - - 8 0.79 150 0 - - 15 100 810 0 - - 0 - - 0 - - 0 - -
false positives 0 - - 0 - - 0 - - 154 1800 9100 0 - - 0 - - 0 - - 0 - - 0 - - 0 - -
false properties 2 4.1 270 74 150 6400 4 7.5 640 0 - - 0 - - 16 150 890 1 8.0 59 0 - - 2 15 520 2 15 520
score (205 files, max score: 361) 200 - - -433 - - 326 - - -1000 - - 22 - - 28 - - 221 - - 0 - - 95 - - 66 - -
Tool Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Forester Map2Check PredatorHP Seahorn Ultimate Automizer r12950 Ultimate Kojak r12950