Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 PeSCo 1.7-svn b8d6131600+ PredatorHP 3.14 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:20:21 CET 2018-12-06 12:44:04 CET 2018-12-07 04:08:42 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET
Run set 2ls.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] cbmc.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] cbmc-path.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] cpa-seq.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] depthk.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] divine-explicit.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] divine-smt.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] esbmc-kind.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] map2check.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] pesco.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] predatorhp.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] smack.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] symbiotic.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] uautomizer.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] ukojak.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] utaipan.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup]
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --witness error-witness.graphml -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
array-memsafety/add_last_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .17  26 1.5  .11  7.1 .77 .056 8.7 .55 3.7 280 32 .22 34 2.2 8.5   450   100    1.6   200   22     .14  27   1.7   .47 83 5.4 3.6  280 31   .17 36 1.1 3.3  82 38   .21  18 2.4  8.3 340 66 9.0 370 70 9.5 370 77
array-memsafety/bubblesort_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .090 24 .68 .11  7.2 .37 .11  7.4 .44 960   12000 9700 .14 33 1.7 8.2   430   96    8.8   430   110     .084 26   .81  .48 83 5.2 920    12000 8700   .15 34 1.5 3.3  86 44   .18  19 2.1  6.8 330 58 9.1 370 68 8.3 370 57
array-memsafety/count_down_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .18  26 1.4  .11  7.5 .99 .061 8.8 .58 3.9 280 36 .22 34 2.2 8.4   450   100    1.6   200   19     .12  30   2.0   .47 83 5.8 3.6  270 32   .16 35 1.6 3.3  83 41   .21  17 2.9  9.5 380 65 8.9 360 68 9.4 380 72
array-memsafety/cstrcat_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .083 24 .66 .064 7.1 .58 .098 6.9 .29 2.7 250 23 .14 33 1.7 8.3   430   110    8.3   430   110     .086 26   1.2   .52 83 5.9 2.7  250 23   .15 33 2.0 3.3  87 40   .15  15 1.7  7.7 360 60 7.9 370 68 7.6 350 57
array-memsafety/cstrchr_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .17  26 1.4  .078 7.5 .95 .069 8.7 .58 3.6 280 34 .20 34 2.3 8.3   450   120    1.6   200   22     .13  27   1.9   .48 83 5.1 3.7  280 34   .27 48 1.7 3.4  85 48   .95  17 12    14   570 130 11   460 86 16   590 130
array-memsafety/cstrlen_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .17  26 1.5  .091 7.7 .60 .10  7.1 .49 3.8 280 33 .55 36 6.6 8.4   440   110    1.6   200   23     .17  27   1.9   39    1100 450   3.7  280 34   .14 36 1.4 3.4  85 45   .31  18 3.1  11   440 87 9.4 360 76 11   430 81
array-memsafety/cstrncat_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .089 24 .83 .067 7.1 .61 .078 6.8 .31 2.6 250 27 .15 33 1.6 8.1   430   110    8.3   430   100     .084 26   .97  .44 83 6.4 2.9  250 26   .26 48 1.5 3.2  82 38   .17  16 1.7  7.8 360 63 8.8 370 72 7.9 370 62
array-memsafety/cstrncpy_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .084 24 .74 .068 8.0 .72 .059 7.5 .51 2.8 250 27 .14 33 1.6 8.4   430   110    8.5   430   93     .084 26   .78  .46 83 5.4 2.8  250 25   .16 33 1.4 3.3  83 46   .17  18 2.4  7.3 350 63 7.7 350 59 7.3 350 58
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .17  26 1.7  .10  7.5 1.0  .073 7.4 .59 3.5 250 32 .22 34 2.6 8.5   440   120    1.6   200   20     .18  27   1.9   .47 83 5.3 3.7  280 31   .27 49 2.0 3.7  88 53   .76  18 10    23   570 240 13   560 110 23   520 260
array-memsafety/diff_usafe_false-valid-deref.i valid-deref valid-free valid-memtrack .084 24 .71 .074 7.3 .67 .075 7.2 .56 840   9300 7500 .14 33 1.6 8.1   430   97    8.5   430   120     .086 26   .86  .45 83 5.9 900    9900 11000   .17 36 1.4 3.3  84 39   .19  18 2.0  8.2 370 67 8.6 360 65 8.0 370 70
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .17  26 1.7  .65  74   8.2  .086 8.3 .96 4.0 290 35 .28 34 3.9 8.4   440   110    1.6   200   20     .23  27   2.4   .47 83 6.4 3.7  280 36   .23 49 1.9 3.5  89 39   .25  18 4.3  10   390 70 10   370 79 9.6 380 81
array-memsafety/lis_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .18  26 1.5  .11  7.5 .94 .11  7.3 .88 3.7 280 34 .22 34 2.6 8.3   450   120    1.6   200   21     .16  27   2.1   900    1700 9200   3.6  280 33   .15 36 1.3 3.6  120 54   .40  18 5.3  12   480 110 27   810 250 14   510 120
array-memsafety/mult_array_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .17  26 1.4  .14  15   1.5  .064 7.4 .55 3.6 280 29 .40 38 4.9 8.4   450   110    1.6   200   21     .20  29   2.4   .48 83 5.2 3.7  280 33   19    15000 200   3.4  86 42   .31  21 3.8  9.6 380 72 8.7 360 66 9.9 380 78
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .16  26 1.5  .28  29   3.0  .11  7.5 .64 3.4 250 32 .64 36 8.0 8.5   450   91    1.6   200   21     .23  27   2.5   .46 82 4.9 3.6  270 30   .16 36 2.7 3.4  87 43   .54  18 8.0  11   400 76 12   480 98 9.9 390 81
array-memsafety/reverse_array_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .16  26 1.9  .24  29   2.8  .062 8.3 .61 3.8 280 30 .20 34 2.3 8.3   450   120    1.6   200   21     .16  27   1.5   .44 83 5.6 3.6  250 34   .15 34 1.5 3.3  87 47   .23  18 3.0  10   370 75 8.5 340 63 9.9 390 78
array-memsafety/selectionsort_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .086 24 .70 .065 7.1 .66 .058 7.0 .53 630   7600 6700 .14 33 2.0 8.1   430   98    8.7   430   110     .086 26   .87  .48 83 5.1 900    8900 8300   .16 35 1.5 3.3  84 45   .19  17 1.9  8.0 360 60 8.1 330 65 7.1 330 56
array-memsafety/stroeder1_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack .089 24 .76 .077 7.4 .33 .069 6.7 .30 2.8 250 27 .14 34 1.9 8.2   430   120    1.6   200   20     .078 26   1.1   .45 82 5.5 2.8  250 25   .17 35 1.4 3.3  83 34   .18  18 2.3  7.9 360 69 7.5 350 63 7.8 350 56
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.5  710     13000   6100    880     830   10000    3.6 280 35 900    190 12000   8.5   440   120    1.6   200   23     900     460   12000     12    74 170   3.8  280 30   19    15000 210   760    370 7300   .22  19 2.4  900   1000 7700 900   860 7700 900   2500 14000
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.7  830     14000   8900    870     3800   12000    3.6 280 31 900    260 12000   8.3   450   90    1.5   200   22     900     660   12000     230    75 3200   3.6  260 32   19    15000 210   760    550 7600   900     1400 12000    11   450 77 15   660 130 10   450 94
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .15  26 1.9  270     13000   3000    880     11000   12000    3.6 280 31 900    240 13000   8.4   450   100    1.6   200   18     900     530   12000     900    75 9400   3.6  270 32   19    15000 210   760    670 9300   900     6400 13000    11   490 92 15   570 130 12   500 93
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  26 1.8  190     14000   2100    880     5600   12000    3.8 280 31 900    770 11000   8.2   450   91    1.6   200   22     900     1200   11000     350    75 4200   3.7  280 33   19    15000 200   760    460 10000   900     1300 10000    12   500 99 64   870 750 13   530 110
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.7  280     13000   3200    840     15000   13000    3.6 280 31 900    1100 9800   8.3   450   120    1.6   200   26     900     1300   10000     18    75 300   3.3  250 32   19    15000 220   760    670 5900   900     130 12000    11   460 87 22   730 170 11   410 89
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.6  850     14000   10000    880     9000   14000    3.6 270 31 900    220 13000   8.3   440   100    1.5   200   22     900     510   13000     900    650 8800   3.5  270 36   19    15000 200   760    230 9200   900     470 7500    13   520 110 34   860 380 14   560 120
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.5  110     14000   1100    .082 8.3 .48 3.5 260 31 300    70 4200   8.4   450   120    1.6   200   20     900     650   13000     900    180 12000   3.8  260 35   .32 49 2.4 760    330 7900   900     320 13000    900   2600 13000 900   870 8000 900   8200 5400
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.6  880     2800   11000    .057 7.9 1.0  3.5 270 32 130    42 1700   8.3   440   100    1.6   200   21     900     800   10000     76    90 1100   3.7  280 32   .17 35 1.3 760    220 8200   900     350 11000    13   500 100 25   610 250 15   610 130
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  26 1.3  880     3300   11000    .075 8.5 .57 3.5 250 35 230    75 3300   8.4   450   100    1.6   200   21     900     580   12000     34    75 440   3.8  280 30   .17 33 2.3 760    280 9700   900     470 11000    24   740 230 900   950 10000 35   780 330
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.8  120     13000   1200    .060 8.8 .57 3.4 250 33 150    46 2300   8.3   450   100    1.6   200   23     900     1400   11000     160    89 2200   3.7  280 31   .16 32 1.5 760    250 11000   900     300 13000    19   540 160 100   730 1100 19   650 160
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  26 1.3  880     4700   10000    .094 8.0 .56 3.8 280 37 900    190 12000   8.4   450   110    1.6   200   24     900     670   11000     30    75 380   3.6  280 32   .47 49 1.3 760    730 6900   900     380 13000    23   570 220 900   970 9200 160   760 2300
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.3  880     3400   5900    .062 8.3 .51 3.7 270 35 66    42 840   8.3   450   99    1.6   200   20     900     780   12000     16    75 200   3.6  280 31   .36 49 1.4 760    210 11000   900     390 11000    13   520 110 20   710 160 14   580 120
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.9  240     14000   2500    .11  7.6 .57 3.8 280 37 390    62 5200   8.3   450   81    1.6   200   21     900     580   11000     900    210 12000   3.8  280 33   .26 49 2.2 760    310 9400   900     140 9400    900   2100 11000 900   970 7300 900   2200 13000
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.4  880     3400   11000    .069 8.7 .55 3.7 280 35 300    67 4600   8.4   450   110    1.6   200   21     900     890   11000     900    98 11000   3.7  280 33   .28 33 2.1 760    310 7900   900     300 13000    28   780 300 140   760 1400 28   610 240
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .15  26 1.9  360     14000   3800    .067 8.5 .65 3.8 280 36 900    310 11000   8.4   450   110    1.6   200   23     900     3800   10000     43    74 540   3.7  280 35   .17 34 1.5 760    280 8900   900     340 9800    20   550 190 190   950 1700 25   710 190
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.8  880     4700   13000    .085 8.0 .40 3.8 280 31 900    180 12000   8.3   450   120    1.6   200   27     900     700   12000     30    75 410   3.7  280 31   .17 35 1.5 760    730 6300   900     400 11000    45   690 430 900   940 7600 33   820 280
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.8  880     4700   10000    .062 8.8 .72 3.7 280 37 900    180 11000   8.2   450   110    1.6   200   20     900     700   12000     31    75 430   3.7  260 34   .31 49 1.6 760    710 8300   900     390 14000    67   720 820 900   960 7800 61   960 640
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.5  880     12000   5000    880     14000   12000    3.7 280 32 900    200 12000   8.5   450   100    1.6   200   20     900     290   12000     41    75 500   3.9  280 34   20    15000 190   760    180 11000   900     1300 11000    22   670 200 900   1000 9600 20   690 180
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.3  460     14000   5400    870     2000   12000    3.6 270 36 900    270 13000   8.4   450   96    1.6   200   19     900     500   11000     14    75 220   3.7  280 32   19    15000 220   760    520 7800   900     1400 9800    15   510 130 27   630 290 17   650 150
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.4  270     13000   3800    830     15000   13000    3.6 270 34 890    790 9500   8.6   440   110    1.6   200   22     900     1300   10000     18    70 230   3.7  280 29   19    15000 200   760    540 7500   900     880 11000    12   490 100 90   740 790 12   560 98
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.9  800     14000   8800    840     15000   14000    3.8 280 34 900    640 12000   8.2   450   120    1.6   200   22     900     990   10000     18    75 280   3.8  280 40   31    15000 290   750    320 6400   900     460 12000    23   750 190 900   1100 6900 23   550 200
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.6  100     14000   830    880     260   11000    3.3 250 29 370    85 4900   8.4   450   120    1.6   200   22     900     2400   11000     900    2100 7000   3.8  280 35   20    15000 230   760    350 7500   900     1100 12000    23   470 280 130   590 1400 26   510 240
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.2  140     13000   1500    .10  7.5 .42 3.7 280 30 60    40 780   8.3   450   100    1.6   200   20     900     2200   12000     740    87 8600   3.8  280 31   .15 34 1.4 760    360 9700   900     330 10000    14   500 120 30   620 280 16   530 150
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.2  880     1900   9400    .058 8.6 .61 3.7 280 32 77    42 1100   8.4   450   100    1.5   200   23     900     1500   11000     310    180 4300   3.8  280 32   .15 36 1.5 760    390 11000   900     580 13000    14   550 120 900   720 10000 15   590 120
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.5  .079 7.2 .81 .12  6.8 .49 3.7 280 33 130    48 1800   8.5   440   110    1.6   200   20     900     310   12000     320    180 4300   3.7  280 34   .16 35 1.4 760    400 9900   900     270 12000    21   540 220 900   760 12000 17   640 160
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  26 1.5  150     13000   1500    .057 8.2 .55 3.6 280 29 58    40 690   8.3   450   130    1.6   200   23     900     2100   13000     180    130 2500   3.4  250 30   .15 35 1.5 760    400 9700   900     1400 11000    14   520 120 20   530 180 13   500 130
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.7  120     13000   1200    .057 7.8 .72 3.7 280 33 150    46 1800   8.3   450   120    1.5   200   22     900     1200   13000     160    88 2000   3.3  250 34   .17 35 1.3 760    260 8700   900     280 10000    17   500 150 45   730 430 26   590 250
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.7  360     14000   3400    .075 7.5 .48 3.8 280 35 900    310 10000   8.4   450   96    1.6   200   20     900     4000   10000     42    75 610   3.7  280 32   .20 36 1.4 760    260 9500   900     520 13000    46   870 400 900   940 10000 89   820 1100
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.5  110     14000   1100    .071 8.1 .59 3.9 280 31 300    75 3600   8.5   450   100    1.6   200   21     900     650   12000     900    180 12000   3.8  280 37   .21 36 2.0 760    320 7800   900     340 13000    900   2600 13000 900   990 8000 900   2200 11000
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .20  26 1.5  880     1800   9900    .089 7.7 .48 3.5 250 34 240    81 2900   8.3   450   92    1.6   200   22     900     830   11000     35    75 470   3.5  250 35   .17 36 2.3 760    270 8100   900     200 11000    26   570 230 190   980 1900 55   720 600
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.5  120     13000   1400    .088 7.6 .41 3.8 280 31 150    46 2000   8.2   450   92    1.6   200   19     900     1200   12000     160    88 1900   3.6  250 31   .29 49 1.7 760    260 9500   900     230 12000    16   520 140 55   940 530 18   680 150
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 2.6  870     310   3600    .092 8.0 .52 3.7 280 34 900    230 11000   8.4   450   110    1.6   200   20     900     1200   13000     48    75 670   3.8  280 31   .20 36 1.7 760    280 8400   900     420 11000    620   1200 9100 900   850 9600 900   1500 14000
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.5  880     8200   6000    .072 8.5 .52 3.6 280 32 900    110 12000   8.5   450   110    1.6   200   21     900     380   13000     41    75 550   3.8  280 38   .21 34 1.5 760    280 9700   900     370 11000    37   690 300 900   940 9300 41   840 400
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.7  880     3400   4400    .063 7.9 .49 3.5 270 28 66    40 850   8.5   450   100    1.6   200   21     900     780   13000     15    75 190   3.7  270 36   .14 34 1.2 760    210 10000   900     350 13000    13   590 96 22   710 160 14   600 120
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.4  230     14000   2400    .066 7.8 1.2  3.9 280 34 370    65 4700   8.2   440   110    1.6   200   18     900     640   11000     900    210 10000   3.8  280 33   .22 36 1.9 760    350 11000   900     140 10000    900   2300 12000 900   860 8900 900   2100 12000
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.6  880     3800   9600    .064 8.5 .58 3.6 280 34 260    75 4000   8.3   450   98    1.5   200   23     900     1200   11000     900    100 14000   3.7  280 31   .23 35 1.4 760    290 9200   900     310 11000    31   810 320 330   1000 3000 38   680 340
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.5  350     14000   4200    .10  7.4 .53 3.6 250 34 900    310 10000   8.4   450   100    1.6   200   20     900     4000   12000     41    75 570   3.7  280 33   .42 49 1.4 760    270 10000   900     490 14000    27   600 270 900   920 12000 31   760 300
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.4  880     1600   9000    .067 8.3 .50 3.7 280 34 71    41 890   8.4   450   100    1.6   200   19     900     810   13000     620    75 7400   3.8  280 33   .38 49 1.5 760    250 8900   900     370 11000    12   500 100 900   810 11000 13   580 110
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.6  880     260   7400    .067 7.7 .64 3.8 280 31 900    190 9700   8.5   450   110    1.6   200   19     900     720   12000     42    75 550   3.4  250 34   .19 36 1.6 760    680 7100   900     330 12000    30   580 380 900   860 8600 170   910 2000
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.7  880     1000   10000    .095 7.5 .56 3.7 280 37 900    160 10000   8.5   450   110    1.6   200   20     900     220   12000     59    75 870   3.7  280 31   .19 37 1.8 760    300 7300   900     360 11000    26   610 240 900   920 10000 35   820 340
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .21  26 1.4  880     4700   4500    .11  7.4 .56 3.8 280 35 900    240 11000   8.5   450   93    1.6   200   20     900     400   14000     53    75 770   3.6  250 31   .30 50 2.3 750    330 7300   900     310 12000    900   1200 11000 900   940 8500 900   1200 13000
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.5  880     5000   7500    .091 7.3 .44 3.7 270 34 .59 36 8.8 8.4   450   110    1.6   200   20     900     990   11000     21    75 290   3.6  280 36   .14 36 1.3 760    310 10000   900     570 11000    13   490 120 25   760 240 14   550 130
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.6  120     14000   1200    880     12000   11000    3.7 280 34 900    220 12000   8.4   450   100    1.6   200   24     900     360   14000     16    75 200   3.7  280 37   19    15000 190   760    510 6400   900     1100 11000    18   680 150 900   1300 11000 17   540 150
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.5  880     2500   3900    880     160   10000    3.9 280 32 78    52 940   8.4   450   110    1.6   200   20     900     3100   11000     15    75 220   3.7  280 30   19    15000 200   760    260 8900   900     1400 13000    11   500 80 13   570 97 12   520 92
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.4  240     13000   2400    870     3300   12000    3.7 280 36 900    160 11000   8.3   450   100    1.6   200   22     900     550   12000     15    74 230   3.4  250 32   20    15000 220   760    670 7400   900     1500 11000    12   510 94 20   550 170 12   490 110
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  26 1.4  880     11000   9300    .059 7.8 .54 3.7 280 33 900    230 12000   8.4   440   120    1.6   200   20     900     240   9500     210    140 3000   3.7  280 31   .17 35 2.2 760    160 9100   900     350 12000    18   600 160 900   610 11000 15   590 130
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  26 1.7  880     1200   4700    .071 8.2 .66 3.7 280 34 690    110 9000   8.3   450   110    1.6   200   21     900     250   13000     36    75 470   3.5  250 30   .17 35 1.4 760    240 8200   900     430 11000    36   640 420 220   770 2300 26   610 270
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.8  880     5300   9600    .088 9.1 .56 3.7 280 33 900    220 10000   8.4   450   100    1.6   200   20     900     780   10000     36    74 470   3.9  280 32   .18 35 1.3 760    710 5700   900     390 14000    230   870 2900 900   880 8000 200   1200 2900
array-examples/relax_false-valid-deref.i valid-deref valid-free valid-memtrack .16  26 1.8  .13  7.9 .76 .13  7.8 .83 3.5 250 33 .23 35 2.6 8.3   450   100    1.6   200   19     .17  27   1.8   320    4000 2800   3.8  280 32   .14 35 1.1 750    250 9400   .67  18 7.8  9.5 350 81 9.7 370 78 9.3 370 76
array-examples/sanfoundry_24_false-valid-deref.i valid-deref valid-free valid-memtrack .090 24 .73 880     4000   7900    180     15000   1900    900   4800 12000 90    71 1100   8.3   430   88    8.6   430   94     900     1000   8500     900    100 9800   900    4800 13000   900    4200 8700   7.5  100 100   900     1100 11000    900   1000 9100 900   1200 7800 900   860 8600
array-examples/standard_strcpy_false-valid-deref_ground.i valid-deref valid-free valid-memtrack .092 23 1.2  56     15000   750    200     15000   2300    900   5200 11000 66    55 800   8.0   430   110    8.2   430   100     900     220   13000     350    4300 4400   900    5200 12000   900    5500 8600   8.3  100 100   2.0   100 31    900   820 10000 900   1100 6600 900   1100 11000
array-examples/standard_strcpy_original_false-valid-deref.i valid-deref valid-free valid-memtrack .099 23 .57 57     15000   720    410     15000   6300    900   5200 12000 53    54 670   8.2   430   100    8.1   430   98     900     1100   11000     340    4300 3500   900    5200 12000   900    4200 9800   9.6  110 130   2.1   100 29    900   930 7800 900   1100 5600 900   980 9100
array-memsafety-realloc/array-realloc_false-valid-free.i valid-deref valid-free valid-memtrack .18  26 1.4  .11  8.0 1.3  .16  8.5 1.0  3.9 280 35 14    49 210   8.3   450   100    9.0   450   110     .16  26   1.5   .75 39 11   11    460 110   .19 35 1.4 760    290 9000   .24  17 2.3  12   450 92 13   520 130 11   420 82
array-memsafety-realloc/array-realloc_true-valid-memsafety.i valid-deref valid-free valid-memtrack .17  26 1.6  10     1300   140    .15  11   1.3  3.8 280 30 37    74 530   8.4   440   110    9.1   450   130     .16  27   1.7   .74 39 9.2 4.2  290 33   .18 37 1.5 880    240 9800   1.3   19 18    27   690 240 63   950 540 900   1000 12000
memsafety/960521-1_false-valid-deref.i valid-deref valid-free valid-memtrack .17  26 1.9  .84  30   11    3.2   34   44    11   700 85 74    63 970   8.6   450   100    8.6   450   98     5.3   110   82     .47 83 5.9 10    720 85   7.0  140 72   750    330 8600   .19  15 1.9  900   830 11000 900   1000 6700 900   910 10000
memsafety/test-0137_false-valid-deref.i valid-deref valid-free valid-memtrack .18  26 3.9  .27  22   3.5  .15  9.6 1.6  910   4700 8100 .20 34 2.2 8.5   450   110    8.7   450   110     .13  27   1.6   .51 83 6.5 910    4700 8400   .40 35 4.3 4.4  92 50   .25  18 2.7  13   330 100 13   360 110 13   340 110
memsafety/test-0235_false-valid-deref.i valid-deref valid-free valid-memtrack .31  27 2.9  58     2600   500    .13  11   1.8  900   5000 9000 .64 42 10   900     560   8900    900     560   9500     .56  33   7.9   .50 83 6.4 900    5000 8600   900    8200 11000   36    150 460   .33  18 4.4  900   2300 12000 900   890 12000 900   960 12000
memsafety/960521-1_false-valid-free.i valid-deref valid-free valid-memtrack .17  26 1.5  .91  30   11    4.8   45   62    11   720 95 74    62 1000   8.5   450   110    8.6   450   110     5.3   110   69     .43 82 6.1 11    730 110   7.0  170 80   750    330 8800   .18  16 2.4  900   1000 11000 900   1200 8300 900   1000 10000
memsafety/test-0158_false-valid-free.i valid-deref valid-free valid-memtrack .19  27 2.2  .13  9.2 .70 .087 9.0 .70 4.0 290 33 .21 34 2.7 8.2   450   99    8.3   450   89     .14  27   1.6   .46 82 6.4 4.1  280 32   .16 35 1.6 4.6  81 58   .18  16 1.8  10   390 75 13   610 120 10   400 76
memsafety/test-0232_false-valid-free.i valid-deref valid-free valid-memtrack 1.8   71 22    .12  8.1 1.2  .071 7.5 .97 900   4900 8600 .63 36 7.2 8.4   450   100    8.5   450   95     .30  28   4.2   900    160 9500   910    4800 7400   .36 50 1.3 760    270 6400   .22  17 2.7  500   1600 6000 900   950 8400 900   780 11000
memsafety/20020406-1_false-valid-memtrack.i valid-deref valid-free valid-memtrack .33  29 4.4  .15  8.9 1.9  .29  12   3.9  4.6 280 44 5.6  66 84   8.3   450   100    8.8   450   100     4.3   93   55     .54 83 6.1 4.6  290 43   .21 40 1.7 12    100 150   .24  17 2.6  900   2300 12000 900   1200 9000 900   1200 11000
memsafety/20051113-1.c_false-valid-memtrack.i valid-deref valid-free valid-memtrack .18  26 1.5  .22  7.5 3.5  1.9   20   25    4.1 280 34 1.4  36 21   8.5   450   100    8.3   450   120     .40  27   5.3   .45 83 5.5 4.3  280 37   .17 35 1.3 8.6  86 110   .18  15 2.1  900   910 11000 900   1100 7200 910   13000 5200
memsafety/lockfree-3.1_false-valid-memtrack.i valid-deref valid-free valid-memtrack 10     230 140    2.7   120   32    .076 8.5 .50 910   3500 7600 4.8  44 61   8.5   450   110    8.6   450   120     1.0   34   13     900    250 12000   910    5500 5300   .22 37 1.9 840    180 10000   .30  17 3.1  82   1000 670 900   1100 6200 110   1200 960
memsafety/lockfree-3.2_false-valid-memtrack.i valid-deref valid-free valid-memtrack 11     220 110    .096 7.5 1.0  .075 7.9 .54 910   5400 5900 .50 35 6.2 8.3   450   100    8.6   440   100     .16  27   1.6   900    240 10000   920    5700 4800   .17 36 1.7 840    180 11000   .23  17 2.8  23   560 200 25   580 200 24   590 210
memsafety/lockfree-3.3_false-valid-memtrack.i valid-deref valid-free valid-memtrack 10     220 100    2.7   120   35    .073 7.6 .49 920   5300 5900 18    68 220   8.8   450   100    8.7   450   110     4.9   74   59     900    240 11000   910    5400 6900   .20 37 2.1 750    160 8400   .58  26 8.3  130   2500 1200 900   1200 6000 180   4100 1800
memsafety/test-0019_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .18  26 2.0  .079 8.3 .69 .12  6.7 .66 3.7 270 34 .16 34 1.9 8.4   440   100    8.3   450   120     .13  26   1.2   .46 83 4.7 3.4  260 34   .15 35 1.7 6.3  110 75   .20  16 1.9  27   580 240 39   670 350 25   570 240
memsafety/test-0102_false-valid-memtrack.i valid-deref valid-free valid-memtrack .20  27 1.7  .18  11   2.2  .093 7.8 .85 900   4700 8300 4.1  63 56   8.5   450   110    8.8   440   120     49     190   560     .48 83 6.3 900    4700 9800   33    710 350   750    330 5500   .25  18 3.1  13   360 100 12   330 110 12   330 110
memsafety/test-0158_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .18  26 1.9  .060 7.0 .67 .064 7.5 .52 3.7 280 31 .15 34 1.6 8.3   450   110    8.3   450   94     .088 27   1.1   .45 83 5.4 3.4  260 34   .15 33 1.5 6.1  76 72   .16  15 1.9  16   340 120 18   380 150 15   340 120
memsafety/test-0220_false-valid-memtrack.i valid-deref valid-free valid-memtrack .18  27 1.8  .21  11   2.0  .094 8.7 .92 900   4800 7700 20    120 240   8.4   450   110    8.6   440   110     68     460   730     900    180 10000   910    4800 8000   .42 38 5.1 750    380 7900   .27  17 2.8  900   1700 12000 900   610 12000 900   1600 11000
memsafety/test-0232_false-valid-memtrack.i valid-deref valid-free valid-memtrack .99  51 12    .093 6.8 1.0  .11  7.0 .55 900   4900 6800 .17 34 1.8 8.3   450   110    8.5   450   100     .11  26   1.2   .49 83 4.5 900    4800 6900   .17 35 1.4 840    320 8400   .21  18 2.5  50   750 510 900   930 10000 58   750 660
memsafety/test-0234_false-valid-memtrack.i valid-deref valid-free valid-memtrack .21  27 2.2  6.4   310   82    .16  11   1.3  900   5000 8500 .49 41 6.1 900     570   8600    900     570   8000     .42  33   5.3   .49 83 7.7 900    5000 11000   3.7  130 40   750    390 7400   .29  18 3.0  900   2200 13000 900   640 12000 900   970 12000
memsafety/test-0235_false-valid-memtrack.i valid-deref valid-free valid-memtrack .27  27 2.8  12     580   150    .14  11   1.5  900   5000 11000 .53 41 5.7 900     570   9700    900     570   10000     .43  33   5.6   .53 83 6.1 900    4900 10000   3.7  130 46   750    380 9600   .32  18 4.2  900   2300 13000 900   770 11000 900   930 13000
memsafety/960521-1_true-valid-memsafety.i valid-deref valid-free valid-memtrack .16  26 1.7  93     15000   1300    880     14000   12000    910   8700 10000 72    64 1100   100     6100   1100    100     6100   1000     900     13000   10000     900    120 9600   900    8800 10000   900    6900 7900   770    210 8800   .62  23 9.3  900   1100 12000 900   1600 5900 900   770 11000
memsafety/lockfree-3.0_true-valid-memsafety.i valid-deref valid-free valid-memtrack 10     220 120    880     2000   6200    .090 8.0 .62 900   5400 7300 900    390 11000   900     7000   8000    900     7000   8400     900     710   12000     900    240 12000   920    5800 5900   37    240 340   880    180 12000   900     3700 6100    910   8600 7800 900   1200 6000 900   12000 7700
memsafety/test-0019_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  26 2.1  .097 6.9 .78 .13  8.0 1.6  3.5 270 30 .42 35 5.2 8.3   390   100    8.5   390   96     .12  26   1.8   120    4400 1500   3.6  280 32   .14 34 1.4 5.7  74 76   .14  15 1.5  21   670 170 900   1200 11000 18   520 160
memsafety/test-0102_true-valid-memsafety.i valid-deref valid-free valid-memtrack .19  26 2.2  880     4400   11000    .13  7.8 .81 900   4700 8700 900    770 9200   900     500   7900    900     500   7200     900     2400   12000     900    170 10000   900    4700 10000   .64 57 6.2 750    370 5900   900     2900 8200    13   330 94 13   350 100 12   340 94
memsafety/test-0134_true-valid-memsafety.i valid-deref valid-free valid-memtrack .19  26 1.6  880     2500   8200    650     15000   7200    900   4700 11000 900    1300 9200   8.4   450   100    8.6   450   82     900     2600   9800     900    190 11000   910    4700 9800   .74 62 6.7 750    360 6600   900     1500 15000    12   310 100 13   350 120 13   340 110
memsafety/test-0158_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.7  .091 7.1 1.1  .081 7.7 .79 3.6 270 31 .49 35 6.0 8.5   390   100    8.4   390   120     .16  26   2.0   320    4300 3200   3.7  280 33   .27 47 1.7 5.4  75 70   .13  16 1.5  10   390 87 13   560 130 10   390 76
memsafety/test-0214_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack .19  27 2.1  880     2100   8200    .10  9.3 1.2  900   5400 8400 900    6100 7300   900     570   9300    900     570   8400     .36  32   4.6   900    200 10000   910    5500 8100   .58 51 3.7 750    210 6300   230     82 2400    900   2100 12000 900   970 7500 900   13000 7500
memsafety/test-0217_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack .17  27 1.8  50     13000   620    .13  8.3 1.0  900   11000 8500 310    15000 3100   900     640   8400    900     670   8200     .87  82   10     900    220 11000   910    11000 7900   .46 38 5.3 750    290 7000   900     130 8600    900   2400 12000 900   1000 8500 900   3700 12000
memsafety/test-0218_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack .18  27 2.0  880     3900   11000    .11  9.0 1.0  950   11000 9900 260    15000 3300   900     640   8100    900     680   9000     .45  48   6.0   900    220 11000   970    11000 8500   .47 38 5.0 750    280 7800   900     260 12000    900   1100 12000 900   960 8900 900   1100 11000
memsafety/test-0219_true-valid-memsafety.i valid-deref valid-free valid-memtrack .18  27 2.2  880     920   6300    .098 8.4 .99 900   4800 8100 900    1600 10000   900     400   8700    900     400   8800     900     2900   9700     900    180 10000   900    4900 9900   .83 58 8.2 750    430 6500   900     2900 6700    900   2300 14000 900   610 12000 900   1200 12000
memsafety/test-0232_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.0   86 22    880     3300   11000    .075 7.5 .81 900   4900 7200 900    300 11000   900     420   9000    900     420   9500     900     660   10000     900    160 10000   900    4900 8900   .39 35 5.1 880    310 8100   900     940 11000    900   1300 11000 900   1000 10000 900   910 13000
memsafety/test-0234_true-valid-memsafety.i valid-deref valid-free valid-memtrack .23  27 2.1  880     1100   3900    .13  11   1.6  910   5000 11000 900    10000 7900   900     560   8900    900     560   8500     200     15000   2000     900    200 11000   910    4900 11000   .82 65 7.8 750    400 6800   900     2800 6700    900   2300 12000 900   840 13000 900   950 10000
memsafety/test-0235_true-valid-memsafety.i valid-deref valid-free valid-memtrack .29  27 2.8  880     2400   3500    .14  11   1.6  900   5000 11000 900    11000 5700   900     560   9800    900     560   8400     210     15000   2400     900    200 11000   900    5000 9700   3.9  160 38   750    390 7700   900     3000 7900    900   2200 12000 900   770 12000 900   12000 10000
memsafety/test-0236_true-valid-memsafety.i valid-deref valid-free valid-memtrack .23  27 2.3  880     1800   4400    .17  12   1.9  900   4800 9300 900    15000 10000   900     550   8400    900     550   8400     210     15000   2400     900    190 12000   900    4800 10000   .91 63 8.2 750    440 6800   900     2800 6400    900   2400 12000 900   630 14000 900   880 11000
memsafety/test-0237_true-valid-memsafety.i valid-deref valid-free valid-memtrack .23  27 2.7  880     1800   6700    .17  12   1.7  900   4700 11000 800    15000 8800   900     550   9500    900     540   9900     210     15000   3100     900    180 11000   900    4800 9700   .94 66 8.9 750    420 9400   900     2800 4800    900   1200 13000 900   800 12000 900   940 13000
memsafety/test-0504_true-valid-memsafety.i valid-deref valid-free valid-memtrack 190     1800 2200    880     1800   8200    .10  7.8 .60 900   11000 5700 900    570 14000   900     750   7100    900     700   8000     900     620   11000     900    160 11000   910    11000 6100   .72 37 8.9 750    330 6500   900     3200 8400    900   2200 12000 900   1000 6500 900   2100 14000
memsafety/test-0513_true-valid-memsafety.i valid-deref valid-free valid-memtrack 14     290 150    880     1900   10000    .088 8.0 .75 970   11000 5900 890    670 11000   8.5   450   100    8.6   450   100     900     930   11000     900    170 10000   910    11000 5600   .69 36 6.5 750    380 8900   900     1600 12000    900   2400 9400 900   1000 9100 900   900 12000
memsafety/test-0521_true-valid-memsafety.i valid-deref valid-free valid-memtrack 900     7100 10000    880     12000   9400    .13  8.2 .92 900   11000 5900 890    1000 9600   900     660   7600    8.7   450   110     900     1900   12000     900    170 10000   940    11000 6400   1.2  58 11   750    420 7200   900     3500 7100    900   2800 9700 900   910 11000 900   2200 12000
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  26 1.5  .16  6.8 1.1  .12  8.6 1.4  3.8 250 35 1.8  39 24   8.2   390   120    8.3   380   97     .65  29   8.0   180    4300 1900   3.6  250 32   .14 34 1.6 5.6  74 75   .16  15 2.1  900   970 9000 260   810 2500 900   940 11000
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.5   59 18    880     3800   12000    .080 7.4 .78 920   11000 6400 900    240 13000   900     600   8800    900     640   7600     900     400   11000     900    180 10000   910    11000 6500   900    890 5400   880    220 10000   900     3800 6800    900   1000 9600 900   890 7400 900   790 12000
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i valid-deref valid-free valid-memtrack 18     370 200    880     2500   6800    .13  8.7 1.3  970   12000 7400 900    160 13000   900     400   7300    900     400   8100     900     190   13000     900    230 10000   970    12000 7700   900    1800 8700   750    290 5600   900     3000 7900    900   1200 12000 900   1000 10000 900   950 13000
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i valid-deref valid-free valid-memtrack 130     1300 1300    870     2300   6600    .13  10   1.5  970   12000 7800 900    190 12000   900     420   7800    900     420   8100     900     250   11000     900    230 11000   970    11000 8000   900    1300 6600   750    350 7800   900     3000 7700    900   2300 12000 900   970 9800 900   880 13000
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack 26     500 240    880     1900   7000    .12  8.8 1.1  920   11000 6100 900    660 10000   900     1800   8300    900     1800   7800     900     800   11000     900    230 10000   930    11000 7000   900    440 5800   750    280 6800   900     190 12000    900   1200 14000 900   1000 8000 900   2100 12000
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack 900     5300 9400    880     2100   9400    .12  9.4 1.3  900   11000 7000 900    500 9900   900     2100   7600    900     2100   7300     900     1500   11000     900    230 12000   900    11000 6500   900    310 6300   750    290 5800   900     150 12000    900   1100 12000 900   930 7500 900   1000 12000
memsafety-ext/tree_of_cslls_true-valid-memsafety.i valid-deref valid-free valid-memtrack 260     3200 2100    880     9400   8900    .15  8.3 .96 940   11000 7100 900    650 10000   900     2700   9000    900     2500   8500     900     690   11000     900    170 10000   910    11000 7400   900    510 6900   750    320 6700   900     550 14000    900   2200 12000 900   1000 7400 900   860 10000
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack 54     900 550    880     1800   8500    .095 8.2 1.2  920   11000 6300 900    400 11000   900     1900   7700    900     1900   8400     900     920   12000     900    230 9800   910    11000 7000   900    480 6200   750    310 7200   900     230 12000    900   800 12000 900   1100 11000 900   1000 13000
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack 33     670 420    880     1800   6400    .11  8.9 1.4  920   11000 6000 900    430 11000   900     1800   8700    900     1800   8200     900     580   11000     900    230 11000   910    11000 6200   900    450 5300   750    310 7100   900     240 10000    900   2100 13000 900   920 7100 900   1500 10000
memsafety-ext2/split_list_test05_false-valid-deref.i valid-deref valid-free valid-memtrack 900     7400 11000    880     12000   9900    .19  9.3 1.3  900   11000 9100 160    15000 1900   8.6   450   100    900     420   8800     99     15000   1100     .49 83 6.4 900    12000 8900   900    1000 6400   750    420 9500   .90  38 12    900   2100 11000 900   1200 9600 910   13000 6600
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i valid-deref valid-free valid-memtrack .25  26 2.5  12     410   130    .11  8.8 1.4  4.6 290 40 900    1500 12000   8.7   450   110    8.5   450   110     900     1700   11000     900    200 11000   4.5  270 38   .33 49 1.8 750    430 6700   .27  18 3.5  900   950 12000 900   950 6300 900   1200 11000
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i valid-deref valid-free valid-memtrack .21  26 2.1  1.3   68   15    .12  10   1.5  970   11000 5900 900    2200 10000   8.2   450   100    8.6   450   120     900     4300   7500     900    160 12000   900    11000 6500   .19 38 1.5 750    430 6900   .32  18 4.2  900   1300 14000 900   1000 9800 900   1900 11000
memsafety-ext2/length_test03_false-valid-memtrack.i valid-deref valid-free valid-memtrack 130     1600 960    .83  20   11    .11  8.5 1.1  910   4800 7100 12    56 130   8.3   450   120    8.6   440   92     3.1   45   41     .46 83 6.2 900    4800 6600   .39 37 4.3 840    320 7200   .26  18 3.0  900   1500 12000 900   1000 8800 900   1800 12000
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i valid-deref valid-free valid-memtrack .17  26 1.7  10     120   120    .086 8.8 .77 900   5100 8300 900    360 10000   900     430   8100    8.6   450   99     900     480   12000     900    190 11000   900    5100 8400   .48 37 4.7 750    350 6500   .32  18 3.8  900   2300 13000 900   1000 9000 900   940 12000
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i valid-deref valid-free valid-memtrack .22  27 2.0  880     1500   8500    .12  9.2 1.2  900   6300 9900 900    1300 9200   8.4   450   99    8.6   450   120     900     1900   8700     900    180 10000   910    6400 9300   900    7200 9900   750    430 9300   900     3100 4600    900   960 11000 900   1000 7000 900   1300 11000
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i valid-deref valid-free valid-memtrack .21  26 2.3  880     1800   8700    .13  9.6 1.4  970   11000 6800 900    1800 10000   8.3   450   110    8.5   450   130     900     4000   8700     900    160 9700   920    11000 6400   900    2500 6800   750    460 8200   900     3100 8800    900   1300 14000 900   1100 8700 900   2000 11000
memsafety-ext2/length_test03_true-valid-memsafety.i valid-deref valid-free valid-memtrack 160     1700 1500    880     2200   9700    .12  8.6 .98 900   4900 6700 900    370 13000   900     420   8600    8.6   450   100     900     580   11000     900    170 9600   910    5000 6600   900    2600 12000   880    320 9200   900     1100 8700    900   2300 11000 900   1100 7100 900   2300 12000
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i valid-deref valid-free valid-memtrack .17  26 1.5  880     4900   8700    .11  7.3 .75 900   5100 7400 890    450 12000   900     430   8600    8.8   450   120     900     450   9900     900    190 12000   910    4200 9300   900    1900 4000   750    350 6100   900     3500 5300    900   2300 11000 900   990 6400 900   950 11000
memsafety-ext2/split_list_test05_true-valid-memsafety.i valid-deref valid-free valid-memtrack 900     7800 10000    880     11000   10000    .14  9.0 1.4  950   11000 8600 150    15000 1700   8.5   450   100    900     420   9500     97     15000   1300     900    160 10000   920    11000 9200   900    1000 7700   750    380 7300   900     3400 6400    900   1600 9000 900   1200 7100 900   990 11000
list-ext-properties/960521-1_1_false-valid-deref.i valid-deref valid-free valid-memtrack .18  26 1.8  .10  8.7 1.1  .090 7.9 .57 6.7 340 58 .58 36 8.3 8.4   450   110    8.3   450   110     .19  27   2.3   .45 83 5.1 6.1  330 57   .17 36 1.3 4.0  120 49   .23  18 2.7  13   540 110 12   540 120 14   590 110
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack 22     260 230    .16  12   1.6  .088 7.9 .61 6.4 310 57 .82 36 10   8.5   450   110    8.4   450   110     150     210   1900     .46 83 6.6 6.6  310 54   13    63 140   750    310 8100   .81  19 10    900   2000 11000 900   980 6800 900   1000 9200
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack 2.0   54 24    .13  9.5 1.2  .062 8.5 .81 910   6300 5600 .58 35 8.9 8.3   450   95    9.6   450   120     .26  27   2.6   2.8  75 41   910    6500 4800   .26 50 1.6 3.8  94 50   .37  18 4.6  11   440 77 21   730 180 11   470 93
list-ext-properties/960521-1_1_false-valid-free.i valid-deref valid-free valid-memtrack .18  26 1.5  .11  9.0 1.3  .067 7.9 .61 6.5 280 50 .59 35 7.5 8.6   450   120    8.3   440   100     .19  27   2.5   .48 83 5.5 6.8  350 54   .16 36 1.5 220    240 3400   .25  18 2.6  14   490 100 23   710 190 19   600 160
list-ext-properties/test-0158_1_false-valid-free.i valid-deref valid-free valid-memtrack .19  25 2.0  .12  8.2 .61 .076 9.1 .81 3.7 280 30 .19 34 2.8 8.4   450   100    8.6   440   110     .14  26   1.7   .44 83 6.5 3.5  250 29   .18 35 1.4 4.7  110 55   .20  18 2.1  10   410 74 20   550 190 9.9 390 80
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .20  26 1.9  .096 7.7 .91 .093 7.5 .80 3.5 250 35 .16 34 1.8 8.4   450   100    8.2   450   92     .10  27   1.3   .45 83 5.0 3.8  280 34   .15 35 1.4 6.5  110 78   .18  15 1.9  140   930 1800 250   970 2900 120   920 1300
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .18  26 1.7  .070 6.5 .43 .061 8.1 .67 3.8 280 37 .15 34 1.6 8.4   450   120    8.4   450   100     .088 26   1.1   .46 82 6.3 3.7  280 33   .26 49 1.8 6.2  83 71   .19  18 2.2  18   380 140 22   470 190 16   350 120
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack 1.2   55 17    .15  7.2 1.2  .086 7.3 .68 6.3 290 54 .16 34 1.9 8.4   450   120    8.6   450   110     .10  26   .92  .49 83 6.1 6.1  300 53   .16 34 1.4 840    340 8400   .21  17 2.9  71   800 830 900   830 11000 69   780 710
list-ext-properties/960521-1_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack .17  26 2.0  36     1000   460    .11  7.3 .48 11   680 95 30    51 460   8.9   390   120    8.9   390   110     6.2   37   77     900    4300 8500   11    690 93   1.1  58 8.5 260    260 4100   .37  17 5.1  900   1000 12000 630   1100 5600 900   1100 12000
list-ext-properties/list-ext_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack 22     260 200    76     240   1000    .082 7.9 .80 36   1900 290 400    220 5400   9.0   390   100    9.3   390   100     170     200   2500     900    4400 5900   38    1900 340   2.5  64 25   880    340 7300   .42  19 4.8  900   2200 10000 900   1000 8100 900   920 9700
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.4   45 17    37     110   450    .095 7.1 .45 900   6900 5400 130    95 1800   8.4   450   110    900     580   6600     51     120   610     900    4400 7200   930    7400 5800   900    470 5300   880    290 7700   600     3100 5700    900   2100 11000 900   1000 8700 900   1200 11000
list-ext-properties/simple-ext_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack .97  39 13    32     200   410    330     15000   4800    24   880 200 520    160 6100   8.6   390   100    8.8   390   120     270     180   3400     900    4400 9200   20    860 160   230    1700 2300   880    280 9200   .42  19 5.4  900   2100 9400 900   1100 6000 900   1000 9900
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .20  26 1.7  .10  7.9 1.2  .21  8.7 2.6  4.1 280 35 .44 35 5.4 8.3   390   110    8.4   380   100     .13  26   1.3   120    4400 1400   3.8  280 38   .16 35 1.2 5.9  77 88   .14  15 1.6  34   660 270 260   1000 2400 34   830 270
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  26 1.9  .10  6.3 .62 .11  8.2 1.1  3.5 280 33 .53 35 6.7 8.4   390   110    8.6   380   120     .15  26   2.0   330    4300 4000   3.5  280 31   .14 33 1.2 5.5  74 68   .16  16 1.7  11   390 85 25   730 260 10   390 78
list-ext-properties/test-0214_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack .18  27 1.8  570     490   4600    .10  8.7 1.1  910   5700 6200 210    310 2700   21     550   220    21     550   240     .36  27   4.5   35    4400 250   960    2500 8500   11    560 120   750    330 6200   1.6   22 21    900   1600 13000 900   1000 7900 900   1200 12000
list-ext-properties/test-0217_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack .19  28 1.6  450     380   4500    .11  8.0 .95 910   5800 7100 190    240 2700   14     440   140    14     440   150     .51  32   7.3   900    300 9400   910    5400 6100   3.2  130 33   750    370 6400   3.4   24 43    900   2600 12000 900   1000 6500 900   1000 11000
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack 9.5   130 110    2.8   37   35    .094 7.7 .70 9.2 480 71 250    230 3100   8.5   390   100    8.5   390   120     120     240   1800     900    4300 11000   8.9  480 79   1.3  38 15   880    330 8900   .31  18 3.8  900   1400 12000 900   1000 9900 900   860 11000
list-ext-properties/test-0504_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack 110     1100 1200    3.3   59   49    .082 7.6 .80 910   5700 5200 900    2200 8200   9.6   390   130    9.8   390   110     270     190   3500     900    4300 9400   900    5900 4900   900    5200 5200   750    390 6400   1.4   39 17    900   1000 12000 900   1000 10000 900   1700 11000
list-ext-properties/test-0513_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack 34     400 270    4.3   140   56    .094 7.8 1.0  5.1 290 47 93    1800 1400   8.4   390   120    8.6   390   110     18     210   210     900    4300 7700   4.8  280 43   .24 38 2.2 190    260 2000   .22  17 2.8  900   2100 9700 900   1100 7200 900   820 11000
memory-alloca/c.03-alloca_true-valid-memsafety.i valid-deref valid-free valid-memtrack .20  26 1.9  880     1300   8300    880     9100   11000    900   1000 13000 280    70 4000   8.3   450   96    1.6   200   22     900     510   10000     900    75 9500   900    940 11000   .49 35 4.3 7.1  82 83   .15  16 2.0  12   480 90 440   810 4700 12   450 93
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c valid-deref valid-free valid-memtrack .089 24 .62 .095 7.3 1.0  .067 7.2 .50 2.8 250 29 .18 33 2.0 8.2   430   120    8.2   430   100     .12  26   1.4   .46 82 6.6 2.9  250 28   .16 34 1.3 5.0  85 57   .20  16 1.7  9.0 350 69 9.5 360 76 9.3 370 69
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c valid-deref valid-free valid-memtrack .094 24 .89 .069 7.7 .61 .058 7.8 .63 2.7 250 28 .15 33 1.6 8.4   430   96    8.3   430   99     .10  26   .75  .48 83 5.7 2.8  250 24   .36 49 1.3 5.2  88 56   .18  15 2.0  9.4 380 75 9.8 410 81 9.6 390 89
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c valid-deref valid-free valid-memtrack .087 24 .78 .075 7.8 .43 .073 7.6 .42 2.8 250 26 .15 33 2.5 8.3   430   110    8.3   430   110     .081 26   .79  .44 82 6.1 2.9  250 25   .18 36 1.3 4.9  86 57   .17  15 1.9  8.5 370 69 8.3 370 59 7.5 350 53
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c valid-deref valid-free valid-memtrack .090 24 .81 .084 7.4 .40 .089 7.9 .48 2.9 240 26 .14 33 1.6 8.2   430   100    8.2   430   110     .080 26   .80  .44 83 5.1 2.8  240 27   .24 49 1.8 6.0  120 74   .17  16 2.5  7.1 340 58 9.2 370 62 8.2 350 59
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c valid-deref valid-free valid-memtrack .12  24 .75 1.3   20   17    1.5   26   21    9.3 380 68 87    220 1000   8.5   430   99    8.5   430   120     1.7   38   26     350    4300 3400   9.6  440 80   1.4  44 14   750    530 8400   .21  15 2.4  650   5000 9100 900   1200 7900 730   5200 8700
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c valid-deref valid-free valid-memtrack .087 24 .96 1.3   21   20    1.5   26   20    10   490 92 92    220 1100   8.5   430   110    8.8   430   120     1.7   37   25     .50 83 5.3 9.7  490 89   3.5  60 39   750    500 6800   .18  16 1.9  600   4900 8300 900   1200 6600 660   5100 8200
ldv-memsafety/memset2_false-valid-deref-write.c valid-deref valid-free valid-memtrack .17  25 1.3  .075 7.6 .52 .13  7.7 .54 2.8 240 23 11    37 140   8.2   430   97    8.3   430   100     1.3   41   17     .75 39 10   2.7  250 25   .24 48 1.5 2.8  74 36   .16  15 2.0  7.1 350 58 8.1 370 56 7.2 340 60
ldv-memsafety/memset3_false-valid-deref-write.c valid-deref valid-free valid-memtrack .16  25 1.4  .093 7.6 .53 .081 8.3 .62 2.7 250 23 46    40 660   8.2   430   100    8.3   430   110     14     340   220     .74 39 10   2.7  250 22   .14 33 1.4 2.8  73 31   .16  16 1.7  7.3 340 62 7.8 370 57 8.2 370 68
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c valid-deref valid-free valid-memtrack .17  25 1.8  .12  8.1 .52 .075 8.8 .65 2.8 250 26 11    38 160   8.3   430   110    8.2   430   98     1.3   41   21     .75 39 10   2.9  240 23   .36 48 1.2 2.8  73 35   .16  15 1.9  7.9 360 61 7.7 360 59 7.9 370 70
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c valid-deref valid-free valid-memtrack .15  25 1.6  .10  8.2 .56 .077 7.8 .58 2.9 250 24 46    40 670   8.3   430   100    7.9   430   99     14     340   190     .75 39 9.9 2.9  250 27   .18 33 1.3 2.8  74 32   .17  17 1.9  7.9 370 60 8.2 360 57 8.3 370 65
ldv-memsafety/memsetNonZero_false-valid-deref-write.c valid-deref valid-free valid-memtrack .16  25 1.8  .12  8.0 .53 .075 7.7 .62 2.9 250 24 46    40 660   8.2   430   100    8.3   430   110     14     340   210     .74 39 9.4 2.8  240 26   .14 33 1.2 2.8  74 31   .15  16 2.1  8.2 370 66 8.9 380 68 8.2 370 60
ldv-memsafety/memset_false-valid-deref-write.c valid-deref valid-free valid-memtrack .20  25 1.6  .082 8.6 .53 .082 7.6 .55 2.8 240 25 46    40 670   8.2   430   110    8.2   430   120     14     340   190     .74 39 9.6 2.7  250 27   .31 48 1.0 2.8  74 39   .16  16 2.0  8.4 370 67 8.0 370 56 8.3 350 61
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c valid-deref valid-free valid-memtrack .094 24 .71 880     4100   6200    870     4300   9400    84   4500 960 900    970 9600   12     380   130    12     380   160     900     2300   11000     900    74 9700   92    4700 960   900    1600 6800   760    380 7500   290     15000 4100    900   2400 12000 900   1000 6800 900   5500 11000
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .088 23 .71 1.3   18   17    1.9   26   23    9.5 760 97 41    140 490   8.5   370   120    8.4   370   100     .75  27   9.5   510    4300 5300   9.6  700 100   2.1  77 24   760    710 6000   .18  15 1.7  25   500 250 900   1200 7200 18   660 140
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c valid-deref valid-free valid-memtrack .092 24 .90 1.2   13   19    1.5   18   19    7.8 400 61 79    190 1000   8.3   370   110    8.4   370   100     1.7   37   20     420    4300 4500   7.6  470 69   2.9  53 34   750    530 9100   .15  15 1.7  19   650 160 900   1300 7600 30   680 330
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .084 23 .75 1.4   18   16    1.9   26   26    10   800 110 41    140 520   8.6   370   110    8.4   370   100     .78  27   11     530    4300 5300   9.6  790 88   2.1  79 23   760    710 8500   .15  15 1.8  17   640 130 900   1600 6900 27   530 300
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c valid-deref valid-free valid-memtrack .12  24 .75 6.2   67   95    22     140   180    51   4000 440 900    1000 11000   9.9   370   100    9.9   380   120     48     660   670     900    1600 11000   50    3800 460   210    700 3400   760    390 7700   .18  15 1.7  17   640 150 900   1100 7100 21   660 200
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .087 24 .78 1.3   13   18    1.6   18   20    7.6 470 62 89    210 1100   8.2   370   110    8.3   370   96     1.9   39   27     340    4300 2900   7.6  470 68   3.0  58 33   750    400 9800   .17  15 1.6  18   530 140 900   1300 7400 18   650 150
ldv-memsafety/StructInitialization1_true-valid-memsafety.c valid-deref valid-free valid-memtrack .11  24 .80 .093 6.4 .28 .11  6.2 .31 3.2 270 26 .88 66 8.7 8.0   370   110    8.1   370   100     .11  27   1.2   330    4300 3400   3.2  270 26   .32 46 1.1 5.4  76 61   .14  16 1.6  11   420 76 30   640 260 11   420 91
ldv-memsafety/StructInitialization2_true-valid-memsafety.c valid-deref valid-free valid-memtrack .10  24 .75 .097 6.2 .33 .057 6.8 .47 3.0 240 24 .89 65 11   8.1   370   94    8.1   370   98     .10  27   1.3   330    4300 3500   3.3  270 30   .16 30 1.2 5.4  76 66   .15  15 1.6  11   400 80 31   620 250 11   400 80
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .10  24 .86 .050 7.5 .48 .077 6.1 .34 3.1 280 28 .83 67 8.3 8.2   370   100    8.4   370   91     .085 26   .97  460    4300 5700   3.0  270 28   .15 32 1.8 5.2  71 59   .13  16 1.6  7.0 340 60 7.6 350 56 8.0 360 68
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .15  25 1.3  .15  6.8 .55 .084 8.5 .80 2.6 240 26 .82 67 8.8 8.2   430   110    8.1   430   110     .084 26   .96  .74 39 9.4 2.7  240 25   .16 33 1.2 5.2  72 70   .13  16 1.5  10   380 86 48   710 390 10   400 77
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .17  25 1.5  .15  7.1 .69 .081 8.0 .65 2.7 250 23 .82 66 8.4 8.3   430   100    8.1   430   99     .083 26   1.0   .73 39 9.9 2.7  250 23   .14 32 1.3 5.3  72 63   .16  14 1.5  9.3 380 88 99   960 810 9.8 390 79
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .19  25 1.5  .095 7.9 .63 .10  7.8 .61 2.7 250 26 11    69 180   8.2   430   87    8.1   430   110     1.4   42   17     .74 39 9.8 2.7  240 25   .14 33 1.2 5.3  72 65   .13  16 1.4  10   390 86 48   900 360 10   400 94
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .15  25 1.9  .080 7.1 .83 .12  7.8 .69 2.8 250 26 46    67 670   8.4   430   97    8.2   430   100     15     350   190     .76 39 9.7 2.7  250 23   .13 33 1.5 5.3  72 69   .14  16 1.5  9.8 390 88 110   1100 990 9.2 370 78
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .16  25 1.6  .084 7.5 .77 .089 8.5 .57 2.7 240 25 46    69 470   8.1   430   99    8.2   430   120     15     350   220     .74 39 9.3 2.8  240 27   .15 33 1.7 5.3  72 60   .15  16 1.7  9.2 370 81 81   1200 840 9.8 400 90
ldv-memsafety/memset_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack .16  25 1.4  .091 7.3 .63 .079 8.0 .71 2.7 240 26 .79 66 12   8.3   430   98    8.4   430   120     .087 26   .77  .76 39 9.2 2.7  240 23   .18 46 1.5 5.3  72 62   .13  15 1.5  10   380 76 81   1300 910 10   400 83
ldv-memsafety/memleaks_test14_3_false-valid-deref.i valid-deref valid-free valid-memtrack .18  28 1.6  .15  11   1.8  .096 10   1.0  4.6 290 41 .21 35 2.3 8.5   450   120    8.6   450   100     .14  27   1.6   .57 83 7.4 4.4  290 40   .22 40 1.8 4.0  120 51   .27  18 3.8  13   350 110 13   350 110 13   360 110
ldv-memsafety/memleaks_test22_3_false-valid-deref.i valid-deref valid-free valid-memtrack .17  28 2.1  .15  8.9 1.7  .14  8.0 .97 4.8 290 37 .27 35 3.3 8.5   450   110    8.7   450   110     .18  27   2.1   .57 84 7.0 4.8  290 43   .22 38 1.8 4.0  86 49   .27  19 3.2  590   2300 7500 530   1100 7000 900   2400 11000
ldv-memsafety/memleaks_test22_5_false-valid-deref.i valid-deref valid-free valid-memtrack .18  27 1.7  .15  8.9 1.6  .14  8.4 1.0  4.8 290 38 .26 35 3.1 8.5   450   100    8.5   450   96     .18  27   2.7   .56 83 6.6 4.8  290 42   .23 40 1.7 4.0  86 48   .28  18 4.4  900   2300 11000 670   840 5800 900   1200 9000
ldv-memsafety/memleaks_test23_2_false-valid-deref.i valid-deref valid-free valid-memtrack .21  28 2.1  6.6   160   80    .12  9.8 1.4  5.1 290 44 2.4  55 31   8.7   450   98    9.1   450   130     2.4   47   30     900    1100 8200   5.3  290 46   .29 40 2.1 5.4  130 81   .59  18 7.8  140   800 1900 16   360 130 130   740 1600
ldv-memsafety/memleaks_test23_4_false-valid-deref.i valid-deref valid-free valid-memtrack .20  28 1.9  6.6   160   89    .12  9.2 1.3  5.4 290 50 2.4  54 29   8.8   450   98    9.0   450   110     2.3   47   33     900    1100 8800   5.1  290 44   .28 37 2.3 5.0  100 59   .59  18 7.2  65   860 540 180   1100 1500 900   1300 13000
ldv-memsafety/memleaks_test11_1_false-valid-free.i valid-deref valid-free valid-memtrack .28  28 2.9  .16  11   1.8  .097 9.5 1.1  4.6 270 43 .52 38 6.2 8.4   450   110    8.7   450   98     .44  30   6.1   .61 83 7.7 4.5  290 43   .25 39 1.8 5.6  84 70   .29  18 3.5  140   890 1600 340   940 2800 430   790 5400
ldv-memsafety/memleaks_test12_false-valid-free.i valid-deref valid-free valid-memtrack .26  29 3.2  .24  13   2.7  .14  10   1.6  5.5 300 48 570    1900 7100   8.7   450   99    8.7   450   100     13     210   180     .65 84 8.9 5.6  290 45   .29 40 2.9 11    120 1200   .70  21 10    900   1400 11000 900   1100 7700 900   1600 13000
ldv-memsafety/memleaks_test17_2_false-valid-free.i valid-deref valid-free valid-memtrack .18  28 1.6  1.3   54   17    .13  9.0 .95 5.3 300 42 30    130 350   8.6   450   100    8.8   450   130     11     120   170     .61 84 7.1 5.5  300 51   .73 36 2.9 52    150 670   .33  18 3.3  310   2100 4000 900   960 7900 350   850 5000
ldv-memsafety/memleaks_test19_false-valid-free.i valid-deref valid-free valid-memtrack .24  28 2.5  .16  8.0 2.1  95     210   1200    4.4 290 38 .20 35 2.0 8.4   450   99    8.7   450   110     .13  27   1.6   .64 86 8.1 4.7  290 44   .23 38 1.8 5.4  84 76   .29  18 4.0  250   860 2700 520   760 4300 590   870 7300
ldv-memsafety/memleaks_test1_false-valid-free.i valid-deref valid-free valid-memtrack .21  28 1.7  .12  8.1 1.0  .12  8.7 1.2  4.0 260 33 .17 35 2.0 8.5   450   110    8.5   440   99     .12  27   1.0   .57 83 8.1 4.1  290 39   .21 37 1.8 4.5  110 55   .28  18 3.3  12   440 98 10   380 74 10   390 76
ldv-memsafety/memleaks_test3_false-valid-free.i valid-deref valid-free valid-memtrack .21  27 1.6  .11  9.3 1.2  .15  9.5 1.1  4.0 280 37 .18 35 1.7 8.5   450   120    8.6   450   100     .11  27   .98  .58 83 7.0 4.3  290 38   .21 38 1.7 4.4  76 52   .26  18 3.4  9.9 360 80 8.4 350 61 8.8 360 63
ldv-memsafety/memleaks_test6_2_false-valid-free.i valid-deref valid-free valid-memtrack .21  28 1.8  .12  8.3 1.5  .14  9.4 1.4  4.3 290 34 .17 35 1.9 8.6   450   99    9.1   450   120     .12  27   1.3   .59 83 7.4 4.3  280 39   .23 38 1.9 5.0  79 62   .29  18 4.2  18   600 140 39   710 360 17   560 130
ldv-memsafety/memleaks_test8_2_false-valid-free.i valid-deref valid-free valid-memtrack .21  27 1.8  .11  8.3 1.0  .12  9.3 1.2  4.4 290 35 .20 35 1.9 8.4   450   130    8.6   450   130     .11  28   .99  .59 83 8.0 4.2  260 40   .24 38 1.7 4.8  110 61   .25  18 3.3  13   450 99 11   410 91 10   380 73
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .27  27 2.5  .21  10   1.8  3.1   64   44    4.5 290 44 .39 37 5.6 8.5   450   100    8.5   450   110     .33  29   4.3   .59 83 7.4 4.4  290 41   .24 38 1.8 7.1  81 91   .29  18 3.2  900   880 11000 350   790 2900 900   930 12000
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .29  28 2.7  .15  10   1.9  .10  10   1.1  4.6 290 39 .40 37 5.1 8.6   450   110    8.7   450   140     .34  29   4.2   .61 84 6.8 4.8  290 40   .23 41 1.8 7.5  82 91   .29  18 3.4  870   800 10000 400   760 3200 900   780 12000
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .21  28 1.5  .10  7.6 1.1  .14  8.6 .90 4.4 280 39 .17 35 1.9 8.3   450   120    8.5   440   100     .10  27   1.2   .56 83 7.3 4.4  280 40   .22 39 2.1 6.5  82 81   .26  17 3.3  200   710 2600 48   880 420 200   690 2700
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i valid-deref valid-free valid-memtrack .18  27 1.7  .15  11   1.5  .091 8.7 1.1  4.4 290 37 1.2  41 14   8.4   450   110    8.3   450   110     .93  37   12     .58 83 8.2 4.7  290 36   .22 40 1.7 8.6  87 110   .28  18 3.1  620   850 9200 250   1000 2200 900   6900 11000
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .23  27 2.2  .13  6.8 1.0  .13  8.7 .83 4.4 290 35 .16 35 2.0 8.5   450   110    8.5   450   100     .13  27   1.2   .58 83 7.4 4.3  290 39   .33 54 2.0 6.4  80 74   .32  18 2.6  13   330 100 14   350 110 12   320 110
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i valid-deref valid-free valid-memtrack .18  28 1.6  .15  10   1.9  .12  8.8 .95 4.6 290 39 1.1  42 16   8.5   450   110    8.8   450   110     .83  36   12     .58 83 7.7 4.6  290 43   .20 41 1.8 8.3  110 100   .28  18 3.8  13   360 100 12   330 110 13   360 120
ldv-memsafety/memleaks_test15_false-valid-memtrack.i valid-deref valid-free valid-memtrack .28  28 2.2  .15  8.4 1.5  2.5   56   36    4.9 290 37 .54 43 6.8 8.5   450   96    9.8   450   110     .49  34   6.5   .60 84 7.7 4.8  290 41   .24 39 2.0 13    93 170   .45  17 6.4  900   1500 11000 900   870 7900 910   14000 8500
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .22  28 1.6  .10  6.8 1.0  .11  9.7 1.0  4.1 270 35 .16 34 1.8 8.5   450   120    8.9   450   100     .13  27   1.0   29    89 370   4.3  290 38   .19 40 1.9 6.2  110 76   .28  19 3.5  23   480 200 15   360 120 20   390 160
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.8  .13  6.7 .82 .11  8.3 .84 4.2 290 37 .16 35 1.9 8.4   450   120    8.7   450   83     .096 27   1.1   .62 83 7.2 4.2  290 39   .23 38 1.7 6.1  81 80   .26  18 3.7  20   400 170 17   370 120 16   370 120
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i valid-deref valid-free valid-memtrack .21  28 1.4  1.9   63   25    .12  9.7 1.2  5.4 290 44 24    130 360   8.4   450   97    8.5   450   110     9.6   120   120     .58 84 8.9 5.5  290 47   .24 40 2.2 110    160 1300   .30  18 3.4  900   2200 11000 900   1000 7300 900   830 11000
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i valid-deref valid-free valid-memtrack .18  28 1.5  1.5   49   22    .099 9.1 1.0  5.2 290 41 31    90 470   8.6   450   92    8.5   450   140     8.4   82   120     .58 83 9.5 5.3  300 46   .23 40 2.2 43    130 580   .38  17 3.6  900   980 11000 900   1000 8600 900   900 14000
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .18  27 1.4  .16  12   2.1  .095 9.8 1.3  5.4 300 48 .18 35 2.0 8.5   450   110    8.6   450   120     .14  27   1.3   .58 83 5.4 4.9  280 40   .23 38 1.9 13    120 180   .27  19 3.4  32   580 320 19   540 160 49   600 550
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .18  27 1.8  1.1   38   13    .097 9.1 1.1  5.1 290 47 89    88 1200   8.5   450   97    8.6   450   120     27     83   330     .59 84 6.7 5.3  290 46   .25 37 1.6 37    120 530   .33  18 3.7  900   1300 11000 900   1100 7600 900   850 11000
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .17  27 1.9  .44  13   5.5  .11  8.6 .96 5.0 290 37 24    49 350   8.5   450   120    8.9   450   120     6.3   36   77     .57 83 8.3 5.2  300 48   120    670 760   8.3  87 100   .40  25 4.7  260   1000 3200 99   1100 900 440   1100 5600
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .20  27 1.6  .099 6.6 .89 .097 9.8 1.0  4.3 290 38 .16 35 2.0 8.3   450   100    8.8   450   120     .097 27   1.0   .56 83 7.1 4.3  280 36   .19 39 2.5 6.0  75 85   .25  17 3.5  20   390 160 15   340 120 15   370 120
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .18  28 2.3  .096 7.5 .90 .11  8.7 .93 4.3 280 40 .17 35 1.9 8.3   450   98    8.3   450   99     .094 27   1.5   .61 83 7.6 4.4  290 35   .30 54 2.1 6.2  82 95   .27  18 3.7  21   430 180 16   370 130 17   380 150
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .20  28 2.3  .095 7.5 .97 .090 9.4 .87 4.2 290 40 .16 35 1.8 8.5   450   92    8.6   450   120     .096 27   1.4   .56 83 7.1 4.3  280 41   .20 39 1.8 6.1  81 71   .25  17 3.1  20   400 160 15   380 130 15   380 140
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .20  28 1.8  .14  8.5 1.6  .15  8.5 1.1  4.4 270 39 .22 35 2.5 8.4   450   100    8.7   450   100     .18  27   2.0   .56 83 8.5 4.6  290 37   .21 39 2.0 7.4  83 94   .27  18 3.7  290   1300 3800 160   1100 1700 260   1300 3500
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.7  .12  7.3 1.3  .10  9.6 1.2  4.4 290 35 .17 34 1.8 8.7   450   98    8.6   450   110     .11  27   1.3   .55 83 8.5 4.0  270 37   .22 38 2.0 6.4  83 68   .28  19 2.9  56   1000 570 58   980 700 72   1000 710
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .20  27 1.7  .14  8.0 1.6  .10  9.8 1.2  4.6 280 37 .22 35 3.1 8.3   450   110    8.7   450   110     .17  27   1.9   .56 84 6.5 4.6  290 47   .23 39 1.8 7.5  83 90   .30  18 2.9  280   1300 3400 190   970 1500 270   1300 3500
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .19  28 2.3  .13  7.0 1.2  .11  9.7 1.4  4.5 280 42 .17 35 1.9 8.4   450   120    8.6   450   110     .15  27   1.3   .57 83 7.4 4.3  290 41   .22 39 1.8 6.2  81 74   .27  18 4.0  23   450 180 16   380 130 19   390 150
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .19  28 2.0  .088 7.3 .84 .093 8.8 .88 4.2 290 37 .16 34 2.0 8.4   450   110    8.4   450   97     .094 27   1.3   .57 83 7.0 4.2  290 40   .24 38 3.4 6.1  80 82   .26  17 2.8  20   380 140 16   360 140 16   380 140
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .20  27 1.7  .10  6.5 1.0  .11  10   1.4  4.4 280 41 .18 35 1.7 8.4   450   110    8.7   450   120     .10  27   1.1   .56 83 6.8 4.2  280 39   .26 53 2.2 6.2  82 76   .28  18 2.8  22   440 160 16   370 120 18   380 140
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .22  27 1.8  .11  7.2 1.3  .13  9.0 1.3  4.1 270 35 .16 35 2.4 8.6   450   93    9.3   450   110     .099 27   1.2   .60 84 6.7 4.3  290 37   .22 38 1.7 6.6  82 74   .28  18 3.2  100   650 1200 26   720 230 110   620 1200
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .22  27 2.7  .11  7.0 1.2  .11  9.3 1.3  4.6 290 42 .19 35 1.8 8.4   450   120    9.3   450   120     .099 27   1.2   .57 83 6.7 4.4  290 43   .25 39 1.7 6.5  81 95   .27  18 3.2  82   670 1000 28   580 280 78   630 910
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.7  .11  7.2 1.1  .12  8.9 1.3  4.4 280 43 .17 35 2.0 8.5   450   97    9.3   450   100     .10  27   .96  .59 84 6.9 4.5  290 36   .23 39 1.8 6.5  82 92   .28  18 3.6  110   560 1400 20   500 160 92   530 1100
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.4  .096 7.2 .98 .095 9.2 1.1  4.3 280 38 .16 35 1.9 8.4   450   100    8.4   450   97     .10  27   1.1   .58 83 7.2 4.3  290 39   .24 39 1.6 6.2  80 66   .25  18 3.4  19   380 140 15   360 130 16   370 120
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .20  28 2.2  .10  7.9 .99 .10  9.6 .97 4.3 280 38 .16 35 1.8 8.5   450   100    8.7   450   98     .10  27   1.1   .58 83 6.9 4.2  280 40   .24 37 1.6 6.3  110 65   .28  18 2.9  22   420 160 16   360 120 17   380 130
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.9  .11  6.7 .88 .13  8.4 .95 4.2 280 38 .18 35 2.0 8.4   450   97    8.6   450   120     .095 27   1.1   .58 83 7.7 4.1  270 41   .21 39 1.7 6.2  81 65   .26  18 2.8  20   380 160 15   360 130 15   340 110
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .27  28 3.5  .32  12   5.1  24     270   320    4.6 290 42 1.8  39 27   8.6   450   91    8.6   450   120     .80  31   9.7   900    4500 7000   4.5  290 44   .22 39 2.7 6.8  78 79   .25  23 3.0  900   870 12000 900   860 7700 900   970 14000
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .29  28 3.0  .23  11   3.4  .10  9.6 1.2  4.7 290 43 1.8  40 24   8.4   450   110    8.7   450   110     .82  31   11     900    4400 8400   4.8  290 44   .23 39 2.4 6.7  79 92   .26  17 2.5  900   1000 12000 810   970 6000 900   820 11000
ldv-memsafety/memleaks_test12_true-valid-memsafety.i valid-deref valid-free valid-memtrack .26  28 2.7  .23  13   2.6  .14  9.9 1.7  6.0 300 50 560    1900 8000   8.7   450   130    8.6   450   110     15     190   210     900    4500 8800   6.1  300 50   .29 41 2.4 270    240 3200   .47  21 6.0  900   1600 12000 900   1100 8000 900   2100 11000
ldv-memsafety/memleaks_test13_true-valid-memsafety.i valid-deref valid-free valid-memtrack .18  27 1.5  .25  11   3.2  .13  8.7 .97 4.3 290 39 14    290 160   8.5   450   98    8.4   450   100     1.4   36   23     52    4400 710   4.6  280 44   .19 39 1.9 8.2  86 110   .22  18 2.8  78   1100 780 300   1000 2500 680   810 8900
ldv-memsafety/memleaks_test14_true-valid-memsafety.i valid-deref valid-free valid-memtrack .18  27 1.6  .24  12   2.2  .14  8.6 .98 4.4 290 38 20    290 250   8.5   450   98    8.6   450   100     1.4   36   23     50    4300 580   4.4  290 41   .20 37 1.7 7.7  85 85   .22  18 3.0  12   340 93 13   340 100 13   360 100
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  28 2.3  .31  13   4.1  .13  9.7 1.4  5.0 290 42 7.1  49 80   8.4   450   110    10     450   140     3.4   40   42     900    4600 6300   4.8  290 42   .25 40 1.9 10    89 140   .29  18 3.3  900   1300 14000 900   970 13000 900   860 11000
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  27 2.0  .14  7.3 1.7  .15  8.7 1.6  4.2 290 36 .42 36 5.2 8.4   450   110    9.3   450   120     .10  27   1.2   65    4400 780   4.4  290 36   .22 38 1.8 5.5  74 64   .22  18 2.6  14   550 110 12   490 94 12   530 100
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  28 1.8  2.9   64   48    .13  9.0 1.2  5.8 300 47 76    170 1100   8.5   450   100    8.6   450   100     68     130   950     900    4500 7600   5.8  300 47   .40 53 2.3 130    160 1600   .29  17 3.9  900   2100 11000 900   1000 8800 900   820 13000
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  28 1.8  280     13000   2800    880     10000   13000    4.7 270 45 900    280 11000   8.5   450   110    1.6   200   21     900     350   11000     900    150 11000   4.6  290 44   .39 53 2.2 880    300 9000   900     460 14000    900   1100 12000 900   1000 7500 900   780 12000
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  27 1.8  1.6   38   21    .096 9.0 .96 5.5 290 48 95    120 1400   8.5   450   110    8.8   450   120     44     92   590     900    4300 9500   5.4  300 48   .37 53 3.8 54    120 840   .28  17 3.6  900   980 12000 900   1100 7400 900   840 12000
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .25  28 2.1  .18  7.4 2.5  .77  27   8.2  4.4 280 44 .54 36 6.8 8.4   450   98    8.9   450   95     .15  27   1.6   270    4300 3100   4.2  270 40   .26 53 1.8 6.5  78 80   .23  18 2.7  900   880 13000 680   780 5900 880   830 12000
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .20  28 1.7  .14  7.2 1.5  .14  8.8 1.7  4.2 290 41 .42 36 4.8 8.5   450   99    8.7   450   100     .11  27   1.2   41    4900 500   4.2  280 37   .21 38 1.7 5.4  76 73   .23  19 2.4  12   490 110 9.6 370 71 9.7 370 72
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  28 1.6  .15  7.0 1.5  .13  8.5 .85 4.4 290 37 .43 36 5.2 8.5   450   120    8.6   450   91     .12  27   1.0   44    4300 590   4.4  290 41   .32 52 1.9 5.7  74 76   .22  18 2.5  15   580 120 12   510 93 12   520 89
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  27 1.5  .14  6.9 1.6  .098 9.3 .98 4.4 290 34 .43 36 5.3 8.5   450   97    8.6   450   120     .10  27   1.3   44    4500 470   4.5  290 43   .23 38 1.6 5.5  74 76   .22  18 2.5  13   490 96 11   540 97 12   460 92
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .21  27 1.7  .22  8.1 2.5  .15  8.2 1.0  4.6 290 46 .60 36 8.3 8.4   450   130    8.5   450   100     .20  27   2.4   48    4600 560   4.5  280 40   .33 52 1.8 6.6  79 92   .26  18 2.8  900   2500 12000 720   850 6000 900   980 9300
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.6  .23  9.6 2.7  .14  8.6 .98 4.5 280 45 .73 36 9.5 8.4   450   110    8.6   450   110     .28  27   2.6   59    4300 700   4.8  290 41   .23 38 2.0 7.3  81 87   .23  19 3.2  900   2700 11000 900   920 7800 900   870 11000
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  27 2.2  .22  9.5 2.7  .13  8.7 1.2  4.4 290 41 .74 36 9.9 8.6   450   120    8.7   450   110     .28  27   2.9   52    4600 640   4.8  290 36   .22 39 1.9 7.4  83 84   .23  18 2.7  900   3800 11000 900   940 7800 900   940 12000
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack .21  28 1.8  880     2200   12000    .12  9.9 1.7  5.2 290 44 900    650 10000   8.9   450   100    9.6   450   110     900     1200   9700     900    3000 12000   5.3  290 45   120    170 1400   890    340 9300   900     92 13000    130   790 1800 16   370 130 130   750 1700
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i valid-deref valid-free valid-memtrack .21  28 2.2  880     2200   12000    .13  9.5 1.2  5.2 290 45 900    920 11000   8.7   450   99    9.8   450   110     900     640   13000     900    560 11000   5.2  290 43   120    170 1400   890    350 11000   900     92 11000    900   2400 10000 900   940 7900 900   1300 11000
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .23  28 1.6  .14  7.4 1.5  .15  9.5 1.7  4.3 290 41 .42 36 6.2 8.6   450   100    8.7   450   120     .11  27   1.2   41    4900 480   4.3  290 38   .19 38 1.8 5.5  76 69   .21  19 2.3  13   510 110 11   480 94 11   410 97
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .23  28 2.1  .16  7.3 1.7  .16  8.7 2.0  4.4 290 39 .48 36 5.8 8.6   450   120    8.5   450   100     .14  27   1.5   68    4700 880   4.4  290 39   .22 39 1.5 5.6  76 64   .22  18 2.8  29   540 280 12   550 99 130   600 1800
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.6  .16  6.8 1.4  .15  8.9 1.7  4.3 270 36 .43 36 5.1 8.5   450   110    8.6   450   98     .11  27   1.2   39    4300 480   4.4  280 39   .21 38 1.6 5.5  75 85   .24  17 2.5  13   500 120 11   490 87 12   490 92
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .22  28 1.8  .16  7.4 1.7  .21  8.6 2.9  4.3 290 38 .44 36 5.2 8.6   450   100    9.0   450   100     .11  27   1.3   180    4600 2300   4.4  290 39   .34 53 2.0 5.9  74 72   .24  18 2.8  18   680 150 64   780 530 17   590 150
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .20  27 1.8  .15  7.1 2.1  .30  12   3.3  4.4 290 40 .45 36 5.5 8.4   450   110    9.1   450   100     .14  27   1.4   180    4800 2300   4.5  290 39   .22 38 2.0 5.8  75 79   .24  18 2.8  17   510 140 45   750 410 16   590 130
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.7  .17  6.7 1.8  .15  8.7 1.6  4.2 280 37 .43 36 5.1 8.6   450   92    8.4   450   140     .10  27   1.1   43    4500 550   4.3  290 41   .19 39 1.6 5.7  73 65   .24  17 2.3  12   480 97 11   450 87 11   430 91
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  27 1.7  .14  7.1 1.6  .15  9.4 1.8  4.4 280 42 .43 36 5.2 8.6   450   120    8.6   450   91     .12  27   1.0   44    4600 570   4.2  290 36   .31 52 1.9 5.7  72 66   .22  18 2.5  13   510 110 11   510 97 12   420 91
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .18  24 1.7  .10  6.5 1.0  .32  18   4.0  3.1 270 29 .84 67 9.0 8.0   370   110    8.0   370   110     .10  26   .96  410    4300 4100   3.3  270 28   .13 31 2.1 5.8  76 78   .18  16 2.1  11   320 86 11   330 86 11   330 93
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  25 1.6  .12  7.3 1.1  .27  21   3.5  2.8 250 26 1.3  67 14   8.0   370   120    8.2   370   96     .16  26   2.0   350    4300 3700   3.0  270 26   .16 32 1.3 6.1  78 81   .16  16 2.1  11   330 89 10   300 83 10   320 87
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .16  25 1.4  .18  6.9 1.3  10     140   130    3.0 270 29 1.6  67 19   8.2   370   96    8.2   370   120     .17  26   1.9   360    4300 3600   3.2  270 29   .15 33 1.2 6.3  79 73   .17  16 2.7  11   320 85 10   310 86 11   330 88
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .19  25 1.8  .12  7.6 1.5  .97  75   12    3.0 270 28 2.3  36 26   8.2   370   98    8.1   370   90     .23  26   2.6   340    4300 3900   3.1  270 31   .26 46 1.4 6.1  77 71   .18  16 1.8  11   350 83 11   330 88 11   340 93
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack .17  25 1.4  .15  7.5 1.4  20     1400   240    2.9 250 29 2.9  67 34   8.1   370   120    8.1   370   86     .27  26   3.0   360    4300 4000   3.2  280 27   .15 33 1.3 6.9  81 89   .16  16 2.0  11   330 88 10   320 79 11   330 88
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i valid-deref valid-free valid-memtrack .18  24 1.9  .12  7.1 .75 .13  7.3 1.2  3.0 270 30 .15 33 1.6 8.0   430   130    8.1   430   96     .11  26   1.1   .44 83 5.6 3.2  260 29   .13 34 1.1 3.1  83 41   .18  17 2.4  11   340 89 11   340 92 11   330 91
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i valid-deref valid-free valid-memtrack .16  25 1.5  .088 8.1 1.1  .12  8.0 .86 3.0 270 27 1.2  35 15   8.2   430   110    8.2   430   110     .16  26   1.6   .47 83 4.8 3.2  270 29   .17 34 1.3 3.2  84 47   .20  16 1.9  11   340 82 10   310 81 11   330 95
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i valid-deref valid-free valid-memtrack .19  25 1.4  .13  8.0 .92 .088 7.9 .79 3.0 270 28 3.3  37 38   8.1   430   120    8.2   430   130     .32  26   3.6   .44 83 5.1 2.7  250 27   .17 34 1.2 2.9  83 31   .19  16 2.3  11   320 80 10   320 79 11   330 79
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i valid-deref valid-free valid-memtrack .16  26 1.8  .10  7.9 .95 .095 8.0 .75 3.2 270 29 2.5  36 28   8.1   430   91    8.1   430   93     .28  26   3.3   .48 83 4.6 3.1  270 28   .14 35 1.2 2.9  82 36   .19  16 2.3  11   340 87 11   330 81 12   330 93
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i valid-deref valid-free valid-memtrack .17  25 1.5  .096 8.4 .77 .30  21   3.4  3.2 280 25 1.2  36 14   8.1   430   99    8.2   430   110     .15  26   1.6   .47 83 5.9 3.1  270 29   .13 33 1.3 5.4  85 71   .20  18 2.5  10   320 83 11   320 87 11   330 88
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .23  29 2.0  880     3800   8000    450     15000   5700    900   4600 8700 900    6200 7900   8.4   450   100    8.4   450   100     900     6500   7200     900    180 10000   900    4600 10000   .74 50 6.5 750    660 6300   900     1100 13000    900   1200 11000 900   1000 8200 900   1100 10000
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 3.8   43 50    880     2500   8400    .14  9.5 1.3  4.3 290 37 900    12000 5400   900     410   8100    900     410   8000     22     15000   270     900    170 9500   4.3  290 40   .79 46 7.2 750    390 10000   900     5600 5800    900   1200 11000 900   880 10000 900   1000 11000
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 880     4900 6200    310     13000   3200    .11  9.0 1.1  910   11000 6000 900    1700 10000   8.4   450   100    8.7   450   100     900     1800   9500     900    170 11000   910    11000 6300   .83 52 7.3 750    610 6700   900     1800 12000    850   2300 11000 900   1100 9800 780   2200 9500
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 900     4400 12000    880     4500   11000    360     15000   4800    910   5000 7300 900    610 11000   900     440   8800    900     440   8100     900     820   11000     900    170 10000   900    5000 7600   .82 47 7.8 750    290 7700   900     4400 10000    900   1900 10000 900   1000 7600 900   860 11000
heap-manipulation/tree_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack 110     1300 1100    .25  18   2.9  .14  7.4 .96 920   11000 5300 .72 35 9.6 8.6   450   100    8.7   450   110     .36  29   4.3   900    170 12000   970    11000 6000   .62 36 6.1 6.8  110 94   .36  18 4.5  350   1300 4500 410   860 4000 900   860 10000
heap-manipulation/tree_false-valid-deref.i valid-deref valid-free valid-memtrack 120     1400 1200    .26  18   2.8  .13  7.8 1.1  930   11000 7600 .17 34 1.9 8.6   450   110    9.4   450   110     .11  27   1.3   .48 83 6.8 910    11000 7000   .17 38 1.4 3.7  93 49   .26  19 3.5  8.8 340 70 10   380 74 9.7 360 75
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .19  26 2.0  .14  10   1.7  620     15000   7800    910   11000 5900 .55 35 6.7 8.4   450   95    9.5   450   99     .25  27   3.1   23    83 320   920    11000 5900   .19 37 1.4 760    230 8000   .29  18 4.0  900   1600 11000 900   1100 7300 900   4000 11000
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack 54     1000 610    .23  18   3.5  .11  8.1 .91 970   11000 6500 .96 38 11   8.3   450   100    8.5   450   97     .59  32   8.9   .48 83 5.2 930    11000 5600   .16 37 1.3 750    310 5300   .27  18 3.1  67   790 680 94   1100 1000 66   810 770
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack 18     360 200    .23  13   2.3  .11  8.3 1.1  900   11000 6500 .86 36 11   8.2   450   100    8.5   450   100     .47  29   5.8   .45 83 5.6 930    11000 6300   .25 50 1.8 840    320 8100   .29  19 3.7  900   2000 9200 550   810 4500 900   1200 13000
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack 4.4   130 54    .15  11   1.6  .092 7.8 .88 920   11000 6600 .82 35 11   8.6   450   93    8.5   450   100     .47  29   6.0   .47 83 5.9 920    11000 7100   .19 34 1.3 840    300 9000   .36  17 3.5  900   1200 12000 340   880 3300 900   1200 9700
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .86  37 11    880     5000   10000    580     15000   7700    910   11000 6200 900    210 11000   900     400   8900    900     400   8000     900     450   12000     900    180 10000   900    11000 6600   900    1800 6600   880    320 9600   900     1800 10000    900   1100 8700 900   1100 7900 900   1200 10000
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .67  32 8.8  .11  7.1 .80 .065 7.8 .60 970   11000 6600 .16 34 2.2 8.4   440   100    9.7   450   120     .11  26   1.4   .44 83 6.3 910    11000 5600   .35 50 1.4 760    330 7700   .26  20 3.2  19   390 150 29   590 240 18   380 150
list-properties/list_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack 2.9   72 34    .16  10   1.5  .071 7.8 .70 910   11000 7000 .18 34 2.5 8.4   450   120    8.5   440   110     .13  26   2.4   .45 83 6.3 910    11000 7100   .16 36 1.4 760    300 6600   .26  18 3.1  26   590 250 44   700 390 25   520 220
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .44  30 4.1  .083 6.7 .55 .064 7.6 .52 930   11000 6700 .43 35 5.9 8.5   440   88    8.6   450   100     .15  26   1.6   900    180 11000   910    11000 6100   .16 32 1.8 760    330 7900   .25  18 2.9  19   400 150 24   590 230 19   380 170
list-properties/simple_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .37  29 3.7  .080 7.7 1.1  .17  7.3 1.1  900   11000 6500 .50 35 6.0 8.3   450   120    8.4   450   100     .20  26   2.7   .46 83 5.8 920    11000 6400   .26 50 1.7 760    260 5900   .26  18 3.0  23   530 210 36   680 350 24   570 230
list-properties/splice_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack 2.3   72 26    .12  9.0 1.3  .10  7.2 .91 910   11000 6600 .16 34 2.3 8.4   450   120    8.5   450   97     .10  27   1.1   .46 79 7.2 910    11000 7000   .39 51 1.3 760    350 9500   .26  18 2.7  20   400 150 25   520 190 19   380 140
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .41  42 3.3  120     970   1200    .48  29   7.1  6.8 300 54 28    180 390   8.8   450   98    1.6   200   21     .20  39   3.1   61    4400 440   6.8  310 60   .64 61 4.8 320    550 4100   .70  35 9.6  31   600 290 900   2100 9400 28   570 220
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .42  41 3.4  99     940   1000    .47  29   5.9  6.4 300 60 26    180 320   8.8   450   120    1.6   200   22     .21  39   2.0   57    4300 410   6.7  300 58   .63 58 4.8 260    530 3100   .72  34 7.8  34   590 260 900   1700 8400 28   580 220
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .38  41 4.8  110     960   1100    .52  28   6.2  6.6 290 56 27    180 330   8.9   450   110    1.6   200   19     .21  39   2.2   42    4300 420   6.4  290 56   .60 59 5.2 210    540 3100   .77  35 9.1  32   590 240 900   1800 8400 29   590 220
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .39  42 3.8  79     1700   870    .48  29   5.4  7.0 300 65 27    180 320   8.8   450   130    1.6   200   23     3.1   130   38     60    4300 630   6.5  290 57   .61 78 4.2 750    670 8500   .91  33 7.8  34   590 250 900   1900 8300 29   560 220
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .37  42 3.7  82     1700   940    .48  28   5.7  6.8 300 56 26    180 320   8.7   450   120    1.6   200   21     3.1   130   47     59    4400 640   7.0  300 57   .60 78 4.1 750    680 9400   .92  33 9.2  32   590 240 900   1900 7700 29   560 220
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .39  41 3.7  84     1700   860    .47  28   6.3  6.7 300 58 28    180 390   8.9   450   120    1.6   200   21     3.1   130   40     80    4400 590   6.8  300 65   .55 60 4.1 750    670 8500   .93  33 9.3  32   570 250 900   1800 8900 29   620 240
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .38  41 4.0  78     1700   960    .48  29   6.4  7.1 310 55 26    180 410   8.6   450   110    1.6   200   20     3.1   130   45     72    4300 580   7.3  310 57   .63 78 4.9 750    680 8700   .92  33 9.8  31   570 290 900   1800 7600 27   590 230
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .39  42 3.6  82     1700   820    .52  29   5.4  7.0 300 61 27    180 330   8.9   450   120    1.6   200   21     3.9   130   55     71    4300 620   6.7  300 54   .54 59 4.6 750    670 8500   .91  33 9.6  32   590 270 900   1900 9100 30   590 220
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .37  41 5.5  82     1700   980    .47  29   7.0  6.7 300 59 26    180 380   8.7   450   110    1.6   200   20     3.1   130   42     59    4300 610   6.8  300 57   .50 59 5.1 750    670 8700   .86  33 9.7  31   590 240 900   1700 8000 28   570 210
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .37  42 4.4  83     1700   830    .48  29   5.0  6.8 310 54 26    180 320   8.6   450   100    1.6   200   22     3.0   130   40     85    4500 550   7.0  300 56   .50 60 6.1 750    680 8700   .86  33 11    31   560 260 900   1800 8400 28   580 230
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .38  42 3.3  81     1700   870    .47  28   6.7  6.8 300 56 27    180 340   9.2   450   120    1.6   200   20     3.0   130   38     58    4300 620   6.7  300 60   .60 78 4.5 750    650 10000   .91  33 9.8  32   590 240 900   1700 9700 29   590 220
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .38  42 4.5  82     1700   870    .47  28   5.6  7.0 300 62 27    180 340   8.9   450   110    1.6   200   21     3.1   130   43     61    4400 570   6.7  300 59   .55 59 4.1 750    670 11000   .87  33 11    33   570 260 900   2000 8400 29   590 220
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack .40  41 3.5  82     1700   990    .47  29   6.0  7.2 310 58 26    180 330   8.9   450   130    1.6   200   22     3.0   130   38     55    4400 610   7.1  310 64   .57 58 5.1 750    670 8500   .88  33 9.8  32   590 260 900   1800 6500 28   570 210
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 120     2200 1700    880     680   12000    .13  8.5 .96 970   11000 5900 900    340 12000   900     680   8100    900     670   8100     900     360   10000     900    170 12000   970    11000 7000   .62 52 7.0 750    290 7300   900     4400 6100    900   1700 11000 900   1000 9100 900   1800 11000
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.5   82 33    250     15000   3000    .11  8.4 1.2  900   9300 4800 900    1100 11000   900     440   9100    900     440   8000     900     2500   11000     900    75 10000   920    9300 4700   .77 40 7.0 880    240 7900   900     6200 9200    900   1300 12000 900   940 7600 900   2100 11000
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 61     1000 550    880     3700   10000    .14  8.3 .94 920   11000 6000 900    350 13000   900     1600   7700    900     1600   7900     900     420   11000     900    170 10000   930    11000 6900   900    860 5900   750    260 5800   900     4800 8100    900   2300 10000 900   1000 9000 900   800 11000
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 10     270 120    880     4100   13000    .13  9.6 1.2  970   11000 5700 900    230 11000   900     420   8200    900     430   7600     900     520   12000     900    170 10000   960    11000 5700   .64 36 7.2 880    310 8000   460     3200 3200    900   970 10000 900   1000 8900 900   960 11000
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 44     930 590    880     2600   7800    .12  8.9 1.1  930   11000 6400 900    330 11000   900     440   8000    900     440   8300     900     440   9700     900    180 11000   970    11000 5500   900    3200 5300   750    300 7200   550     4000 4000    900   2100 12000 900   960 6400 900   790 9900
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 54     990 540    880     2800   6400    .12  8.1 1.1  970   11000 6300 890    310 12000   900     440   8400    900     450   8200     900     490   11000     900    180 11000   970    11000 6300   900    3100 4900   750    300 7800   570     3900 3800    900   2400 9800 900   1000 7000 900   730 12000
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 64     910 650    880     5300   13000    .17  9.4 1.3  920   11000 5800 900    590 10000   900     510   9100    900     510   7800     900     990   13000     900    170 9700   910    11000 6200   .70 38 7.7 880    310 8000   900     4000 11000    900   960 7600 900   940 6700 900   920 10000
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 47     570 410    880     1500   7800    .12  9.4 1.4  910   11000 6800 900    310 11000   900     790   7400    900     790   8000     900     710   12000     900    180 9600   900    11000 6200   .66 40 6.5 750    320 6600   900     4800 5300    900   2100 7300 900   950 6700 900   750 10000
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.2   60 14    880     610   9500    .11  8.0 1.0  940   11000 6200 900    270 11000   900     400   8600    900     400   8700     900     590   12000     900    170 10000   960    11000 6200   .52 49 5.6 880    330 9100   900     1400 9000    900   1400 12000 900   1000 7400 900   1300 13000
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 25     510 270    880     600   10000    .11  8.2 1.0  910   11000 6400 900    350 13000   900     500   8100    900     500   8900     900     360   11000     900    180 9400   900    11000 6300   900    310 6800   750    280 7500   900     4400 5800    900   1800 11000 900   1000 7600 900   1600 9300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 51     840 400    880     1100   6100    .13  8.4 1.0  900   10000 4700 900    260 12000   900     970   7700    900     970   9100     900     200   12000     900    160 11000   920    11000 4900   .73 37 6.7 750    340 5400   900     3800 4900    900   2200 9700 900   1000 8000 900   1200 13000
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.5   54 19    220     15000   2800    .12  7.8 .95 910   9300 4600 900    1100 12000   900     430   8200    900     430   9000     900     2400   12000     900    74 10000   900    9300 5000   .74 37 8.0 880    240 6100   900     6100 7100    900   890 11000 900   990 8100 900   1800 9800
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 30     640 420    870     3900   11000    .17  7.4 1.4  920   11000 6100 900    340 10000   900     1000   7300    900     1000   8200     900     410   11000     900    170 9600   900    11000 7500   900    720 6100   750    240 8900   900     4600 5500    900   2300 9900 900   1000 8700 900   1000 9900
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 5.8   150 61    880     4200   12000    .12  9.0 1.4  970   11000 5800 900    220 11000   900     420   7800    900     420   7500     900     450   12000     900    180 11000   960    11000 5500   .63 38 7.1 880    300 8800   480     3200 4000    900   1100 10000 900   1000 6500 900   1000 12000
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 20     530 200    880     2100   12000    .13  8.5 1.1  920   11000 6400 900    320 12000   900     430   9100    900     430   8200     900     410   11000     900    190 11000   910    11000 7500   900    3200 5300   750    290 6200   900     5000 6400    900   1100 11000 900   1200 11000 900   970 13000
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 24     590 270    880     1300   8300    .10  7.6 1.4  970   12000 7300 900    300 13000   900     430   7600    900     430   7800     900     400   12000     900    190 11000   910    12000 6900   900    3200 6500   750    300 6600   900     4900 5600    900   2200 9600 900   1000 7600 900   1000 10000
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 22     420 270    880     2400   11000    .11  8.6 1.0  930   11000 6800 900    460 12000   900     460   8400    900     460   8500     900     870   9900     900    180 11000   940    11000 6400   .69 39 7.8 880    330 7800   900     4200 10000    900   2200 9400 900   980 6800 900   950 11000
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 24     340 190    880     2000   9200    .11  8.4 1.1  920   11000 7000 900    330 12000   900     640   7600    900     640   8200     900     710   11000     900    190 12000   920    11000 6400   .67 39 7.0 750    340 8100   900     4800 5400    900   2400 8700 900   1100 7900 900   920 9900
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .70  34 8.1  880     500   10000    .12  7.6 .95 930   11000 6600 900    240 10000   900     400   9300    900     400   7700     900     460   11000     900    190 9700   920    11000 5700   .61 49 4.3 880    290 9200   900     1700 10000    900   2300 13000 900   1000 5400 900   2100 10000
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack 6.1   210 84    .18  15   2.2  .11  8.4 1.7  930   12000 7400 .81 36 9.8 8.5   450   110    8.5   440   97     .43  30   5.1   900    180 11000   910    11000 6600   .24 37 2.1 5.3  110 72   .28  19 3.2  80   780 660 490   990 4200 900   800 11000
forester-heap/sll-01_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack 7.0   230 81    .16  11   1.8  .10  8.2 1.1  930   11000 5600 .22 34 2.5 8.5   450   120    8.6   450   120     .17  27   2.2   .49 83 5.1 970    11000 6500   .17 36 1.5 5.6  110 74   .29  22 3.8  30   810 280 470   940 3800 35   820 310
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack 2.8   110 31    .14  11   1.7  .11  8.2 1.0  920   12000 7400 .80 36 9.8 8.5   450   130    8.5   450   100     .42  30   5.5   900    190 9700   910    11000 8100   .23 35 2.0 4.9  99 60   .31  18 3.5  54   920 500 410   790 4000 900   1000 11000
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.9   97 40    .33  8.8 3.8  870     12000   13000    4.2 280 39 1.1  37 17   8.3   390   100    8.4   390   110     .22  27   2.7   46    4300 520   4.4  290 38   .33 49 1.4 12    96 170   .22  16 2.9  900   960 14000 900   1000 8600 900   1800 12000
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 3.1   99 39    .34  8.9 3.6  870     7100   14000    4.2 290 35 1.2  37 14   8.1   390   120    8.4   380   110     .25  27   3.5   52    4500 470   4.2  280 36   .18 37 1.4 12    96 160   .21  16 2.2  900   1100 11000 900   1000 8300 900   2300 11000
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 5.0   140 59    .32  8.7 3.7  880     12000   11000    4.3 280 44 1.2  38 13   8.4   390   110    8.3   390   98     .22  27   2.6   45    4300 460   4.4  290 39   .35 49 1.5 12    100 150   .22  16 2.6  900   1100 12000 900   900 7900 900   980 14000
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 3.8   120 57    .35  9.5 4.8  870     7200   11000    4.4 290 38 1.2  39 15   8.3   390   110    8.3   390   110     .25  27   2.6   62    4300 460   4.3  280 38   .18 37 1.5 12    110 170   .27  17 2.3  900   870 13000 900   1100 7400 900   860 12000
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.1   49 18    .32  8.5 4.0  880     12000   11000    4.2 280 36 1.1  36 13   8.2   390   100    8.3   390   98     .22  27   2.5   47    4300 500   4.4  280 38   .18 36 1.3 12    98 140   .21  16 2.8  900   930 13000 900   1100 7700 900   1100 11000
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.1   50 16    .31  8.8 4.2  880     7200   10000    4.1 290 36 1.1  37 16   8.2   390   110    8.5   380   100     .25  27   2.6   63    4400 450   4.3  280 44   .16 37 1.5 12    98 150   .22  17 2.5  900   960 10000 900   920 7400 900   1700 11000
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 7.5   370 91    .27  7.4 3.3  1.5   16   18    4.0 280 33 .48 35 6.7 8.2   390   100    8.6   390   110     .17  27   1.9   57    4400 410   4.1  280 36   .37 49 1.3 9.1  91 120   .23  16 2.3  900   1300 11000 900   950 8600 900   1100 12000
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.2   56 14    .29  7.2 3.3  1.7   16   23    4.2 280 35 .91 37 12   8.3   390   130    8.5   380   120     .17  27   2.1   43    4300 470   4.1  280 41   .31 49 1.6 9.0  91 130   .20  17 2.5  900   1300 13000 900   970 10000 900   1000 13000
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 8.9   180 110    .23  7.7 3.3  710     5800   10000    4.3 280 38 .98 39 12   8.5   390   100    8.3   390   110     .20  27   2.0   44    4400 450   4.2  280 37   .16 36 1.6 9.1  98 140   .24  15 2.9  300   1200 3600 900   1100 6700 910   14000 5300
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 22     300 230    .25  7.7 2.7  720     5800   8200    4.3 280 38 1.0  38 12   8.5   380   110    8.5   390   100     .17  27   2.1   60    4500 450   4.3  280 32   .19 37 1.3 9.0  97 120   .21  16 2.3  320   1100 4400 900   1100 7000 910   14000 7100
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 15     330 180    .29  9.9 3.9  880     14000   12000    4.3 280 34 1.4  37 21   8.3   390   94    8.3   390   110     .42  27   5.1   60    4400 510   4.3  290 37   .18 36 1.4 14    110 170   .22  16 2.6  720   2300 9300 900   1000 7800 900   1100 13000
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 13     300 150    .32  10   3.5  880     15000   12000    4.1 260 35 1.4  39 17   8.2   390   110    8.3   390   120     .41  28   4.9   58    4400 530   4.2  280 37   .19 36 1.2 15    110 210   .21  16 2.5  900   1100 12000 900   1000 8000 820   2300 10000
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 17     340 160    .30  9.4 3.5  650     6300   9000    4.2 280 40 1.5  37 20   8.4   390   97    8.3   390   100     .40  28   5.0   58    4400 450   4.3  290 34   .30 49 1.5 12    100 160   .21  16 2.5  900   1200 10000 900   950 9000 900   900 13000
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 43     580 450    .32  11   4.9  640     6200   7800    4.5 290 38 1.5  39 18   8.2   390   93    8.1   390   93     .43  28   6.0   54    4400 460   4.3  280 34   .18 37 2.3 13    110 170   .22  16 3.1  900   2400 10000 900   950 7500 900   960 14000
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.2   87 27    .27  9.2 3.4  290     2800   3500    4.3 280 34 1.4  37 17   8.4   390   100    8.3   390   100     .37  27   5.1   53    4300 440   4.1  260 35   .17 37 1.3 11    98 130   .24  16 2.6  900   1300 13000 900   1000 7900 900   1000 9200
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.4   96 32    .28  9.7 3.7  290     2800   3400    4.2 280 37 1.4  37 16   8.3   390   92    8.3   390   110     .38  27   5.1   53    4500 590   4.2  280 35   .18 35 2.2 11    97 170   .21  16 2.5  900   860 13000 900   1000 8200 900   1600 14000
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.4   94 25    .27  9.4 3.1  24     98   300    4.2 280 38 .85 37 11   8.3   390   99    8.3   380   130     .15  26   2.1   50    4300 440   4.1  280 33   .16 36 1.5 9.0  90 120   .21  17 2.2  900   1100 13000 900   1000 7100 900   1600 12000
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .66  35 8.0  .24  6.9 2.3  2.6   27   35    4.2 280 34 .78 36 9.8 8.4   380   100    8.6   380   120     .16  27   1.5   48    4400 530   4.1  280 35   .19 35 4.0 8.1  86 88   .20  17 2.4  150   890 1900 900   1000 8200 900   1600 12000
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 80     740 680    .23  7.8 2.4  230     1900   3300    4.1 260 35 .87 37 11   8.4   380   100    8.4   380   110     .17  27   1.6   40    4400 440   4.2  280 41   .29 49 1.5 8.1  93 110   .21  16 2.7  900   2400 13000 400   1100 4000 830   1200 8900
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 82     690 670    .24  8.3 2.7  260     2200   3200    4.2 280 36 .87 38 12   8.4   380   97    8.3   380   120     .16  27   1.7   65    4500 480   4.4  280 40   .17 35 1.3 8.5  95 110   .21  17 2.4  900   1600 11000 900   1000 6800 900   1100 10000
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.1   72 26    .29  8.9 3.7  440     15000   6300    4.2 280 35 1.2  38 15   8.3   390   120    8.3   390   120     .22  27   2.5   73    4400 460   4.3  280 35   .26 49 3.7 10    100 140   .21  16 2.5  900   1200 13000 900   980 7200 860   2200 9900
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 4.2   110 65    .34  9.5 4.0  400     15000   5100    4.3 280 38 1.3  38 16   8.4   390   100    8.4   380   100     .22  27   3.6   48    4400 480   4.3  280 41   .16 35 1.6 11    98 130   .23  16 2.8  900   1900 12000 900   950 8500 840   2300 10000
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.1   73 28    .28  8.2 3.5  880     12000   11000    4.1 280 35 1.1  37 15   8.4   390   110    8.3   390   110     .21  27   2.8   44    4500 460   4.3  280 35   .34 49 1.3 9.5  99 110   .21  16 2.5  900   1300 13000 900   920 8300 900   790 13000
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 3.3   97 39    .31  8.7 3.7  780     6500   12000    4.3 280 35 1.2  38 15   8.2   390   99    8.3   390   100     .25  27   2.6   56    4300 440   4.4  280 40   .19 37 2.6 9.7  93 120   .22  16 2.3  900   1300 13000 900   880 8000 900   810 12000
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.8   65 19    .29  9.0 3.8  440     15000   6500    4.2 280 38 1.1  37 16   8.3   380   120    8.2   380   120     .22  27   2.7   46    4400 560   4.3  280 40   .18 37 1.6 10    100 110   .21  16 2.6  900   1800 12000 900   1000 10000 900   1300 11000
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.6   63 18    .30  9.1 4.7  510     15000   7200    4.0 260 38 1.1  37 14   8.3   390   100    8.5   390   94     .24  27   2.2   60    4400 440   4.3  290 38   .20 37 1.3 9.9  100 140   .21  16 2.7  900   1700 9100 900   980 8300 900   1400 12000
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .84  40 12    .34  9.3 3.4  880     3700   12000    4.2 280 39 1.1  42 14   8.3   390   96    8.2   390   98     .18  27   2.4   43    4400 440   4.1  280 39   .15 36 1.5 8.4  96 93   .20  16 2.4  900   750 11000 900   960 7900 900   730 11000
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .91  43 10    .27  8.3 2.7  31     150   450    4.2 280 34 .99 38 14   8.2   390   100    8.4   390   110     .17  27   2.2   77    4300 410   4.0  280 37   .16 36 1.5 8.3  90 130   .20  16 2.4  380   820 4000 900   1000 8800 900   730 12000
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 5.1   120 72    .22  7.4 3.0  660     5500   6200    4.5 290 35 .95 38 13   8.3   390   110    8.3   390   100     .17  27   2.3   68    4500 430   4.1  290 41   .21 49 1.8 8.3  93 110   .21  17 2.4  900   910 11000 850   1000 7100 910   13000 5300
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 7.2   130 72    .23  7.7 2.9  630     5500   9100    4.1 290 41 .95 39 13   8.4   390   99    8.3   390   120     .17  27   2.0   49    4400 530   4.2  280 30   .26 49 1.9 8.3  93 100   .21  17 2.7  900   990 12000 900   930 6700 910   12000 10000
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 5.8   170 71    .27  10   3.1  880     13000   11000    4.1 260 34 1.4  37 18   8.4   390   110    8.3   390   120     .38  27   5.0   53    4400 460   4.1  280 38   .17 36 1.3 11    97 160   .20  17 2.4  900   2200 11000 900   1000 7800 900   1600 11000
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 5.2   160 65    .29  10   3.3  880     13000   11000    4.2 280 37 1.5  38 17   8.3   380   100    8.3   390   120     .40  27   5.4   69    4500 510   4.2  290 35   .18 35 1.3 12    100 140   .21  16 2.5  840   2200 11000 900   1000 9600 900   2200 11000
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 6.4   180 82    .25  9.3 3.2  290     2800   3500    4.4 280 38 1.4  37 16   8.4   390   98    8.3   390   120     .37  27   5.2   72    4400 390   4.4  290 38   .19 36 1.3 11    96 140   .21  17 2.5  900   920 11000 900   910 7400 900   1100 11000
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 18     320 200    .28  10   3.4  280     2800   4000    4.4 280 40 1.4  38 21   8.3   390   120    8.5   390   97     .40  27   5.9   56    4400 530   4.3  290 41   .17 36 1.4 12    100 170   .21  16 2.6  900   1100 10000 900   830 8000 900   990 12000
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.3   59 17    .24  8.6 3.5  270     2600   3900    4.2 280 34 1.3  37 17   8.2   390   110    8.2   390   110     .36  27   4.9   49    4500 520   4.2  280 37   .18 37 1.4 10    93 120   .23  16 2.0  900   1200 11000 900   910 9400 900   1400 10000
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.3   56 16    .26  9.5 3.9  270     2600   3400    4.0 280 36 1.3  37 17   8.2   390   94    8.3   390   110     .39  27   4.1   69    4400 450   4.3  280 41   .18 36 1.3 5.5  94 65   .20  16 2.4  900   1200 11000 900   1000 7900 900   1000 11000
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.6   71 20    .24  9.3 3.0  21     98   280    4.2 280 40 .86 37 11   8.4   390   110    8.3   380   110     .15  26   1.8   44    4400 540   4.1  280 33   .16 37 1.5 9.1  91 130   .21  16 2.2  900   1100 10000 900   910 8200 900   860 14000
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack .40  30 4.6  .19  6.7 1.9  .65  12   10    4.1 280 37 .75 36 9.2 8.4   380   130    8.2   380   110     .15  27   1.7   49    4300 520   4.2  270 37   .17 35 1.3 7.8  85 95   .20  17 2.3  320   800 4000 250   1000 2600 900   1200 11000
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 35     390 280    .22  7.9 2.8  230     2200   3300    4.2 280 40 .86 38 11   8.4   390   96    8.2   390   99     .14  27   2.0   51    4500 550   4.3  280 34   .16 36 1.4 8.4  95 89   .23  16 2.6  470   1100 5400 900   940 6800 900   1100 11000
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 41     410 320    .20  8.1 2.7  230     2200   2900    4.3 280 37 .86 37 11   8.3   380   99    8.3   390   110     .14  27   1.6   53    4400 450   4.2  260 40   .16 35 1.4 8.6  94 120   .21  16 2.4  590   920 8200 900   990 8700 900   1200 9800
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 4.0   87 47    .29  9.9 3.2  19     160   290    4.7 290 38 2.4  38 29   8.4   390   120    8.2   390   120     .59  27   7.2   81    4300 720   4.2  280 39   .39 36 4.3 21    130 300   .20  16 2.6  900   2400 9200 900   1100 8700 900   1200 11000
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i valid-deref valid-free valid-memtrack .78  37 8.7  .21  7.3 2.3  .087 8.1 .94 4.2 280 37 .96 36 12   8.3   380   94    8.4   390   98     .24  27   2.5   130    4400 1400   4.2  290 36   .16 36 1.7 8.6  88 110   .25  18 2.9  900   1900 6300 390   1000 4500 900   2000 6700
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.5   75 30    .32  12   3.8  880     7400   11000    4.4 290 38 2.8  39 38   8.3   390   100    8.4   390   110     .71  27   11     93    4400 720   4.0  270 36   .18 48 2.3 38    150 530   .25  16 2.3  900   2000 13000 900   1200 6900 900   1100 11000
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.8   52 23    .26  8.8 2.7  15     150   190    4.1 270 37 2.4  39 32   8.3   390   87    8.2   390   97     .61  27   8.1   73    4300 700   4.5  280 34   .33 49 1.2 18    110 220   .20  16 2.3  900   1100 12000 900   990 7900 900   940 11000
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 150     15000 1100    5.4   78   72    870     7100   12000    21   1200 150 740    440 8500   9.0   390   100    8.9   390   100     340     260   3800     900    4300 7400   18    980 130   1.8  50 19   880    310 8100   .47  18 5.7  900   2500 9700 900   890 7700 900   1900 14000
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 260     15000 2600    18     230   250    760     15000   11000    280   5900 2100 900    2400 10000   9.4   390   110    9.2   390   100     100     250   1300     900    4400 8100   270    5800 2400   .74 61 7.4 750    270 8600   1.8   44 23    900   1300 13000 900   970 9200 900   1200 14000
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack 900     4300 11000    880     4000   12000    .084 9.2 .81 910   7000 5500 900    3300 8000   230     510   2400    240     510   2100     900     1300   9400     900    4000 12000   920    7200 5100   4.4  86 41   750    420 9200   6.3   100 81    900   800 12000 900   1000 7200 900   910 12000
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i valid-deref valid-free valid-memtrack .19  26 1.8  .097 6.9 .87 .13  8.8 1.9  4.0 280 35 .43 35 5.1 8.3   450   86    8.3   450   100     .12  26   1.3   100    4300 1200   3.8  280 33   .14 35 1.1 6.7  78 92   .18  15 2.0  15   560 130 50   720 550 71   530 880
list-ext3-properties/dll_circular_traversal_false-valid-deref.i valid-deref valid-free valid-memtrack 4.4   90 41    .23  9.6 2.8  880     15000   12000    4.7 280 39 3.1  40 41   8.6   450   120    8.4   450   100     .72  27   11     .49 83 6.3 4.8  280 40   .16 35 1.6 15    130 200   .22  17 2.7  900   2400 10000 900   1100 8700 900   2200 10000
list-ext3-properties/sll_circular_traversal_false-valid-deref.i valid-deref valid-free valid-memtrack 2.0   54 26    .23  9.0 2.3  830     15000   11000    4.6 290 41 2.9  39 37   8.4   450   110    8.4   450   100     .69  27   9.4   .47 83 5.5 4.6  270 38   .19 50 2.3 14    110 190   .23  16 2.9  900   850 12000 900   1100 8900 900   900 10000
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i valid-deref valid-free valid-memtrack .74  37 9.0  .18  6.9 2.6  .079 9.2 1.2  4.2 290 36 .92 36 11   8.5   450   99    8.6   450   130     .20  27   2.0   .47 83 5.9 4.4  280 40   .39 51 1.4 9.3  88 110   .30  17 3.0  260   990 2900 180   1000 1500 410   950 5100
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i valid-deref valid-free valid-memtrack .19  26 1.7  .078 6.7 .80 .091 8.5 .83 3.9 280 33 .18 34 2.0 8.6   450   100    8.5   440   110     .10  26   1.2   .44 83 6.6 3.8  280 34   .15 35 1.5 7.4  86 89   .26  16 2.3  35   510 370 19   500 170 36   620 370
loops/invert_string_false-valid-deref.c valid-deref valid-free valid-memtrack .12  24 1.1  .077 7.7 .51 .14  9.2 .52 2.7 240 22 .15 33 1.6 8.2   430   98    1.6   200   21     .11  26   .86  .46 83 6.5 2.7  240 24   .16 48 1.7 3.5  88 43   .75  18 7.9  8.3 350 63 9.4 380 80 8.0 360 63
loop-acceleration/array3_false-valid-deref.i valid-deref valid-free valid-memtrack 810     15000 5600    14     610   180    78     660   600    900   1600 11000 120    49 1800   8.8   430   93    8.4   430   89     19     370   280     900    4600 6500   900    1500 12000   900    88 11000   760    1300 4800   13     21 190    900   850 9700 900   1900 7200 900   2400 11000
ntdrivers/floppy_false-valid-deref.i.cil.c valid-deref valid-free valid-memtrack 1.0   61 11    4.4   150   94    1.7   67   20    11   550 100 5.7  390 74   1.3   170   16    1.3   170   16     900     750   12000     .92 41 11   11    570 110   1.2  90 11   46    300 600   1.9   110 26    69   1400 560 64   1600 570 53   1100 460
ntdrivers/kbfiltr_false-valid-deref.i.cil.c valid-deref valid-free valid-memtrack .31  38 3.1  .74  22   12    .38  21   5.6  5.6 290 46 24    380 330   1.2   170   14    1.2   170   16     9.0   380   110     .80 40 10   5.3  290 48   .40 48 3.2 6.8  140 89   .94  31 13    26   830 240 25   770 200 27   800 230
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack 1.5   420 17    .93  31   10    7.4   140   110    33   1700 260 1.8  66 21   8.3   430   110    1.6   200   20     .54  42   6.6   900    4500 6900   32    1600 300   2.2  120 22   320    320 4300   1.0   120 13    12   460 90 25   690 210 13   460 90
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack 1.4   420 20    .91  31   11    7.3   140   90    36   1800 270 1.8  67 21   8.5   430   99    1.6   200   22     .54  42   8.3   900    4400 9000   32    1500 280   2.3  120 22   320    320 4000   1.0   120 11    12   480 98 23   810 210 12   450 90
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .47  110 5.2  880     5600   3100    880     690   11000    900   7300 8700 1.1  67 13   8.4   430   99    1.6   200   23     .38  31   4.5   900    4400 7600   900    7400 9500   65    590 690   160    220 2200   .44  39 5.1  11   390 88 21   790 180 10   360 77
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .35  72 4.1  .22  9.8 2.9  2.5   100   31    55   3200 470 1.1  65 14   8.3   430   120    1.6   200   19     .21  31   2.3   900    4300 8400   54    3400 490   7.1  130 75   150    220 1700   .39  36 4.5  8.9 360 68 14   560 110 11   380 84
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .37  72 3.7  .22  9.8 2.6  2.5   100   30    51   3300 480 1.2  66 14   8.5   430   110    1.6   200   21     .20  31   2.3   900    4400 7800   59    3400 560   7.2  130 71   150    220 1900   .38  36 4.7  10   370 85 14   510 100 11   370 87
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .58  140 6.7  .47  16   7.6  5.6   180   73    88   4300 770 1.3  65 17   8.3   430   100    1.6   200   23     .31  33   3.8   900    4300 10000   85    4400 760   8.2  150 85   230    270 3100   .53  52 6.6  11   390 87 16   530 120 12   430 88
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .55  140 6.3  .46  16   7.1  5.4   170   66    92   4300 730 1.4  66 16   8.4   430   98    1.6   200   19     .31  33   4.0   900    4300 9300   89    4400 790   8.6  170 79   230    260 3400   .53  52 6.6  11   430 84 16   600 130 11   410 92
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .19  26 1.5  .17  6.2 1.8  .54  15   6.9  7.6 420 67 .88 66 8.9 8.2   430   97    1.6   200   20     .12  28   1.3   810    4400 7500   7.8  430 65   .82 47 8.5 32    130 520   .24  17 3.1  8.9 370 65 12   500 97 9.3 380 78
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .31  47 3.8  .17  9.0 2.1  1.0   21   14    19   760 150 1.0  67 12   8.4   430   100    1.6   200   18     .16  30   1.9   900    4400 9500   16    670 120   1.7  70 16   62    170 1000   .31  22 5.0  9.9 380 87 15   600 120 10   380 73
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack .26  47 2.8  .18  8.9 2.0  1.0   21   13    19   750 150 1.0  66 12   8.3   430   120    1.6   200   20     .15  30   2.0   900    4300 9200   15    680 120   2.2  72 22   64    170 950   .31  22 3.8  10   380 73 13   570 110 9.7 380 82
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .11  24 1.0  870     870   8100    140     15000   1600    900   11000 5600 .96 65 10   8.3   430   110    900     410   9200     .12  27   1.5   900    3900 8100   920    11000 4700   170    360 1800   7.2  87 91   .20  17 2.4  7.6 360 57 8.7 360 69 7.6 350 66
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .12  24 1.2  880     1000   9200    130     15000   1600    920   11000 4400 1.0  67 10   8.3   430   110    900     400   8400     .12  27   1.6   900    4300 8500   900    11000 5500   820    1500 7900   7.7  85 110   .21  16 2.7  8.5 370 61 9.0 370 76 8.1 370 66
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .12  25 1.2  880     1200   8300    130     15000   1800    930   11000 4900 1.1  66 12   8.1   430   120    900     400   8600     .16  27   1.4   900    4300 9600   970    11000 4900   900    1300 8100   8.4  87 100   .21  16 2.3  8.2 360 63 9.3 370 70 8.0 400 63
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .13  25 1.7  880     1400   9200    120     15000   1700    930   11000 4700 1.1  67 10   8.0   430   100    900     400   9000     .14  27   1.7   900    4300 11000   910    11000 4500   900    1100 8100   11    88 130   .21  16 2.4  7.9 370 63 7.6 350 69 8.3 370 65
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .17  24 1.2  880     460   9700    240     15000   3500    920   6300 7900 1.2  71 13   8.3   430   80    900     410   9400     .15  27   2.1   900    4300 11000   900    5400 7600   900    1100 7800   7.1  87 93   .21  16 2.5  7.5 340 54 8.6 370 64 8.1 360 64
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .13  24 1.1  880     1400   9300    100     15000   1200    920   11000 4700 1.1  67 13   8.2   430   95    900     400   9200     .17  27   1.8   900    4300 9900   910    11000 5500   900    1000 9800   14    87 200   .21  16 2.7  8.4 370 62 8.7 360 67 8.1 370 61
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .13  25 1.1  880     520   10000    82     15000   1100    910   4200 7200 1.2  78 12   8.3   430   120    900     410   8000     .16  27   1.8   900    4200 12000   900    4400 7800   900    1100 8300   7.2  87 87   .21  16 2.6  8.6 360 68 9.7 370 74 8.3 370 69
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .12  25 1.3  880     460   9000    83     15000   1200    930   11000 5300 1.2  73 15   8.5   430   110    900     400   10000     .17  27   1.8   900    4300 9800   930    11000 5900   900    960 8000   24    89 330   .21  16 2.3  7.1 320 61 8.3 360 71 8.3 350 61
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .10  24 .88 880     950   7600    130     15000   1800    900   11000 4600 .88 65 10   8.4   430   84    420     480   4600     .097 26   1.0   900    4300 9300   970    11000 4800   .69 52 5.3 6.6  82 82   .19  16 2.7  7.0 340 52 7.8 360 64 7.7 370 67
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .13  24 .92 880     1300   9000    83     15000   1000    930   11000 5100 .89 66 11   8.4   430   98    900     430   8500     .098 26   1.2   900    4300 8200   910    11000 5100   1.9  42 18   6.6  78 79   .19  17 2.2  7.8 360 64 8.2 370 63 7.3 340 59
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .11  24 1.0  880     1500   9500    89     15000   1200    910   11000 4900 .87 66 11   8.2   430   100    900     420   8600     .11  26   1.3   900    3800 9000   900    11000 5100   6.9  80 67   6.7  79 76   .22  16 2.5  8.1 360 60 8.5 370 61 7.8 370 67
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .11  24 1.4  880     580   8600    110     15000   1500    920   11000 5000 .93 65 9.7 8.2   430   110    900     410   9400     .12  26   1.2   900    4300 7800   970    11000 5100   17    85 160   6.9  80 82   .21  16 2.5  7.1 340 53 8.1 340 59 8.3 370 64
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack .13  24 .87 870     710   8700    160     15000   2200    930   11000 5500 .95 65 10   8.2   430   100    900     410   8900     .13  26   1.3   900    4300 8000   970    11000 5600   44    120 490   7.0  86 75   .20  17 2.1  7.7 360 64 8.3 360 77 7.1 330 58
memsafety-ext3/derefAfterFree1_false-valid-deref.c valid-deref valid-free valid-memtrack .15  24 1.3  .076 7.6 .54 .068 8.0 .62 2.7 240 22 .15 33 1.6 8.3   430   100    8.4   430   110     .084 26   1.0   .43 83 5.0 2.8  250 30   .25 48 1.4 2.8  75 38   .18  16 1.7  8.6 380 69 8.0 340 60 7.6 360 64
memsafety-ext3/derefAfterFree2_false-valid-deref.c valid-deref valid-free valid-memtrack .16  25 1.2  .21  7.6 1.3  .17  8.0 1.9  2.9 240 29 1.6  36 19   8.1   430   110    8.0   430   110     .15  26   1.8   .46 83 5.0 3.0  250 26   .15 34 1.6 3.0  82 38   .17  15 1.8  11   460 91 40   730 350 11   510 83
memsafety-ext3/derefInLoop1_false-valid-deref.c valid-deref valid-free valid-memtrack .084 24 .71 .13  6.5 .41 .073 6.9 .47 2.9 250 22 .79 66 8.5 7.9   370   110    8.1   370   93     .084 26   .83  340    4300 3700   2.8  250 28   .14 35 1.4 .44 24 6.5 .17  16 1.6  8.3 380 71 7.6 350 62 8.8 390 73
memsafety-ext3/getNumbers1_false-valid-deref.c valid-deref valid-free valid-memtrack .089 24 .90 .28  8.1 1.9  .22  8.8 1.7  3.0 240 28 3.3  68 41   8.1   430   94    8.2   430   100     .19  26   2.1   110    4400 1400   3.1  250 26   .26 47 1.8 .45 24 5.6 .24  17 2.6  14   540 99 18   720 140 13   490 110
memsafety-ext3/getNumbers2_false-valid-deref.c valid-deref valid-free valid-memtrack .082 24 1.0  .11  7.3 1.1  .21  7.3 .84 3.6 280 29 .79 67 8.2 8.0   430   89    8.1   430   110     .091 26   .82  110    4400 1100   3.5  280 29   .21 35 1.4 .46 24 6.4 .18  16 1.8  22   550 190 60   1100 630 25   730 220
memsafety-ext3/getNumbers4_false-valid-deref.c valid-deref valid-free valid-memtrack .089 24 .83 .16  7.0 1.7  .15  7.3 2.0  3.4 250 30 3.9  67 56   8.3   430   94    8.4   430   110     .21  27   2.4   110    4400 1100   3.4  250 29   .46 48 1.8 .48 24 5.8 .18  15 2.0  59   770 590 320   1100 3400 60   900 620
memsafety-ext3/naturalNumbers1_false-valid-deref.c valid-deref valid-free valid-memtrack .085 24 .87 .079 7.0 .69 .15  6.9 .47 2.9 240 29 .57 35 8.0 8.1   430   92    8.2   430   100     .095 26   1.1   .44 82 5.7 2.8  250 29   .19 35 1.3 .46 23 5.2 .17  15 1.9  9.8 390 77 11   490 110 10   410 92
memsafety-ext3/realloc1_false-valid-deref.c valid-deref valid-free valid-memtrack .19  24 1.4  .19  7.6 1.9  .12  6.8 .44 3.1 240 28 2.6  36 31   8.3   430   100    1.5   200   18     .20  26   2.4   .74 39 11   3.0  250 28   .15 35 1.3 3.4  85 41   .19  16 3.2  15   550 120 71   1000 810 15   600 130
memsafety-ext3/scopes1_false-valid-deref.c valid-deref valid-free valid-memtrack .097 24 .84 .064 7.8 .35 .092 7.7 .27 2.9 250 25 .82 67 8.5 8.2   430   98    8.1   430   120     .082 26   .84  180    4300 2000   2.8  250 26   .15 34 1.4 .44 24 5.0 .16  16 2.0  7.8 360 71 8.1 350 65 7.9 370 57
memsafety-ext3/scopes2_false-valid-deref.c valid-deref valid-free valid-memtrack .11  24 .80 .057 7.4 .34 .066 7.2 .38 2.7 250 25 .15 34 1.5 8.4   430   98    8.5   430   120     .11  26   .96  .45 83 5.7 2.7  250 27   .36 48 1.3 .45 24 5.4 .22  18 2.5  7.6 350 60 7.4 350 55 8.1 370 61
memsafety-ext3/scopes3_false-valid-deref.c valid-deref valid-free valid-memtrack .091 24 .68 .12  7.1 1.0  .12  7.5 1.2  3.0 250 27 .79 65 8.2 8.1   430   100    8.2   430   120     .11  26   .90  370    4300 4000   3.1  250 26   .15 34 1.2 .44 24 6.2 .16  16 2.0  12   480 110 13   500 110 13   570 120
memsafety-ext3/scopes4_false-valid-deref.c valid-deref valid-free valid-memtrack .091 24 .79 .066 11   .76 .073 11   .56 2.7 250 24 .83 67 8.4 8.0   430   96    8.1   430   110     .078 26   .97  150    4400 1500   2.8  250 29   .19 34 1.3 .45 24 6.2 .16  16 1.9  8.7 370 66 8.6 370 72 8.6 370 67
memsafety-ext3/scopes5_false-valid-deref.c valid-deref valid-free valid-memtrack .085 24 .77 .060 7.1 .39 .12  7.1 .29 2.8 250 28 .81 67 8.6 8.1   430   93    8.2   430   110     .081 26   .86  500    4300 5300   2.7  250 29   .29 48 1.6 .47 24 5.6 .15  16 2.0  7.7 350 67 7.6 370 67 6.9 330 57
memsafety-ext3/freeAlloca_false-valid-free.c valid-deref valid-free valid-memtrack .16  24 1.6  .24  9.0 1.5  .24  9.1 2.8  2.9 250 29 3.1  68 37   8.2   430   92    8.3   430   110     .15  26   2.1   .83 86 12   3.0  250 30   .32 47 1.8 .45 24 5.8 .23  18 2.8  13   430 140 27   680 290 17   480 160
memsafety-ext3/getNumbers1_true-valid-memsafety.c valid-deref valid-free valid-memtrack .093 24 .67 .10  6.6 .81 .093 6.5 .64 3.0 250 29 2.7  68 37   8.3   370   100    8.2   370   120     .12  26   1.0   200    4300 2000   3.0  250 27   .18 35 1.4 .46 24 5.6 .14  15 1.4  12   530 110 25   800 230 12   500 94
memsafety-ext3/getNumbers3_true-valid-memsafety.c valid-deref valid-free valid-memtrack .091 24 .69 .096 6.2 .80 .080 6.3 .79 3.1 270 29 .80 65 8.6 8.3   370   110    8.1   370   110     .085 26   .88  160    4300 1900   3.2  280 32   .18 35 1.2 .45 24 6.6 .14  15 1.5  9.5 400 73 11   540 100 10   470 94
memsafety-ext3/getNumbers4_true-valid-memsafety.c valid-deref valid-free valid-memtrack .086 24 .71 .16  6.5 1.8  .17  6.2 1.4  3.4 250 32 4.0  68 57   8.2   370   92    8.3   370   94     .20  27   2.5   140    4400 1100   3.4  250 33   .29 35 2.3 .48 24 5.9 .15  16 1.9  45   1100 480 900   1100 7100 44   1100 400
memsafety-ext3/scopes4_true-valid-memsafety.c valid-deref valid-free valid-memtrack .10  24 .72 .11  6.0 .33 .074 6.0 .32 2.8 250 23 .80 66 9.1 8.2   370   93    8.2   370   130     .087 26   .82  200    4400 1800   2.7  240 25   .14 34 1.3 .51 24 6.5 .13  17 1.6  11   400 79 11   410 95 15   530 120
pthread-memsafety/fillarray1_false-valid-deref.i valid-deref valid-free valid-memtrack .19  28 1.8  .096 7.7 1.3  .12  11   1.3  4.4 290 41 .21 35 2.5 8.4   450   120    1.6   200   21     .15  27   1.8   .94 81 11   4.3  280 36   .26 50 1.6 1.2  35 15   .089 14 1.0  17   360 120 16   370 140 16   680 120
pthread-memsafety/fillarray_false-valid-deref.i valid-deref valid-free valid-memtrack .22  28 2.0  .098 8.0 1.2  .13  10   1.6  4.2 280 36 .21 35 2.6 8.3   450   96    1.6   200   20     .14  27   1.7   1.0  84 14   4.3  280 36   .15 38 1.4 1.0  37 15   .086 15 .93 17   370 140 15   370 120 15   500 120
pthread-memsafety/list1_false-valid-deref.i valid-deref valid-free valid-memtrack .34  29 4.1  .11  7.8 1.3  .17  10   1.4  4.2 280 39 900    5500 9600   8.5   450   100    8.9   450   92     .13  27   1.2   .47 83 5.6 4.3  280 36   .15 36 1.2 1.1  37 15   .11  19 1.2  17   390 140 16   360 140 60   820 580
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i valid-memcleanup .39  32 4.2  .096 7.2 1.3  330     15000   3600    3.2 260 29 .16 34 2.0 .027 4.6 .28 .030 4.6 .16  .020 5.5 .050 84    4300 730   .55 44 5.5 .16 35 1.2 3.4  89 48   .25  18 2.8  16   530 140 28   800 250 33   650 400
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i valid-memcleanup .19  28 1.7  .34  26   5.1  450     15000   5800    4.0 260 33 .24 35 3.1 .055 4.6 .24 .036 4.7 .19  .037 5.3 .083 900    83 11000   .50 42 5.3 .61 45 6.0 3.9  94 48   .25  18 2.8  900   1100 12000 900   1000 8000 900   1300 9700
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 3.8   43 46    .51  27   6.6  .12  9.4 1.4  3.6 260 35 900    12000 5700   .034 4.6 .18 .033 4.6 .10  .049 5.5 .078 900    210 11000   .48 42 4.5 2.8  63 27   8.2  120 110   .35  22 3.1  900   1200 11000 900   980 8600 900   1000 11000
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 360     3000 3200    .55  43   7.0  .12  7.7 1.0  3.9 270 36 .70 38 9.1 .053 4.7 .16 .034 4.5 .30  .028 5.5 .17  900    180 11000   .49 42 5.4 .16 38 1.6 3.8  95 45   .25  17 3.3  24   610 190 71   870 650 25   580 190
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 900     4500 10000    .26  19   2.9  .097 8.2 .88 3.9 260 32 .19 35 2.3 .033 4.6 .18 .036 4.8 .18  .021 5.4 .091 900    140 11000   .51 43 4.8 .79 58 4.2 3.8  97 56   .27  18 3.4  900   2200 13000 900   1000 7600 900   970 12000
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 110     1400 1300    .25  18   3.1  .10  7.9 .96 3.8 260 39 .47 36 6.0 .030 4.5 .16 .046 4.6 .17  .034 5.5 .067 900    170 11000   .51 42 5.2 .54 50 4.1 3.7  96 46   .26  17 2.8  900   2300 11000 900   980 8600 900   930 9800
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 13     360 160    .16  10   1.8  .11  8.8 1.0  3.8 270 35 .21 35 2.5 .031 4.6 .22 .029 4.6 .20  .023 5.5 .14  900    170 12000   .53 43 4.6 .16 37 1.6 3.9  130 54   .25  17 3.0  900   1500 10000 900   970 6700 900   880 11000
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 2.5   82 30    .12  7.6 1.2  .11  8.0 .99 3.5 260 32 .16 34 1.8 .029 4.5 .19 .030 4.6 .21  .024 5.4 .054 900    75 9400   .51 42 4.4 .14 38 1.3 3.6  94 48   .24  19 3.5  900   840 12000 900   1000 8500 900   2000 10000
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 9.1   200 100    .14  8.4 1.5  .11  8.0 1.1  3.8 280 36 .16 34 1.8 .055 4.6 .16 .029 4.6 .27  .020 5.5 .093 900    170 10000   .51 42 5.2 .16 34 1.4 3.7  94 44   .24  18 2.8  900   2100 8800 900   1000 7900 900   960 11000
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 11     270 98    .38  16   5.5  .12  9.6 1.6  4.2 270 39 1.3  37 16   .032 4.6 .18 .054 4.6 .17  .044 5.4 .10  900    170 12000   .49 43 5.3 .39 49 1.4 4.1  100 57   .26  18 2.4  900   960 9400 900   960 8000 900   960 10000
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 20     380 200    .19  13   2.3  .12  8.6 .98 3.5 250 32 .18 35 2.0 .031 4.5 .25 .057 4.6 .18  .026 5.5 .18  900    170 10000   .54 43 5.4 .19 36 1.3 3.7  95 51   .25  18 3.2  900   1100 11000 900   1000 6900 900   2200 11000
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 32     410 320    .18  12   2.0  .12  8.9 1.5  4.2 270 34 .51 36 5.8 .026 4.8 .26 .033 4.7 .19  .047 5.3 .14  900    180 11000   .51 42 5.1 .44 37 4.6 4.0  100 39   .24  18 2.9  900   2300 9800 900   990 7100 900   970 12000
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 1.2   57 15    .18  12   1.9  .11  7.9 1.1  3.4 250 32 .19 34 2.2 .034 4.6 .17 .029 4.6 .19  .021 5.4 .12  900    170 10000   .55 42 5.4 .16 37 1.5 3.6  95 46   .23  17 3.0  900   2600 12000 900   960 6900 900   1000 10000
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 41     720 390    .22  14   2.0  .10  8.4 .96 4.1 280 33 .65 36 9.9 .043 4.6 .13 .029 4.6 .17  .043 5.3 .13  900    160 10000   .50 43 4.7 .18 37 1.3 3.8  97 50   .27  17 4.1  900   2200 12000 900   870 8900 900   970 12000
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 1.5   53 18    .14  7.1 1.1  .092 8.0 1.1  3.4 260 29 .17 34 1.8 .027 4.6 .19 .048 4.5 .14  .028 5.3 .17  900    75 9300   .49 42 5.4 .17 33 1.3 3.6  98 42   .23  17 3.0  900   750 10000 900   1000 7700 900   2100 10000
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 5.1   110 54    .14  7.9 1.4  .099 8.0 1.1  3.5 260 30 .19 35 1.7 .030 4.6 .13 .029 4.6 .18  .021 5.4 .083 900    170 9400   .48 43 4.9 .35 49 1.3 3.7  93 43   .23  18 2.6  900   2200 11000 900   1000 7400 900   820 10000
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 5.5   150 63    .35  15   4.0  .15  8.8 1.2  4.1 270 33 1.3  37 17   .030 4.7 .21 .027 4.6 .21  .024 5.4 .090 900    180 11000   .54 42 5.0 .18 35 1.4 4.1  100 50   .26  18 3.2  900   2000 10000 900   1000 7200 900   820 11000
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 23     580 260    .20  12   1.7  .092 8.5 .88 4.1 260 39 .53 36 7.0 .049 4.6 .14 .032 4.6 .22  .027 5.3 .085 900    190 11000   .52 44 4.8 .37 49 1.9 3.8  96 58   .30  17 2.5  900   2200 9800 900   1100 7800 900   1000 10000
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 2.6   92 35    .16  11   1.7  .095 8.2 .82 3.6 250 33 .18 34 1.9 .036 4.8 .22 .030 4.6 .21  .020 5.4 .16  900    180 9900   .51 43 4.7 .15 34 1.5 3.7  97 50   .26  18 3.2  900   2400 9300 900   1000 7500 900   1400 11000
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 16     250 180    .16  11   1.5  .11  8.6 1.1  10   480 86 .49 35 5.9 .033 4.6 .24 .044 4.6 .20  .021 5.5 .093 900    190 12000   .49 42 4.6 .50 49 3.5 4.4  110 66   .26  18 3.5  900   790 11000 900   1000 9000 900   1000 11000
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i valid-memcleanup .58  32 7.7  .14  10   1.6  .087 7.8 1.1  3.4 260 33 .18 34 2.0 .045 4.7 .20 .055 4.6 .15  .020 5.3 .12  900    190 10000   .50 42 4.4 .38 49 1.2 3.6  120 43   .22  18 2.4  900   2400 11000 900   850 8300 900   720 12000
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i valid-memcleanup .82  34 9.8  .10  7.7 1.2  570     15000   7100    3.5 260 32 .48 35 4.8 .028 4.7 .41 .036 4.5 .20  .034 5.5 .11  900    180 9500   .51 44 5.0 .16 34 1.5 3.5  89 39   .26  18 3.3  25   740 220 750   1000 5900 47   640 480
list-properties/list_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 4.0   85 44    .15  10   1.6  .090 7.9 .50 3.8 260 34 .68 36 8.6 .032 4.7 .15 .031 4.7 .20  .027 5.4 .15  .45 83 5.6 .52 44 5.1 .21 35 1.1 3.6  120 40   .26  18 3.6  12   580 110 15   520 140 13   580 110
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i valid-memcleanup .64  31 8.0  .097 7.2 1.1  .069 7.5 .48 3.4 250 32 .51 35 5.7 .038 4.6 .30 .044 4.7 .20  .020 5.5 .11  .46 82 6.6 .51 42 5.3 .16 35 1.2 3.4  89 42   .26  18 3.2  10   390 79 13   580 120 9.8 390 71
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i valid-memcleanup .33  29 4.0  .20  8.4 2.1  .20  16   2.2  3.8 270 36 1.0  36 14   .031 4.6 .19 .034 4.6 .19  .020 5.4 .063 40    4500 460   .52 42 4.9 .18 37 1.5 3.5  84 45   .19  16 2.1  480   870 6200 380   1100 3200 910   14000 5300
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i valid-memcleanup .64  35 10    .24  10   3.1  430     2200   5900    3.9 260 38 1.4  37 18   .060 4.7 .19 .030 4.6 .18  .022 5.4 .050 900    75 9600   .50 42 4.9 .17 35 1.5 3.9  94 47   .20  16 2.2  900   850 10000 900   980 9400 900   2500 7600
list-properties/simple_false-unreach-call_false-valid-memcleanup.i valid-memcleanup .40  30 4.1  .090 7.1 .79 .14  7.2 1.2  3.4 250 32 .47 35 6.0 .035 4.6 .29 .049 4.7 .20  .022 5.5 .097 .44 83 5.5 .49 42 4.9 .33 49 1.4 3.4  85 50   .25  19 2.8  13   510 100 14   560 110 14   590 120
list-properties/splice_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 2.3   74 27    .12  9.1 1.2  .096 8.0 .88 3.7 260 32 .49 36 6.1 .026 4.6 .22 .025 4.6 .26  .024 5.4 .093 .46 83 6.5 .51 42 4.4 .28 50 1.8 3.5  98 40   .25  18 2.8  9.8 390 73 12   520 94 9.6 370 70
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 3.7   77 36    .26  12   3.2  880     7100   9900    6.8 300 56 2.2  39 28   .034 4.6 .27 .045 4.6 .18  .035 5.5 .087 900    2100 7000   .50 42 4.7 .17 35 1.3 4.3  94 54   .27  17 2.7  900   2300 11000 900   1100 11000 900   1400 11000
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 150     15000 1300    .21  10   2.1  870     7500   13000    4.4 290 35 1.2  36 14   .037 4.6 .12 .031 4.6 .086 .049 5.4 .13  19    83 290   .52 43 5.0 .22 37 2.2 3.5  86 43   .30  18 4.1  900   2200 12000 900   930 6100 910   12000 11000
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 260     15000 2600    .77  50   8.2  580     15000   7200    4.5 290 38 1.3  39 20   .028 4.6 .23 .054 4.6 .12  .038 5.3 .086 900    570 10000   .53 42 5.3 .46 51 3.5 3.6  91 44   .31  18 3.5  900   1300 11000 900   940 7400 900   1700 12000
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i valid-memcleanup 900     4600 11000    16     640   200    .087 8.9 .64 7.2 370 59 68    1200 730   .026 4.6 .25 .035 4.7 .17  .047 5.4 .090 900    120 13000   .51 41 4.8 .52 36 5.0 7.4  130 88   .32  18 3.5  900   970 11000 900   980 9000 900   1000 11000
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
total 434 13000 180000 140000 434 92000    760000 920000   434 50000    870000 670000   434 100000 1100000 800000 434 90000   230000 1100000 434 47000   200000 450000 434 57000   180000 540000 434 98000    250000 1200000   434 150000    710000 1700000   434 100000   1100000 810000 434 36000 330000 300000 434 130000 89000 1400000 434 92000   210000 1000000 434 170000 450000 2100000 434 210000 360000 2000000 434 180000 540000 2200000
    correct results 95 470 9700 4300 190 1600    9700 16000   126 7700    70000 100000   256 2000 110000 17000 125 2800   8300 35000 142 1500   64000 19000 150 1600   67000 19000 194 1800    10000 24000   237 16000    430000 170000   225 1800   100000 16000 296 2200 21000 23000 121 13000 17000 140000 299 110   5800 1300 172 8300 100000 95000 145 13000 91000 120000 161 8300 94000 96000
        correct true 49 290 6000 2500 119 1600    8200 16000   71 7600    69000 100000   118 1400 70000 11000 80 2400   6500 31000 79 1000   36000 12000 79 1000   36000 12000 130 1600    6600 20000   120 14000    370000 160000   118 1300   69000 12000 154 2000 13000 21000 80 12000 12000 120000 135 44   2800 530 108 4500 59000 50000 84 7800 56000 71000 102 4700 56000 54000
        correct false 46 180 3700 1800 71 28    1400 370   55 87    1200 680   138 620 40000 5400 45 310   1800 4200 63 520   28000 6700 71 600   31000 7600 64 250    3700 3300   117 1400    62000 13000   107 490   31000 4400 142 230 7500 1800 41 980 4500 12000 164 64   3100 790 64 3800 44000 46000 61 5100 35000 48000 59 3600 38000 42000
    correct-unconfimed results 10 30 780 310 103 900    20000 10000   24 450    2600 6100   0 75 530   4900 7000 4 34   1800 400 6 54   2700 660 76 250    4600 3000   10 750    9400 8700   0 30 13 1500 110 14 5500 2800 54000 8 5.8 320 79 3 610 3000 7600 2 18 730 140 4 48 1900 360
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 10 30 780 310 103 900    20000 10000   24 450    2600 6100   0 75 530   4900 7000 4 34   1800 400 6 54   2700 660 76 250    4600 3000   10 750    9400 8700   0 30 13 1500 110 14 5500 2800 54000 8 5.8 320 79 3 610 3000 7600 2 18 730 140 4 48 1900 360
    incorrect results 3 31 590 340 8 1.4  87 13   5 .78 45 7.8 0 17 140   1500 1800 9 74   3800 890 23 610   10000 6900 10 1.4  260 15   5 1400    17000 15000   2 15   750 140 0 0 0 7 700 4400 8800 6 1300 5000 10000 6 270 3500 3000
        incorrect true 0 2 .41 15 2.3 3 .53 25 4.9 0 1 1.4 37 18 1 7.9 370 110 1 8.1 370 93 8 .92 210 9.7 4 1400    17000 15000   1 11   460 110 0 0 0 6 570 3600 7000 6 1300 5000 10000 5 130 2800 1300
        incorrect false 3 31 590 340 6 .94 72 10   2 .25 21 2.9 0 16 140   1400 1800 8 66   3500 780 22 600   9700 6800 2 .46 53 4.9 1 .47 83 5.6 1 4.2 290 33 0 0 0 1 130 790 1800 0 1 130 750 1700
Run set 2ls.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] cbmc.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] cbmc-path.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] cpa-seq.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] depthk.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] divine-explicit.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] divine-smt.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] esbmc-kind.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] map2check.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] pesco.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] predatorhp.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] smack.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] symbiotic.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] uautomizer.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] ukojak.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup] utaipan.[sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup]