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