Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]]
Run set [sv-comp17.MemSafety-Arrays; sv-comp17.MemSafety-Heap; sv-comp17.MemSafety-LinkedLists; sv-comp17.MemSafety-Other]
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) .19 .19 1.8  20 .0082 0      error 4.4  2.4  77   260 false(valid-deref) 8.9 4.8 180 350 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) .11 .10 .98 17 0      0      error 3.4  1.9  54   260 false(valid-deref) 8.6 4.7 190 340 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) .25 .24 2.3  24 .0082 0      error 4.4  2.4  82   260 false(valid-deref) 10   5.4 140 350 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) .11 .11 1.1  20 0      2.3    false(valid-deref) 3.2  1.8  68   240 false(valid-deref) 8.3 4.5 170 340 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) .12 .12 1.1  19 0      0      error 4.5  2.5  85   250 false(valid-deref) 17   9.5 360 560 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) .21 .20 1.7  20 .0082 0      error 4.3  2.3  70   260 false(valid-deref) 11   5.8 220 370 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) .12 .12 1.1  21 0      0      error 3.4  1.9  55   250 false(valid-deref) 8.5 4.6 170 350 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) .12 .11 1.3  21 0      0      error 3.3  1.9  46   250 false(valid-deref) 8.9 4.7 150 320 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) .13 .12 1.3  20 0      0      true 4.3  2.4  68   270 false(valid-deref) 12   6.7 270 380 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) .11 .11 1.1  20 0      0      error 3.6  2.0  65   250 false(valid-deref) 8.4 4.4 180 330 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) .39 .38 3.7  39 .0082 0      error 5.2  2.8  55   260 false(valid-deref) 28   17   520 660 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) .24 .23 1.8  20 .0082 0      exception 3.0  1.7  51   190 false(valid-deref) 15   8.2 320 420 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) .25 .24 2.8  27 .0082 0      error 5.3  2.8  58   260 false(valid-deref) 10   5.5 230 350 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) .32 .32 3.0  33 .0082 2.0    error 4.1  2.2  77   260 false(valid-deref) 10   5.3 130 340 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) .70 .69 9.5  83 .0082 0      error 4.7  2.6  97   260 false(valid-deref) 12   6.6 230 360 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) .11 .10 1.0  18 0      0      error 3.3  1.9  72   250 false(valid-deref) 8.4 4.5 180 340 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) .12 .11 .88 17 0      0      error 3.2  1.8  69   250 false(valid-deref) 8.7 4.7 180 350 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i error (134) 120    120    1200    13000 .66   .074  - - error (invalid witness file) .48 .31 5.0 40 error (invalid witness file) 7.1 3.8 87 320
array-memsafety/array01-alloca_true-valid-memsafety.i error (42) 850    850    6300    8900 3.6    .19   - - error (invalid witness file) .52 .32 8.9 40 error (invalid witness file) 7.0 3.7 93 300
array-memsafety/array02-alloca_true-valid-memsafety.i error (1) 470    470    3700    14000 2.6    0      - - error (invalid witness file) .63 .41 7.1 39 error (invalid witness file) 5.7 3.0 120 300
array-memsafety/array03-alloca_true-valid-memsafety.i error (134) 510    510    3700    14000 1.7    12      - - error (invalid witness file) .59 .38 10   42 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i error (42) 850    850    6600    2700 3.2    0      - - error (invalid witness file) .50 .33 8.6 40 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/count_down-alloca_true-valid-memsafety.i error (42) 850    850    5400    9000 3.0    0      - - error (invalid witness file) .47 .31 6.4 39 error (invalid witness file) 5.7 3.0 100 290
array-memsafety/cstrcat-alloca_true-valid-memsafety.i error (134) 110    110    1100    14000 .72   .18   - - error (invalid witness file) .59 .38 9.6 39 error (invalid witness file) 6.6 3.5 88 300
array-memsafety/cstrchr-alloca_true-valid-memsafety.i error (42) 850    850    6700    4600 5.1    2.4    - - error (invalid witness file) .49 .32 8.2 39 error (invalid witness file) 6.3 3.4 100 300
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i error (42) 850    850    9700    1800 4.2    0      - - error (invalid witness file) .54 .36 8.5 42 error (invalid witness file) 6.6 3.5 110 300
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i error (134) 83    83    940    13000 1.8    .074  - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 7.1 3.7 110 320
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i error (42) 850    850    7300    9000 4.3    0      - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 8.1 4.2 100 310
array-memsafety/cstrlen-alloca_true-valid-memsafety.i error (42) 850    850    4500    3900 4.1    0      - - error (invalid witness file) .49 .32 8.5 41 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i error (134) 380    380    3600    14000 .78   0      - - error (invalid witness file) .54 .35 9.7 39 error (invalid witness file) 6.3 3.3 130 310
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i error (42) 850    850    8500    2000 2.4    0      - - error (invalid witness file) .49 .31 5.7 40 error (invalid witness file) 7.0 3.7 100 300
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i error (134) 220    220    3000    14000 4.8    12      - - error (invalid witness file) .59 .38 10   40 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i error (42) 850    850    8600    9200 4.5    0      - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i error (42) 850    850    7400    9100 3.8    .10   - - error (invalid witness file) .51 .34 5.0 39 error (invalid witness file) 6.7 3.6 72 290
array-memsafety/diff-alloca_true-valid-memsafety.i error (42) 850    850    3400    6500 2.0    2.4    - - error (invalid witness file) .60 .38 12   42 error (invalid witness file) 6.1 3.2 84 280
array-memsafety/insertionsort-alloca_true-valid-memsafety.i error (42) 850    850    3700    9000 .24   0      - - error (invalid witness file) .61 .39 8.9 40 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i error (42) 850    850    6500    2800 2.9    0      - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 6.8 3.6 81 290
array-memsafety/lis-alloca_true-valid-memsafety.i error (42) 850    850    5700    2500 1.8    0      - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.9 3.6 80 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i error (134) 110    110    1300    14000 1.8    .074  - - error (invalid witness file) .51 .32 13   39 error (invalid witness file) 8.2 4.3 84 320
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i error (1) 83    83    1100    13000 1.5    0      - - error (invalid witness file) .59 .37 14   44 error (invalid witness file) 7.7 4.0 110 320
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i error (42) 850    850    5900    1300 7.8    0      - - error (invalid witness file) .47 .30 8.6 39 error (invalid witness file) 8.4 4.4 85 310
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i error (42) 850    850    3900    1000 .44   0      - - error (invalid witness file) .60 .38 6.2 42 error (invalid witness file) 6.1 3.2 100 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i error (1) 84    84    870    13000 1.5    0      - - error (invalid witness file) .57 .37 9.6 41 error (invalid witness file) 6.1 3.2 100 310
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i error (1) 93    94    1000    13000 2.1    0      - - error (invalid witness file) .65 .40 6.4 40 error (invalid witness file) 6.8 3.5 110 310
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i error (134) 220    220    2600    14000 5.8    0      - - error (invalid witness file) .50 .33 11   41 error (invalid witness file) 6.1 3.2 120 310
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i error (134) 110    110    1300    14000 .73   .36   - - error (invalid witness file) .62 .40 8.0 40 error (invalid witness file) 5.3 2.8 82 290
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i error (42) 850    850    8900    2200 4.8    .10   - - error (invalid witness file) .50 .32 5.5 39 error (invalid witness file) 6.0 3.2 99 300
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i error (134) 96    96    1100    13000 1.9    .20   - - error (invalid witness file) .51 .34 6.8 42 error (invalid witness file) 6.5 3.4 110 300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i error (42) 850    850    2600    380 4.6    0      - - error (invalid witness file) .51 .32 13   39 error (invalid witness file) 7.7 4.0 91 300
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i error (42) 850    850    4600    13000 .71   0      - - error (invalid witness file) .52 .33 10   39 error (invalid witness file) 7.8 4.1 80 300
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i error (42) 850    850    5100    4700 4.6    0      - - error (invalid witness file) .57 .37 10   39 error (invalid witness file) 7.2 3.8 91 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i error (134) 430    430    2500    14000 .82   .18   - - error (invalid witness file) .50 .31 7.8 40 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i error (42) 850    850    8800    2100 2.7    .19   - - error (invalid witness file) .49 .31 8.3 40 error (invalid witness file) 5.7 3.0 110 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i error (134) 200    200    2400    14000 5.7    .18   - - error (invalid witness file) .51 .32 8.2 40 error (invalid witness file) 7.0 3.6 120 310
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i error (42) 850    850    4700    2100 6.0    0      - - error (invalid witness file) .55 .36 11   41 error (invalid witness file) 6.9 3.7 100 300
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i error (42) 850    850    3900    300 4.6    12      - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.7 3.1 110 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i error (42) 850    850    4900    920 .19   0      - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 7.2 3.8 81 290
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i error (42) 850    850    3100    7600 .38   0      - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.9 3.6 83 310
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i error (42) 850    850    5000    8300 4.1    0      - - error (invalid witness file) .47 .31 7.9 39 error (invalid witness file) 7.6 3.9 85 290
array-memsafety/selectionsort-alloca_true-valid-memsafety.i error (134) 63    63    640    14000 .18   .074  - - error (invalid witness file) .50 .33 8.4 39 error (invalid witness file) 7.6 3.9 89 310
array-memsafety/stroeder1-alloca_true-valid-memsafety.i error (134) 76    76    1000    14000 .88   0      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.3 3.3 110 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i error (134) 61    61    560    14000 .12   .074  - - error (invalid witness file) .68 .42 8.1 41 error (invalid witness file) 7.2 3.7 86 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i error (134) 220    220    1300    14000 .80   2.4    - - error (invalid witness file) .48 .33 11   39 error (invalid witness file) 6.6 3.5 95 300
array-memsafety/subseq-alloca_true-valid-memsafety.i error (42) 850    850    4700    1900 .66   0      - - error (invalid witness file) .52 .33 10   41 error (invalid witness file) 6.1 3.2 120 290
array-memsafety/substring-alloca_true-valid-memsafety.i error (42) 850    850    6500    10000 5.6    .10   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 8.7 4.5 85 310
array-examples/relax_false-valid-deref.i false(valid-deref) .20 .20 1.9  20 .0082 0      error 4.5  2.5  100   260 false(valid-deref) 10   5.7 140 350 - -
array-examples/sanfoundry_24_false-valid-deref.i error (42) 850    850    5200    6200 15      0      error (invalid witness file) .50 .31 9.2 39 error (invalid witness file) 5.5 3.0 120 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i out of memory 74    74    930    15000 .76   2.0    error (invalid witness file) .64 .40 7.9 40 error (invalid witness file) 6.0 3.2 110 290 - -
array-examples/standard_strcpy_original_false-valid-deref.i out of memory 74    74    960    15000 .76   0      error (invalid witness file) .49 .32 9.8 40 error (invalid witness file) 6.0 3.2 91 300 - -
memsafety/960521-1_false-valid-deref.i false(valid-deref) 2.7  2.7  28    51 1.6    11      error 12    6.1  230   570 out of memory 89   55   1400 7000 - -
memsafety/test-0137_false-valid-deref.i error (1) .21 .21 2.3  20 .0082 0      error (invalid witness file) .48 .32 11   40 error (invalid witness file) 5.9 3.1 130 290 - -
memsafety/test-0235_false-valid-deref.i error (1) 1.0  1.1  12    33 .0082 8.2    error (invalid witness file) .57 .35 13   40 error (invalid witness file) 6.8 3.6 100 300 - -
memsafety/960521-1_false-valid-free.i false(valid-free) 2.7  2.7  30    40 2.0    0      error 11    5.8  180   550 timeout 90   55   1700 7000 - -
memsafety/test-0158_false-valid-free.i false(valid-free) .20 .20 1.5  20 .0082 0      true 4.5  2.4  73   270 false(valid-free) 12   6.7 190 370 - -
memsafety/test-0232_false-valid-free.i false(valid-free) .21 .21 2.2  21 .0082 0      error 4.5  2.5  75   260 false(valid-free) 26   15   540 650 - -
memsafety/20020406-1_false-valid-memtrack.i error (134) 46    46    550    13000 2.4    .26   error (invalid witness file) .49 .31 7.3 39 error (invalid witness file) 6.3 3.3 130 300 - -
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 3.3  3.3  44    85 .76   0      exception 3.5  1.9  52   210 true 9.4 5.0 180 340 - -
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 3.6  3.6  49    150 .22   0      assertion 6.1  3.3  58   270 true 8.8 4.7 170 360 - -
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) .21 .21 2.0  23 .0082 0      assertion 4.7  2.6  83   270 true 8.5 4.5 140 330 - -
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 3.8  3.8  43    160 .22   8.2    assertion 5.8  3.1  67   260 true 9.5 5.0 180 360 - -
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) .19 .19 1.7  20 .0082 0      error 4.2  2.3  81   250 true 9.0 4.7 180 330 - -
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) .27 .26 3.1  23 .0082 .35   error 5.1  2.8  90   270 true 8.7 4.7 160 330 - -
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) .21 .21 1.7  22 .0082 2.4    true 4.1  2.3  87   260 true 7.6 4.0 150 320 - -
memsafety/test-0220_false-valid-memtrack.i error (1) .20 .20 2.2  21 .0082 0      error (invalid witness file) .49 .31 9.0 39 error (invalid witness file) 6.4 3.4 140 300 - -
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) .18 .18 2.7  20 .0082 0      error 5.3  2.9  76   260 true 9.2 4.9 180 330 - -
memsafety/test-0234_false-valid-memtrack.i error (1) .67 .67 6.8  21 .0082 .23   error (invalid witness file) .51 .32 5.5 40 error (invalid witness file) 7.2 3.8 77 300 - -
memsafety/test-0235_false-valid-memtrack.i error (1) .77 .76 8.7  22 .0082 0      error (invalid witness file) .51 .33 12   39 error (invalid witness file) 5.2 2.8 78 290 - -
memsafety/960521-1_true-valid-memsafety.i out of memory 140    140    1900    15000 1.6    0      - - error (invalid witness file) .47 .31 5.4 39 error (invalid witness file) 6.8 3.6 85 300
memsafety/lockfree-3.0_true-valid-memsafety.i error (42) 850    850    6200    2100 1.5    .10   - - error (invalid witness file) .66 .43 12   41 error (invalid witness file) 6.3 3.3 97 300
memsafety/test-0019_true-valid-memsafety.i true .35 .35 3.0  20 .016  0      - - true 3.9  2.2  72   250 true 20   12   260 550
memsafety/test-0102_true-valid-memsafety.i error (1) 16    16    230    270 1.6    0      - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 5.8 3.1 120 300
memsafety/test-0134_true-valid-memsafety.i error (1) .21 .21 2.3  20 .0082 0      - - error (invalid witness file) .50 .32 8.9 41 error (invalid witness file) 7.1 3.8 100 300
memsafety/test-0158_true-valid-memsafety.i true .33 .32 3.5  20 .016  .16   - - true 3.7  2.1  73   250 true 12   6.7 180 380
memsafety/test-0214_true-valid-memsafety.i error (42) 850    850    5400    1800 .025  0      - - error (invalid witness file) .49 .32 9.4 40 error (invalid witness file) 6.5 3.4 110 310
memsafety/test-0217_true-valid-memsafety.i error (1) 42    42    560    13000 .025  .10   - - error (invalid witness file) .60 .38 8.8 44 error (invalid witness file) 6.0 3.2 110 310
memsafety/test-0218_true-valid-memsafety.i error (42) 850    850    5300    4100 .025  0      - - error (invalid witness file) .51 .34 10   40 error (invalid witness file) 6.9 3.6 110 320
memsafety/test-0219_true-valid-memsafety.i error (1) .22 .21 2.0  20 .0082 0      - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 7.4 3.9 76 290
memsafety/test-0232_true-valid-memsafety.i error (1) 29    29    370    190 1.2    12      - - error (invalid witness file) .48 .31 8.2 39 error (invalid witness file) 6.4 3.4 85 300
memsafety/test-0234_true-valid-memsafety.i error (1) .74 .74 7.4  22 .0082 .033  - - error (invalid witness file) .51 .34 4.9 39 error (invalid witness file) 6.0 3.2 120 290
memsafety/test-0235_true-valid-memsafety.i error (1) .97 .97 11    26 .0082 0      - - error (invalid witness file) .49 .33 7.0 40 error (invalid witness file) 5.7 3.0 120 300
memsafety/test-0236_true-valid-memsafety.i error (1) .82 .81 8.5  23 .0082 0      - - error (invalid witness file) .51 .35 6.2 41 error (invalid witness file) 5.6 3.0 96 290
memsafety/test-0237_true-valid-memsafety.i error (1) .80 .80 11    23 .0082 .029  - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 7.2 3.8 100 310
memsafety/test-0504_true-valid-memsafety.i error (1) 310    310    3900    670 2.7    2.2    - - error (invalid witness file) .47 .31 6.8 40 error (invalid witness file) 5.9 3.1 110 300
memsafety/test-0513_true-valid-memsafety.i error (42) 850    850    5600    1900 1.4    0      - - error (invalid witness file) .62 .37 8.5 40 error (invalid witness file) 6.4 3.4 110 300
memsafety/test-0521_true-valid-memsafety.i error (134) 150    150    1800    14000 4.3    .074  - - error (invalid witness file) .52 .32 13   39 error (invalid witness file) 5.1 2.8 97 290
memsafety/test-memleak_nexttime_true-valid-memsafety.i error (1) .18 .18 1.9  21 .0082 0      - - error (invalid witness file) .50 .32 8.7 40 error (invalid witness file) 6.8 3.5 89 300
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i error (1) 78    78    960    300 1.6    .10   - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 5.9 3.2 120 300
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i error (42) 850    850    8000    420 .51   .10   - - error (invalid witness file) .54 .34 10   40 error (invalid witness file) 7.0 3.7 85 300
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i error (42) 850    850    8300    630 .76   .19   - - error (invalid witness file) .51 .33 8.4 40 error (invalid witness file) 6.8 3.5 95 300
memsafety-ext/tree_cnstr_true-valid-memsafety.i error (42) 850    850    4900    2100 1.1    .10   - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.3 3.3 110 300
memsafety-ext/tree_dsw_true-valid-memsafety.i error (42) 850    850    4100    1700 .68   .10   - - error (invalid witness file) .55 .34 11   43 error (invalid witness file) 8.2 4.3 95 310
memsafety-ext/tree_of_cslls_true-valid-memsafety.i error (42) 850    850    8100    1000 .025  .10   - - error (invalid witness file) .55 .35 9.6 40 error (invalid witness file) 6.2 3.3 110 290
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i error (42) 850    850    5800    2000 .76   0      - - error (invalid witness file) .51 .34 4.6 39 error (invalid witness file) 6.5 3.4 90 300
memsafety-ext/tree_stack_true-valid-memsafety.i error (42) 850    850    4900    1400 .63   0      - - error (invalid witness file) .51 .33 8.7 41 error (invalid witness file) 5.5 2.9 110 290
memsafety-ext2/split_list_test05_false-valid-deref.i out of memory 310    310    4100    15000 .0082 0      error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.2 3.3 130 300 - -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i false(valid-memtrack) 17    17    190    630 8.7    0      error 15    7.7  250   620 true 43   24   680 3400 - -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i false(valid-memtrack) 1.9  1.9  25    110 .45   0      error 7.9  4.2  150   310 true 14   7.5 280 760 - -
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 1.4  1.4  16    34 .36   0      assertion 6.1  3.2  110   280 true 10   5.3 150 420 - -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(valid-memtrack) 16    16    200    280 2.8    0      error 5.9  3.1  96   290 true 12   6.1 240 520 - -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i error (42) 850    850    10000    2500 9.0    0      - - error (invalid witness file) .50 .31 7.1 42 error (invalid witness file) 6.1 3.2 99 300
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i error (1) 52    52    600    480 2.4    .10   - - error (invalid witness file) .69 .44 7.8 42 error (invalid witness file) 6.2 3.3 110 300
memsafety-ext2/length_test03_true-valid-memsafety.i error (42) 850    850    4200    2000 2.0    0      - - error (invalid witness file) .59 .39 8.9 40 error (invalid witness file) 7.0 3.7 87 300
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i error (1) 200    200    2100    800 8.6    0      - - error (invalid witness file) .50 .33 7.1 40 error (invalid witness file) 7.8 4.1 73 310
memsafety-ext2/split_list_test05_true-valid-memsafety.i out of memory 210    210    2500    15000 .0082 0      - - error (invalid witness file) .48 .32 7.4 40 error (invalid witness file) 7.5 3.9 59 300
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) .20 .20 1.8  20 .0082 0      error 5.4  2.9  71   270 false(valid-deref) 11   5.7 210 370 - -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 100    100    1100    390 2.2    0      assertion 6.5  3.4  65   290 false(valid-free) 61   32   1100 1700 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) .26 .26 1.9  21 .0082 0      assertion 4.4  2.4  83   260 false(valid-free) 9.0 4.8 180 330 - -
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) .20 .20 2.1  20 .0082 .16   error 4.5  2.5  82   260 false(valid-free) 10   5.6 150 360 - -
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) .18 .17 1.8  20 .0082 0      true 4.2  2.3  84   260 false(valid-free) 13   6.8 200 370 - -
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) .21 .21 1.6  20 .0082 0      error 5.1  2.7  88   260 true 9.5 5.0 130 320 - -
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) .21 .20 1.5  20 .0082 0      true 4.8  2.7  100   270 true 6.7 3.6 130 320 - -
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) .23 .22 2.1  20 .0082 0      error 5.0  2.7  110   270 true 9.0 4.8 190 330 - -
list-ext-properties/960521-1_1_true-valid-memsafety.i true 56    56    730    850 .50   0      - - true 10    5.3  100   420 timeout 960   900   18000 1200
list-ext-properties/list-ext_1_true-valid-memsafety.i true 110    110    1200    290 1.7    .10   - - true 22    12    260   950 timeout 960   870   29000 1600
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 45    45    650    150 1.8    .16   - - timeout 910    860    17000   4800 timeout 960   870   31000 1600
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 48    48    550    270 1.9    0      - - true 19    9.7  110   650 timeout 960   890   31000 1700
list-ext-properties/test-0019_1_true-valid-memsafety.i true .33 .33 3.2  20 .016  0      - - true 5.5  3.0  66   250 true 50   32   850 740
list-ext-properties/test-0158_1_true-valid-memsafety.i true .33 .33 2.9  20 .016  0      - - true 3.9  2.1  85   250 true 11   6.1 250 380
list-ext-properties/test-0214_1_true-valid-memsafety.i true 430    430    3300    460 2.6    0      - - timeout 910    830    17000   5900 timeout 960   900   30000 2300
list-ext-properties/test-0217_1_true-valid-memsafety.i true 400    400    3400    390 3.5    0      - - timeout 950    870    15000   5400 timeout 960   870   26000 2800
list-ext-properties/test-0232_1_true-valid-memsafety.i true 6.1  6.1  88    62 .77   0      - - true 8.1  4.3  85   390 timeout 960   900   15000 1100
list-ext-properties/test-0504_1_true-valid-memsafety.i true 4.6  4.6  64    87 .46   .10   - - true 420    380    8800   4800 timeout 960   900   23000 1500
list-ext-properties/test-0513_1_true-valid-memsafety.i true 10    10    110    290 1.5    .16   - - true 7.0  3.7  100   280 timeout 960   870   23000 1900
memory-alloca/c.03-alloca_true-valid-memsafety.i error (42) 850    850    6900    2100 11      0      - - error (invalid witness file) .51 .33 6.9 41 error (invalid witness file) 6.2 3.3 98 300
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) .15 .15 .97 18 .0041 .16   error 3.6  2.0  55   260 false(valid-deref) 9.0 4.8 170 350 - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) .15 .14 .92 18 .0041 .16   error 3.8  2.1  64   260 false(valid-deref) 11   6.0 230 360 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) .14 .13 .94 18 .0041 0      error 3.7  2.1  55   260 false(valid-deref) 7.8 4.2 140 320 - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) .12 .12 .90 18 .0041 .19   error 3.3  1.9  47   270 false(valid-deref) 7.7 4.2 160 320 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 1.7  1.7  17    26 1.8    .16   error 14    7.1  190   620 timeout 98   61   1500 5600 - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 1.7  1.7  19    26 1.8    0      error 11    5.5  160   600 timeout 96   65   1600 4600 - -
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 2.0  1.9  22    19 .22   0      error 3.1  1.7  55   250 false(valid-deref) 7.9 4.2 170 330 - -
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 2.1  2.1  20    19 .23   0      error 3.3  1.9  72   250 false(valid-deref) 7.4 4.1 150 340 - -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 2.0  2.0  21    19 .23   .40   error 3.2  1.8  52   260 false(valid-deref) 8.1 4.4 170 320 - -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 2.1  2.1  21    19 .23   0      error 3.3  1.9  68   260 false(valid-deref) 8.0 4.4 160 350 - -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 2.1  2.1  21    18 .23   0      error 4.0  2.2  58   270 false(valid-deref) 7.4 4.0 140 330 - -
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 2.1  2.1  20    19 .23   0      error 3.8  2.1  52   260 false(valid-deref) 7.9 4.2 170 330 - -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c error (42) 850    850    4300    5500 49      0      - - error (invalid witness file) .49 .31 9.5 39 error (invalid witness file) 6.7 3.6 85 300
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c true 2.0  2.0  25    19 2.2    0      - - true 10    5.3  69   450 true 21   13   510 550
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 1.7  1.7  19    19 1.2    0      - - true 9.5  5.0  180   420 true 25   14   340 500
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c true 2.0  2.0  25    19 2.2    0      - - true 11    5.7  220   460 true 29   18   310 560
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 6.1  6.1  80    67 6.6    0      - - true 36    19    480   1300 true 170   150   3100 930
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c true 1.7  1.7  20    19 1.3    0      - - true 9.0  4.8  97   340 true 21   12   250 500
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true .18 .18 2.1  17 .0082 .16   - - true 3.1  1.8  64   240 error 6.7 3.6 84 290
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true .19 .19 1.6  17 .0082 0      - - true 3.0  1.7  57   240 error 6.2 3.3 110 300
ldv-memsafety/StructInitialization_true-valid-memsafety.c true .19 .19 1.9  17 .0082 0      - - true 2.9  1.6  40   240 unknown 6.4 3.4 100 300
ldv-memsafety/memset2_true-valid-memsafety.c true 2.2  2.2  24    19 .23   0      - - true 3.2  1.8  39   240 true 9.8 5.3 160 350
ldv-memsafety/memset3_true-valid-memsafety.c true 2.2  2.2  22    19 .24   0      - - true 3.2  1.8  62   240 true 9.4 5.1 180 350
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true 2.2  2.2  22    19 .23   0      - - true 3.0  1.7  39   240 true 9.8 5.2 200 340
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 2.3  2.3  19    21 .24   2.3    - - true 3.5  1.9  44   240 true 9.2 5.1 150 350
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 2.2  2.2  24    19 .24   .19   - - true 3.0  1.7  43   240 true 11   5.8 140 350
ldv-memsafety/memset_true-valid-memsafety.c true 2.1  2.1  28    19 .24   0      - - true 3.1  1.7  58   240 true 11   6.2 120 350
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) .26 .25 2.3  26 .0082 0      error 5.7  3.0  85   310 true 14   7.7 260 380 - -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 1.5  1.5  15    28 .25   0      error 6.2  3.3  94   320 true 11   5.9 220 500 - -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 1.5  1.5  19    27 .25   .23   error 5.9  3.1  120   300 true 13   6.8 180 500 - -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 10    10    120    220 .0082 0      exception 4.3  2.3  63   270 true 14   7.4 290 380 - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 10    10    110    220 .0082 0      exception 4.3  2.4  64   250 true 16   8.6 250 390 - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) .25 .24 2.8  27 .0082 0      error 6.6  3.5  120   310 true 36   26   1100 590 - -
ldv-memsafety/memleaks_test12_false-valid-free.i error (1) .37 .36 3.9  36 .0082 0      error (invalid witness file) .48 .32 8.6 39 error (invalid witness file) 6.2 3.2 110 300 - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 1.6  1.6  17    53 .21   0      error 6.5  3.4  120   310 out of memory 67   40   1400 7000 - -
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) .21 .22 2.0  23 .0082 2.3    error 7.1  3.8  63   320 false(valid-free) 15   8.1 320 420 - -
ldv-memsafety/memleaks_test2_false-valid-free.i false(valid-free) .21 .21 1.6  23 .0082 2.3    error 5.3  2.8  96   280 true 9.5 5.1 210 350 - -
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) .22 .21 1.7  21 .0082 0      error 6.2  3.3  87   310 false(valid-free) 7.8 4.2 140 320 - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) .23 .22 1.8  21 .0082 0      error 5.7  3.1  110   320 false(valid-free) 11   6.2 240 370 - -
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) .20 .19 2.0  20 .0082 0      error 5.7  3.1  98   320 false(valid-free) 12   6.1 220 360 - -
ldv-memsafety/memleaks_test10_false-valid-memtrack.i false(valid-memtrack) .25 .25 2.3  22 .0082 0      error 5.6  3.0  84   300 true 10   5.3 220 340 - -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i false(valid-memtrack) .26 .26 2.5  25 .0082 0      error 5.7  3.1  110   300 true 9.7 5.1 160 330 - -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i false(valid-memtrack) .20 .19 2.0  21 .0082 0      error 7.0  3.8  64   310 true 9.8 5.2 110 320 - -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-memtrack) .29 .33 2.6  35 .0082 11      error 5.8  3.1  120   310 true 10   5.5 140 320 - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i false(valid-memtrack) .22 .23 1.9  23 .0082 2.4    error 5.6  3.0  100   310 true 8.0 4.2 160 330 - -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-memtrack) .23 .23 3.0  24 .0082 0      error 6.7  3.6  85   310 true 8.8 4.7 160 350 - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) .21 .21 2.8  21 .0082 0      error 6.7  3.6  97   310 true 8.6 4.6 160 330 - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i false(valid-memtrack) .23 .23 1.7  21 .0082 0      error 5.9  3.2  60   270 true 7.8 4.2 160 320 - -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i false(valid-memtrack) .21 .21 1.8  20 .0082 0      error 6.7  3.6  52   290 true 7.6 4.0 160 310 - -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(valid-memtrack) 2.2  2.1  21    67 .29   0      error 6.7  3.5  130   290 true 10   5.3 210 470 - -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 1.9  1.9  20    55 .23   0      error 5.8  3.1  120   280 true 9.5 5.0 170 390 - -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i false(valid-memtrack) .24 .23 2.3  24 .0082 0      error 5.6  3.0  95   310 true 8.3 4.4 170 330 - -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i false(valid-memtrack) 1.5  1.5  15    42 .16   0      error 6.5  3.5  120   320 true 9.4 5.0 150 320 - -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i false(valid-memtrack) 1.0  1.0  12    27 .14   .25   error 6.6  3.5  130   330 true 8.4 4.5 180 330 - -
ldv-memsafety/memleaks_test1_false-valid-memtrack.i false(valid-memtrack) .19 .19 1.8  20 .0082 0      error 5.6  3.0  100   310 true 7.4 3.9 150 320 - -
ldv-memsafety/memleaks_test20_false-valid-memtrack.i false(valid-memtrack) .21 .21 1.7  21 .0082 0      error 5.2  2.8  88   290 true 7.6 4.0 150 320 - -
ldv-memsafety/memleaks_test21_false-valid-memtrack.i false(valid-memtrack) .22 .22 1.7  21 .0082 0      error 5.1  2.7  68   300 true 7.3 3.9 150 320 - -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i false(valid-memtrack) 1.5  1.5  14    25 .22   0      error 6.7  3.6  85   310 true 11   5.7 200 490 - -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i false(valid-memtrack) 1.4  1.4  15    24 .17   .13   error 6.0  3.2  110   300 true 11   5.7 210 470 - -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i false(valid-memtrack) 1.5  1.5  14    27 .22   0      error 6.1  3.3  100   300 true 11   5.9 200 510 - -
ldv-memsafety/memleaks_test4_false-valid-memtrack.i false(valid-memtrack) .20 .20 1.7  21 .0082 .16   error 5.4  2.9  98   290 true 7.5 4.0 140 320 - -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i false(valid-memtrack) .19 .19 1.7  21 .0082 0      error 4.7  2.6  90   270 true 7.0 3.8 140 320 - -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i false(valid-memtrack) .20 .19 1.7  21 .0082 0      error 5.0  2.7  70   270 true 8.3 4.4 160 340 - -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i false(valid-memtrack) .24 .23 1.7  21 .0082 0      error 5.4  2.9  98   310 true 9.8 5.2 100 330 - -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i false(valid-memtrack) .19 .19 1.9  21 .0082 0      error 5.4  2.9  74   290 true 8.0 4.2 160 320 - -
ldv-memsafety/memleaks_test7_false-valid-memtrack.i false(valid-memtrack) .23 .27 2.4  33 .0082 13      error 5.7  3.1  90   320 true 8.3 4.4 150 330 - -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i false(valid-memtrack) .21 .21 1.6  21 .0082 .16   error 6.1  3.3  120   320 true 7.3 3.9 150 330 - -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i false(valid-memtrack) .21 .21 2.0  21 .0082 0      error 4.9  2.6  97   270 true 7.7 4.1 150 320 - -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i false(valid-memtrack) .20 .20 2.2  21 .0082 0      error 5.9  3.1  82   310 true 8.4 4.5 120 330 - -
ldv-memsafety/memleaks_test10_true-valid-memsafety.i true .44 .44 5.1  23 .016  0      - - true 5.2  2.8  81   260 timeout 960   930   32000 860
ldv-memsafety/memleaks_test11_true-valid-memsafety.i true .49 .48 4.4  26 .016  .16   - - true 5.5  3.0  76   260 timeout 960   910   33000 930
ldv-memsafety/memleaks_test12_true-valid-memsafety.i error (1) .36 .35 4.7  36 .0082 0      - - error (invalid witness file) .52 .34 9.2 39 error (invalid witness file) 6.7 3.6 86 300
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true .47 .51 4.6  38 .016  12      - - true 5.2  2.8  110   260 true 810   780   17000 1100
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true .44 .43 6.1  26 .016  0      - - true 5.9  3.1  80   260 true 200   170   3900 1100
ldv-memsafety/memleaks_test15_true-valid-memsafety.i error (1) .24 .23 2.4  23 .0082 0      - - error (invalid witness file) .48 .30 6.9 39 error (invalid witness file) 7.2 3.8 120 310
ldv-memsafety/memleaks_test16_true-valid-memsafety.i true .38 .38 3.4  21 .016  0      - - true 5.4  2.9  110   260 true 16   8.6 170 430
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i true 3.2  3.2  37    66 .35   .10   - - true 8.5  4.5  86   290 timeout 960   930   19000 1900
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i error (134) 580    580    4500    14000 .40   .10   - - error (invalid witness file) .54 .33 10   39 error (invalid witness file) 6.9 3.6 89 300
ldv-memsafety/memleaks_test18_true-valid-memsafety.i true 2.1  2.1  19    41 .21   .13   - - true 7.0  3.7  140   280 timeout 960   920   25000 970
ldv-memsafety/memleaks_test19_true-valid-memsafety.i true .40 .40 3.5  21 .016  0      - - true 5.0  2.7  67   250 true 230   200   5500 830
ldv-memsafety/memleaks_test1_true-valid-memsafety.i true .36 .36 3.8  21 .016  .19   - - true 4.6  2.5  86   260 true 11   6.0 190 370
ldv-memsafety/memleaks_test20_true-valid-memsafety.i true .36 .36 3.4  21 .016  0      - - true 5.0  2.7  50   260 true 15   8.5 260 460
ldv-memsafety/memleaks_test21_true-valid-memsafety.i true .40 .43 3.7  33 .016  13      - - true 5.2  2.8  110   260 true 14   8.0 190 430
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i true 1.7  1.7  19    26 .21   0      - - true 5.3  2.8  94   260 true 330   290   8000 1000
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i true 1.9  1.9  17    28 .27   0      - - true 6.1  3.2  88   290 timeout 960   910   21000 2600
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i true 1.8  1.8  16    28 .27   0      - - true 5.5  3.0  89   260 timeout 960   900   18000 2300
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i error (42) 850    850    5900    10000 8.6    0      - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 7.5 4.0 87 310
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i error (42) 850    850    6900    10000 8.0    .10   - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.7 3.0 110 300
ldv-memsafety/memleaks_test2_true-valid-memsafety.i true .38 .37 3.3  21 .016  0      - - true 5.2  2.8  51   260 true 13   6.9 150 360
ldv-memsafety/memleaks_test3_true-valid-memsafety.i true .38 .37 3.3  21 .016  0      - - true 4.8  2.6  75   260 true 11   6.3 220 360
ldv-memsafety/memleaks_test4_true-valid-memsafety.i true .38 .38 3.3  21 .016  .19   - - true 4.9  2.6  63   260 true 17   9.7 200 490
ldv-memsafety/memleaks_test5_true-valid-memsafety.i true .36 .36 4.3  21 .016  0      - - true 4.5  2.5  53   250 true 13   7.1 210 420
ldv-memsafety/memleaks_test6_true-valid-memsafety.i true .37 .36 3.1  21 .016  0      - - true 5.4  2.9  43   290 true 170   160   4500 660
ldv-memsafety/memleaks_test7_true-valid-memsafety.i true .36 .36 3.7  21 .016  0      - - true 4.8  2.6  89   260 true 86   76   2800 600
ldv-memsafety/memleaks_test8_true-valid-memsafety.i true .40 .39 3.3  21 .016  0      - - true 4.9  2.6  62   290 true 13   7.2 160 370
ldv-memsafety/memleaks_test9_true-valid-memsafety.i true .39 .39 3.0  21 .016  0      - - true 4.7  2.5  100   260 true 13   7.2 180 380
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i true .36 .35 2.8  18 .016  0      - - true 3.2  1.8  53   240 unknown 8.3 4.4 90 320
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety.i true .63 .62 6.0  19 .053  0      - - true 3.4  1.9  70   250 unknown 6.6 3.5 130 310
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety.i true .71 .71 5.3  21 .057  .23   - - true 3.2  1.8  33   240 unknown 7.8 4.1 81 300
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety.i true .93 .93 9.5  19 .098  0      - - true 3.1  1.7  40   240 unknown 7.4 3.9 75 300
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety.i true 1.0  1.0  9.1  19 .11   0      - - true 3.2  1.8  52   240 unknown 7.1 3.7 150 320
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) .18 .17 1.8  18 .0082 0      error 3.2  1.8  75   250 unknown 6.0 3.2 130 300 - -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i false(valid-deref) .50 .49 4.4  19 .037  0      error 3.2  1.8  71   250 unknown 7.5 3.9 130 320 - -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i false(valid-deref) .86 .85 7.6  19 .082  0      assertion 3.3  1.8  69   260 unknown 6.5 3.5 130 300 - -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) .78 .77 11    19 .086  0      assertion 4.2  2.3  51   250 unknown 6.7 3.6 120 310 - -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i false(valid-free) .49 .48 5.1  19 .041  0      error 3.3  1.9  67   250 unknown 6.4 3.4 120 320 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (1) .30 .29 2.4  21 .0082 0      - - error (invalid witness file) .54 .35 11   43 error (invalid witness file) 6.9 3.6 98 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 850    850    9100    3300 6.8    0      - - error (invalid witness file) .65 .41 9.0 40 error (invalid witness file) 6.0 3.2 110 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 400    400    3700    13000 6.7    .18   - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.4 3.3 120 290
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 850    850    4500    4300 1.7    0      - - error (invalid witness file) .50 .32 7.7 39 error (invalid witness file) 6.2 3.3 96 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) .47 .46 4.5  36 .0082 .19   error 4.8  2.6  100   260 timeout 96   54   1300 6300 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) .44 .43 4.9  37 .0082 .16   error 5.2  2.8  110   300 false(valid-deref) 9.1 4.9 200 320 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .30 .30 2.5  26 .0082 0      error 5.2  2.8  110   270 true 9.1 4.9 180 330 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) .40 .39 4.5  33 .0082 0      assertion 5.0  2.7  48   260 error 11   5.9 230 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .29 .28 2.9  27 .0082 0      assertion 4.1  2.3  80   260 true 9.1 4.9 150 340 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .27 .27 2.5  25 .0082 0      assertion 4.3  2.4  63   270 true 8.9 4.8 170 340 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 850    850    4900    4400 2.9    0      - - error (invalid witness file) .51 .33 5.1 39 error (invalid witness file) 7.1 3.8 98 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .24 .24 1.8  20 .0082 0      assertion 4.3  2.3  90   260 true 8.8 4.7 160 320 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .65 .64 5.0  24 .10   .19   error 8.3  4.4  70   280 true 11   5.8 220 450 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .28 .27 2.6  26 .0082 0      assertion 4.1  2.3  75   250 true 9.6 5.0 180 330 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .22 .22 1.6  19 .0082 0      assertion 3.9  2.2  52   260 true 7.7 4.1 160 320 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .23 .22 1.5  22 .0082 0      assertion 4.0  2.2  79   260 true 8.3 4.4 170 330 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) .26 .25 2.0  25 .0082 0      assertion 4.7  2.6  75   270 true 9.3 5.0 150 340 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 49    49    580    930 6.1    0      - - true 12    6.2  220   350 true 320   240   7600 2200
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 43    43    480    910 5.4    0      - - true 10    5.2  130   320 true 310   220   4200 1700
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 48    48    530    920 5.8    0      - - true 12    6.1  180   320 true 290   210   5400 2000
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 38    38    430    1100 1.8    0      exception 5.5  2.9  92   230 true 15   8.3 320 480 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    470    1100 1.7    .10   exception 5.8  3.1  83   220 true 16   8.6 240 490 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 38    38    510    1100 1.8    .10   exception 5.5  3.0  89   220 true 15   8.2 310 480 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    460    1100 1.7    .29   exception 5.5  2.9  91   220 true 15   8.3 300 480 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    450    1100 1.8    0      exception 5.5  2.9  93   220 true 17   9.1 310 480 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    440    1100 1.8    .27   exception 5.5  2.9  110   220 true 16   8.7 340 480 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    470    1100 1.8    0      exception 5.5  2.9  110   220 true 18   9.4 270 490 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    510    1100 1.8    0      exception 5.4  2.9  100   220 true 16   8.6 320 490 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    460    1100 1.8    0      exception 5.3  2.8  100   220 true 17   9.3 260 480 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 39    39    420    1100 1.9    .10   exception 6.7  3.5  76   230 true 16   8.5 330 480 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (42) 850    850    7900    3900 8.9    .19   - - error (invalid witness file) .51 .33 9.6 40 error (invalid witness file) 8.0 4.2 87 310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 340    340    3900    15000 14      0      - - error (invalid witness file) .54 .35 12   41 error (invalid witness file) 7.3 3.8 81 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (1) 98    98    1100    400 4.4    0      - - error (invalid witness file) .53 .34 10   41 error (invalid witness file) 7.6 4.0 80 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (42) 850    850    4200    2300 2.4    0      - - error (invalid witness file) .48 .31 5.3 40 error (invalid witness file) 6.9 3.6 91 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 850    850    5300    3100 2.1    0      - - error (invalid witness file) .52 .33 10   42 error (invalid witness file) 6.4 3.4 110 320
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 850    850    6100    3300 2.1    0      - - error (invalid witness file) .48 .32 8.4 40 error (invalid witness file) 6.7 3.5 130 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (42) 850    850    6000    5400 5.1    .10   - - error (invalid witness file) .59 .38 8.3 40 error (invalid witness file) 5.4 2.9 120 290
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 850    850    5500    1000 3.6    .32   - - error (invalid witness file) .70 .45 9.9 39 error (invalid witness file) 5.8 3.1 120 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (42) 850    850    11000    890 3.5    0      - - error (invalid witness file) .49 .32 7.1 41 error (invalid witness file) 7.1 3.8 120 310
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (42) 850    850    11000    720 8.5    .19   - - error (invalid witness file) .50 .33 7.8 40 error (invalid witness file) 7.3 3.8 88 310
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (42) 850    850    6400    880 1.2    0      - - error (invalid witness file) .50 .33 6.8 41 error (invalid witness file) 5.8 3.1 120 310
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 320    320    3900    15000 12      0      - - error (invalid witness file) .51 .33 9.7 39 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (1) 94    94    930    390 4.1    .10   - - error (invalid witness file) .48 .30 7.5 39 error (invalid witness file) 6.3 3.3 130 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (42) 850    850    3600    1800 2.0    0      - - error (invalid witness file) .50 .32 7.0 40 error (invalid witness file) 7.0 3.7 87 310
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 850    850    5600    2100 2.5    .10   - - error (invalid witness file) .51 .33 9.1 40 error (invalid witness file) 6.9 3.6 110 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 850    850    5100    2300 2.4    .10   - - error (invalid witness file) .56 .37 9.8 39 error (invalid witness file) 6.7 3.5 110 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (42) 850    850    5800    2400 4.2    0      - - error (invalid witness file) .62 .40 6.2 40 error (invalid witness file) 7.2 3.8 100 310
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 850    850    7800    870 6.5    .19   - - error (invalid witness file) .51 .31 8.7 41 error (invalid witness file) 6.7 3.5 130 320
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (42) 850    850    10000    910 2.9    0      - - error (invalid witness file) .65 .41 8.1 41 error (invalid witness file) 6.4 3.4 110 320
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) .37 .36 3.6  31 .0082 0      assertion 4.5  2.5  91   260 false(valid-deref) 13   6.7 250 470 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) .25 .25 2.9  23 .0082 .19   assertion 4.5  2.4  84   260 false(valid-deref) 29   16   580 890 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) .29 .28 2.7  26 .0082 0      assertion 4.6  2.5  86   260 false(valid-deref) 13   6.9 260 460 - -
loop-acceleration/array3_false-valid-deref.i false(valid-deref) 23    23    290    930 20      0      timeout 94    59    1600   4300 out of memory 81   51   1400 7000 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 3.5  3.5  34    200 .012  .23   error 12    6.0  180   380 unknown 7.4 3.9 140 300 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c error (1) .68 .67 7.7  35 .012  0      error (invalid witness file) .64 .42 6.8 39 error (invalid witness file) 6.9 3.6 140 300 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.1  1.1  11    38 .0082 0      - - true 37    21    510   2500 true 20   11   320 460
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.1  1.1  12    38 .0082 .16   - - true 35    20    400   2300 true 19   11   240 470
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error (42) 850    850    3700    7400 6.1    0      - - error (invalid witness file) .51 .33 6.9 39 error (invalid witness file) 7.2 3.8 77 290
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .37 .36 4.0  20 .0082 0      - - true 45    27    760   2600 true 12   6.3 190 440
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .36 .36 3.8  21 .0082 0      - - true 45    27    440   2700 true 11   6.1 190 430
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .61 .61 6.8  22 .0082 0      - - true 82    52    1300   3500 true 15   7.8 240 470
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .62 .61 6.4  22 .0082 0      - - true 76    47    1100   3500 true 14   7.7 210 470
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .25 .25 2.9  18 .0082 0      - - true 9.8  5.1  140   400 true 9.2 4.9 180 330
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .34 .33 3.1  20 .0082 0      - - true 23    12    170   1000 true 12   6.2 200 390
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .32 .31 3.2  20 .0082 0      - - true 20    10    250   1000 true 13   6.8 140 390
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    6100    3100 15      0      - - error (invalid witness file) .56 .35 11   39 error (invalid witness file) 6.2 3.3 100 300
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    5000    3700 16      0      - - error (invalid witness file) .64 .40 8.9 40 error (invalid witness file) 6.0 3.2 110 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    8000    4300 18      0      - - error (invalid witness file) .54 .34 10   40 error (invalid witness file) 7.2 3.8 85 310
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    7000    2000 20      0      - - error (invalid witness file) .51 .33 9.7 40 error (invalid witness file) 6.5 3.4 120 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    6900    1800 8.9    0      - - error (invalid witness file) .47 .30 7.2 39 error (invalid witness file) 7.4 3.9 79 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    7700    1500 21      0      - - error (invalid witness file) .51 .33 5.5 39 error (invalid witness file) 6.7 3.5 110 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    6800    2000 9.5    0      - - error (invalid witness file) .66 .41 9.5 43 error (invalid witness file) 5.9 3.1 110 300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    6400    1800 22      12      - - error (invalid witness file) .49 .31 9.4 39 error (invalid witness file) 6.5 3.4 130 310
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    6100    5500 20      0      - - error (invalid witness file) .52 .33 14   39 error (invalid witness file) 5.8 3.1 110 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    5700    1300 22      .0041 - - error (invalid witness file) .48 .31 9.1 39 error (invalid witness file) 7.0 3.6 98 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    6000    1700 11      0      - - error (invalid witness file) .61 .39 7.7 39 error (invalid witness file) 6.3 3.4 100 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    5300    2000 12      0      - - error (invalid witness file) .49 .32 7.0 40 error (invalid witness file) 7.3 3.8 90 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 850    850    5000    2600 13      0      - - error (invalid witness file) .49 .33 9.6 40 error (invalid witness file) 6.0 3.2 82 290
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 328 76000 76000 570000 750000 710 180 328 770 430 13000 41000   328 2100 1200 38000 98000   328 4000 3400 70000 62000   328 19000 17000 460000 91000  
    correct results 193 1900 1900 20000 24000 110 89 6 770 420 13000 40000   113 2000 1100 36000 94000   63 3900 3300 68000 57000   43 18000 16000 440000 54000  
        correct true 66 1300 1300 12000 6900 49 29 5 0 0 0 0   70 0 0 0 0   63 3900 3300 68000 57000   43 18000 16000 440000 54000  
        correct false 127 650 640 7500 17000 65 60 1 770 420 13000 40000   43 2000 1100 36000 94000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (328 tasks, max score: 517) 259
Run set [sv-comp17.MemSafety-Arrays; sv-comp17.MemSafety-Heap; sv-comp17.MemSafety-LinkedLists; sv-comp17.MemSafety-Other]