Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29794 CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ 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 VeriAbs 1.3.10
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-04 22:41: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:44:04 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 2018-12-10 16:50:17 CET
Run set 2ls.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cbmc.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cbmc-path.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cpa-bam-bnb.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] depthk.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] divine-explicit.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] divine-smt.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] esbmc-kind.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] pesco.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] smack.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] symbiotic.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] uautomizer.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] ukojak.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] utaipan.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] veriabs.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety]
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19-bam-bnb -disable-java-assertions -heap 10000m -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -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)
busybox-1.22.0/basename_false-valid-deref.i valid-deref valid-free valid-memtrack .25  32 2.9  12    770   130   28    340 340   .49 42 5.5 5.2 280 47 350    650 5300   1.3   170   19    1.3   170   16    540     1000 7900    4.9 270 44 750   270   9900 .65 23 8.6 820   2600 9300 900   950 9200 900   2900 9900 .024 7.5 .12 
busybox-1.22.0/head_false-valid-deref.i valid-deref valid-free valid-memtrack .40  39 3.8  3.5  53   50   .76 29 10   .53 42 5.1 6.5 300 52 22    15000 250   1.2   160   17    1.2   160   15    22     15000 260    6.2 290 58 900   9.5 12000 1.8  96 19   8.8 340 61 8.0 320 58 9.5 360 72 .020 7.7 .11 
busybox-1.22.0/sleep_false-valid-deref.i valid-deref valid-free valid-memtrack 1.2   39 11    .88 27   11   .63 27 8.5 .53 44 5.8 6.1 310 51 900    800 10000   1.2   160   16    1.2   160   16    .22  32 3.2  6.0 290 47 750   480   7400 .38 21 3.7 8.6 360 69 8.8 340 74 8.6 360 73 .016 7.4 .11 
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i valid-deref valid-free valid-memtrack .35  37 3.3  .29 13   3.5 .39 20 5.7 .51 43 4.9 5.9 290 48 580    980 7000   1.2   160   14    1.2   160   15    .20  30 2.5  6.2 290 51 840   500   8400 1.2  22 14   9.1 360 75 8.0 340 65 8.6 350 65 .021 7.5 .12 
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .27  32 2.4  880    6400   9800   21    290 320   .50 44 4.5 5.1 290 50 900    810 12000   1.3   170   14    1.3   170   17    900     1100 11000    4.9 270 44 750   200   8600 900    470 9300   170   2900 2000 900   1000 11000 200   2800 2500 .026 7.3 .14 
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .66  38 7.7  .39 16   4.9 .43 23 6.5 .52 43 5.1 5.8 290 45 900    2200 7100   1.2   160   16    1.2   160   15    900     4400 7900    6.0 300 45 750   370   6800 900    68 14000   8.9 340 72 9.1 370 78 7.6 350 61 .031 7.8 .11 
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 15     89 190    7.1  84   87   1.3  47 16   .50 42 4.6 7.1 310 55 22    15000 280   1.2   170   20    1.2   170   19    22     15000 230    6.3 290 52 900   9.6 12000 14    180 120   8.4 350 64 8.5 340 65 8.5 330 65 .022 7.1 .20 
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .47  47 4.5  3.0  130   40   2.8  79 39   .50 44 5.2 6.9 310 57 22    15000 280   1.2   170   16    1.3   170   19    22     15000 270    7.2 300 54 900   9.8 13000 16    330 170   9.4 350 68 8.4 340 69 9.0 330 77 .021 7.4 .13 
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .24  31 2.6  590    13000   6700   1.1  32 15   .52 44 5.0 5.1 290 42 900    920 11000   1.3   170   17    1.3   170   16    900     4400 11000    5.1 290 41 880   400   9500 .65 27 8.1 900   3200 11000 900   940 8700 900   2300 12000 .046 7.4 .11 
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 7.9   72 96    62    220   710   .70 40 8.4 .55 43 4.7 6.7 300 56 22    15000 240   1.3   160   15    1.3   160   17    22     15000 320    6.8 310 59 750   3300   8900 41    210 440   9.4 370 82 8.9 360 77 8.6 320 63 .023 7.8 .18 
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .55  38 6.6  880    7200   7200   .50 22 7.1 .50 42 4.5 6.0 290 53 900    1700 10000   1.2   160   15    1.2   160   18    .23  32 2.8  6.0 300 43 750   170   11000 900    680 7900   7.7 330 71 9.0 340 71 8.5 360 72 .025 7.7 .088
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 35     130 470    34    210   460   .51 29 6.9 .53 43 4.9 7.0 300 63 24    15000 290   1.2   170   16    1.2   170   17    22     15000 280    6.9 310 58 900   9.5 13000 25    270 220   8.6 360 70 8.9 370 72 9.2 360 70 .025 7.8 .15 
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 6.2   57 88    3.7  50   49   .45 26 5.6 .52 43 5.2 6.5 300 57 22    15000 270   1.3   160   15    1.2   160   14    22     15000 280    6.5 300 58 900   9.7 11000 8.9  170 77   9.1 360 80 8.9 350 75 8.7 340 68 .021 7.6 .13 
busybox-1.22.0/head_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .38  40 4.4  3.5  54   44   .74 27 9.3 .52 42 5.1 6.6 300 60 22    15000 310   1.2   160   17    1.7   160   30    22     15000 260    6.4 300 56 900   9.6 12000 1.8  97 19   8.3 340 72 8.5 330 67 8.4 340 64 .050 6.9 .12 
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .26  34 2.2  570    13000   6600   .26 16 3.1 .52 42 6.2 5.1 280 45 900    670 10000   1.3   170   17    1.3   170   21    900     1600 9200    5.1 280 47 880   400   8100 900    2000 13000   900   2200 11000 900   840 11000 900   1800 10000 .026 6.9 .10 
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .34  37 4.0  .25 14   3.7 .30 19 2.9 .48 43 5.1 5.8 300 55 830    1500 7200   1.2   160   15    1.2   160   18    .19  30 2.7  5.5 280 46 890   440   9200 .67 24 8.2 8.6 370 69 8.6 330 69 8.8 370 76 .022 7.3 .11 
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 300     340 3000    3.6  55   45   1.1  58 13   .53 42 4.9 8.2 330 70 23    15000 300   1.3   170   20    1.3   170   16    22     15000 260    8.6 370 74 750   3500   9400 210    1000 1900   18   350 140 19   360 160 18   360 150 .026 7.7 .091
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 3.1   45 31    880    1100   3300   2.4  64 31   .51 43 5.3 6.5 300 52 22    15000 260   1.2   160   16    1.3   160   17    22     15000 300    7.0 310 60 900   9.9 14000 14    180 120   8.8 360 69 9.2 340 75 8.7 350 66 .021 7.7 .15 
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .31  36 3.3  .28 14   3.9 .22 17 2.6 .51 42 4.8 5.4 290 40 900    1700 8500   1.3   170   17    1.3   170   18    .19  30 2.7  5.8 280 49 750   450   7500 900    64 11000   8.8 350 68 8.7 330 73 8.6 350 69 .023 7.6 .10 
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 900     670 11000    880    670   4700   3.1  90 42   .51 43 4.6 9.1 390 79 22    15000 250   1.3   170   15    1.3   170   16    22     15000 280    8.4 380 75 900   10   13000 90    860 670   9.4 350 80 9.8 360 79 11   370 81 .045 6.7 .080
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .57  43 4.8  23    110   290   .46 25 4.9 .51 43 5.1 6.5 300 60 900    2000 7600   1.3   160   17    1.2   160   15    .24  36 3.0  6.4 280 56 750   320   9800 2.5  110 29   8.8 370 79 8.1 320 66 9.0 370 71 .028 7.3 .13 
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 3.2   41 35    .82 27   13   1.9  53 25   .53 42 4.9 6.7 300 52 22    15000 260   1.2   160   15    1.2   160   15    22     15000 290    6.5 300 54 890   760   6400 5.6  95 66   8.6 350 79 9.0 360 71 8.6 360 65 .030 7.1 .10 
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .35  37 3.9  .30 14   5.4 .38 20 4.7 .53 42 4.8 5.5 280 43 900    1600 8700   1.2   160   20    1.2   160   20    .22  31 2.2  6.1 290 58 750   430   7100 900    76 11000   8.7 350 63 8.4 350 75 9.0 360 78 .024 7.6 .11 
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 7.2   68 93    880    270   12000   1.2  45 17   .52 42 4.8 6.8 300 57 22    15000 260   1.2   160   19    1.2   160   17    22     15000 260    6.9 300 57 140   580   1300 44    210 450   9.2 360 79 8.9 360 81 8.4 320 71 .026 7.6 .13 
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.8   40 22    .71 21   10   1.1  41 12   .50 42 4.8 6.4 310 56 22    15000 270   1.2   160   15    1.2   160   20    22     15000 260    6.3 310 60 900   9.2 13000 4.5  83 53   8.5 360 78 8.7 360 82 8.3 330 64 .021 7.7 .094
busybox-1.22.0/sleep_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.2   39 11    .90 27   12   .67 26 9.8 .51 42 4.8 6.2 300 50 900    870 12000   1.2   160   16    1.3   160   13    .23  32 2.6  5.9 280 55 750   480   8500 .35 21 3.5 8.9 360 77 8.8 370 72 8.3 360 79 .023 7.6 .11 
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 78     210 790    66    180   800   1.3  63 18   .51 43 4.8 10   510 100 23    15000 270   1.3   160   19    1.3   160   18    22     15000 310    10   510 84 760   660   5500 900    520 12000   9.5 350 77 10   380 85 9.8 370 83 .025 7.8 .092
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .30  35 3.2  .21 11   2.6 .37 21 4.6 .52 42 5.0 5.4 290 45 900    610 13000   1.3   170   18    1.3   170   18    .19  30 2.7  5.3 290 49 890   460   7800 900    160 8300   8.1 350 65 7.8 340 68 8.1 340 72 .025 7.6 .12 
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 6.2   57 68    2.6  44   35   1.0  40 15   .49 42 5.2 6.3 300 51 22    15000 290   1.2   160   15    1.2   160   16    22     15000 300    6.7 300 55 750   710   7100 7.1  110 86   9.1 370 73 8.6 360 71 8.0 340 65 .023 7.6 .13 
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 4.0   49 47    1.2  32   15   1.1  46 14   .52 42 5.6 6.5 290 56 22    15000 280   1.2   160   18    1.2   160   15    22     15000 320    6.4 300 61 750   3300   9200 6.2  110 66   8.0 320 66 8.7 360 71 8.0 330 71 .025 7.2 .15 
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 37     130 380    880    690   5900   .99 35 15   .52 43 4.5 6.8 300 66 900    15000 5900   1.2   160   15    1.2   160   16    .24  37 2.8  6.6 290 61 750   490   7500 2.7  87 21   9.3 360 80 9.1 350 83 8.7 340 71 .026 7.3 .11 
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 6.5   67 69    2.8  110   36   2.5  69 31   .53 44 5.8 7.2 310 56 22    15000 250   1.3   160   17    1.2   160   17    22     15000 290    6.8 290 63 900   9.8 11000 11    270 100   9.0 320 75 8.6 330 69 9.1 370 71 .022 7.3 .11 
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.9   41 21    1.1  120   16   2.3  62 29   .53 44 5.1 6.7 310 56 22    15000 250   1.2   160   16    1.3   160   16    22     15000 300    6.9 300 58 890   760   8800 5.7  110 54   8.6 370 67 8.5 360 70 8.6 360 69 .022 7.6 .091
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 5.8   58 67    2.0  39   25   1.2  43 15   .50 42 5.3 6.6 310 59 22    15000 270   1.2   170   15    1.2   170   20    22     15000 290    6.8 300 52 900   9.7 11000 9.7  140 110   9.0 360 76 8.1 340 67 8.3 330 70 .030 7.5 .095
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .48  37 6.1  .25 13   3.5 .73 26 9.2 .53 43 5.3 5.8 300 48 85    350 990   1.2   160   17    1.2   160   15    .23  31 2.3  5.7 290 47 750   410   9700 900    180 8000   8.6 360 78 7.9 320 62 7.9 340 65 .024 7.5 .11 
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 12     81 170    6.1  85   69   2.0  58 29   .49 42 5.2 7.0 310 63 22    15000 270   1.2   160   16    1.3   160   16    22     15000 290    7.0 310 55 900   9.8 13000 22    250 180   8.8 350 72 8.5 350 81 9.0 330 83 .021 7.6 .089
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .37  42 4.5  880    580   6000   .45 25 6.2 .50 43 5.2 6.5 300 50 22    15000 250   1.2   160   14    1.2   160   17    22     15000 240    6.2 300 57 890   840   9800 7.9  130 68   8.6 340 72 8.4 330 75 8.9 370 66 .039 7.2 .13 
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 2.1   42 21    .78 27   12   1.7  50 21   .50 42 4.8 6.5 300 51 22    15000 270   1.3   170   16    1.2   170   16    23     15000 350    6.3 300 55 750   720   9500 5.9  100 58   8.6 350 64 8.4 320 70 9.1 360 75 .022 7.2 .12 
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .35  37 3.2  .22 12   3.3 .33 19 3.2 .54 43 5.1 5.5 280 53 900    700 9600   1.2   160   16    1.2   160   15    .20  31 2.3  5.9 290 46 890   470   10000 900    150 8700   8.4 360 64 8.7 360 73 8.5 330 66 .023 7.8 .084
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .34  37 3.5  .24 12   3.1 .30 19 3.9 .51 43 4.4 5.8 300 50 360    1200 3800   1.2   160   17    1.2   160   19    .21  30 2.5  6.0 290 53 760   520   8900 900    110 11000   8.1 320 63 7.5 330 65 7.9 350 65 .025 7.6 .099
busybox-1.22.0/chgrp-incomplete_false-no-overflow.i no-overflow .30  37 3.2  .23 12   2.9 .20 18 2.2 .52 44 5.2 900   1700 7600 900    800 11000   .033 4.6 .22 .029 4.7 .19 3.0   140 45    900   1700 6200 880   670   8000 900    140 8200   8.4 350 70 7.6 320 58 8.3 360 67 .023 7.5 .16 
busybox-1.22.0/chroot-incomplete_false-no-overflow.i no-overflow .46  38 4.8  .28 14   3.6 .97 68 12   .50 42 5.0 900   1300 5900 900    1700 9200   .037 4.8 .15 .031 4.6 .20 3.0   150 46    900   1300 6800 880   690   7100 900    59 11000   8.5 350 62 9.2 350 74 8.6 330 69 .023 7.4 .14 
busybox-1.22.0/cut_false-no-overflow.i no-overflow 10     50 91    5.8  76   69   .79 75 9.4 .49 43 5.1 900   6700 11000 22    15000 270   .046 4.6 .19 .055 4.6 .20 22     15000 270    910   6800 13000 880   730   6600 1.7  81 17   8.6 350 66 9.1 330 65 9.2 350 77 .022 7.5 .097
busybox-1.22.0/date_false-no-overflow.i no-overflow .43  48 3.7  2.4  120   28   .71 55 8.4 .53 42 7.8 900   3400 11000 22    15000 340   .031 4.6 .19 .030 4.6 .18 22     15000 250    900   3600 12000 880   4000   11000 2.9  170 25   9.2 370 71 9.3 360 75 9.3 350 74 .024 7.6 .087
busybox-1.22.0/du_false-no-overflow.i no-overflow 5.8   46 54    52    200   480   .48 39 5.7 .53 44 5.4 900   3300 11000 23    15000 310   .028 4.7 .18 .029 4.6 .21 22     15000 290    900   3500 11000 880   3700   11000 3.1  120 20   8.8 320 67 9.4 360 76 8.8 350 72 .022 7.9 .090
busybox-1.22.0/echo_false-no-overflow.i no-overflow .41  38 5.3  880    3100   5700   .66 86 7.9 .52 42 4.7 910   850 13000 900    1600 9700   .028 4.7 .19 .031 4.6 .21 4.2   240 66    910   870 7900 880   570   6900 900    460 6600   8.1 340 64 8.4 330 67 8.5 360 73 .021 7.5 .11 
busybox-1.22.0/expand_false-no-overflow.i no-overflow 24     71 190    29    200   420   .38 33 4.4 .52 42 4.6 910   6400 12000 22    15000 290   .055 4.7 .16 .028 4.5 .25 22     15000 270    910   6600 12000 880   840   6700 2.9  100 21   8.8 360 73 9.0 360 75 8.9 330 67 .031 7.7 .13 
busybox-1.22.0/fold_false-no-overflow.i no-overflow 4.7   42 32    2.9  45   37   .35 29 3.8 .51 44 4.9 900   810 10000 22    15000 270   .037 4.6 .26 .032 4.6 .17 22     15000 280    900   830 11000 880   690   8900 1.1  60 13   9.1 350 75 8.9 350 68 9.1 370 71 .021 7.1 .11 
busybox-1.22.0/head_false-no-overflow.i no-overflow .37  40 4.1  2.9  48   37   .59 51 7.0 .51 42 5.2 900   1200 5800 22    15000 270   .036 4.6 .21 .052 4.6 .17 22     15000 290    900   1200 5700 880   490   8700 .63 54 7.1 9.2 350 67 8.7 330 73 8.1 320 61 .024 7.7 .083
busybox-1.22.0/logname_false-no-overflow.i no-overflow .28  37 2.8  .20 13   2.5 .21 18 2.3 .51 42 5.4 900   1400 6000 190    640 2500   .028 4.6 .22 .028 4.6 .19 3.0   150 39    900   1400 7500 880   660   7200 900    51 13000   9.0 350 63 8.5 350 77 8.6 350 74 .021 7.6 .16 
busybox-1.22.0/ls-incomplete_false-no-overflow.i no-overflow 190     180 1500    2.6  45   38   1.1  120 13   .49 43 5.2 910   3100 13000 22    15000 260   .042 4.7 .22 .026 4.6 .20 22     15000 310    900   3200 12000 880   3900   10000 19    310 100   9.9 340 88 10   350 79 10   370 92 .018 7.5 .15 
busybox-1.22.0/mkdir_false-no-overflow.i no-overflow 2.2   44 19    880    1600   4800   .54 33 7.5 .53 43 5.3 910   6700 12000 22    15000 270   .032 4.6 .20 .026 4.6 .25 22     15000 250    900   6900 11000 880   670   6400 1.2  81 16   8.9 350 82 9.0 340 74 9.4 360 78 .024 7.7 .11 
busybox-1.22.0/mkfifo-incomplete_false-no-overflow.i no-overflow .31  36 2.0  .23 12   2.4 .20 16 2.0 .50 43 5.0 68   720 660 900    2000 11000   .046 4.6 .18 .027 4.6 .27 3.0   140 39    68   730 660 880   680   7500 900    52 11000   7.9 350 64 8.6 360 74 8.5 360 63 .025 7.6 .098
busybox-1.22.0/od_false-no-overflow.i no-overflow 540     340 5500    880    740   4800   .79 61 8.2 .47 41 4.8 900   6600 13000 22    15000 280   .028 4.6 .25 .031 4.6 .16 22     15000 250    910   6900 11000 880   1100   6100 13    350 68   8.9 330 77 10   360 89 10   350 76 .027 7.6 .099
busybox-1.22.0/printf_false-no-overflow.i no-overflow .48  43 5.1  18    98   230   .25 24 2.8 .54 43 5.4 900   1200 6700 900    4000 7100   .027 4.6 .27 .054 4.6 .14 3.0   150 35    900   1200 5800 880   490   8500 .27 17 3.4 8.2 330 65 9.2 360 71 8.8 360 76 .023 7.5 .12 
busybox-1.22.0/readlink_false-no-overflow.i no-overflow 2.1   41 26    .64 24   7.5 .84 69 11   .49 42 5.0 910   7000 12000 23    15000 270   .030 4.6 .20 .030 4.6 .20 22     15000 280    910   6900 12000 880   690   6800 .95 54 9.1 8.1 320 73 8.5 330 76 8.6 360 70 .022 7.6 .092
busybox-1.22.0/realpath_false-no-overflow.i no-overflow .30  37 2.4  .23 13   2.9 .95 61 11   .50 42 5.2 900   1300 6800 900    2100 7800   .035 4.6 .14 .033 4.8 .27 3.0   140 38    900   1400 8500 880   680   8100 900    72 13000   8.0 350 69 8.5 360 69 8.5 330 70 .021 7.3 .12 
busybox-1.22.0/rm_false-no-overflow.i no-overflow 5.2   45 41    880    310   10000   .71 70 9.1 .51 42 6.0 910   6600 12000 22    15000 260   .030 4.5 .17 .026 4.7 .24 22     15000 260    900   6600 13000 880   690   7700 1.9  110 16   8.9 360 70 8.5 330 68 9.1 360 78 .022 7.8 .17 
busybox-1.22.0/seq_false-no-overflow.i no-overflow 1.1   41 12    .52 16   7.3 .47 30 5.8 .51 43 5.2 900   7100 11000 22    15000 280   .029 4.6 .27 .055 4.6 .18 22     15000 280    900   6900 12000 880   680   9900 .27 18 2.8 8.5 340 67 8.6 360 72 9.1 360 80 .021 7.6 .099
busybox-1.22.0/sleep_false-no-overflow.i no-overflow .73  38 8.2  .69 24   9.6 .71 85 9.8 .51 43 5.1 7.9 340 72 890    670 9900   .029 4.6 .21 .027 4.6 .17 3.5   170 52    8.1 340 77 880   490   8000 .25 17 3.1 8.0 340 69 8.9 360 74 8.7 360 67 .035 7.7 .12 
busybox-1.22.0/stty_false-no-overflow.i no-overflow 47     110 500    57    160   640   3.4  180 46   .54 44 5.0 900   2200 11000 23    15000 260   .031 4.6 .16 .046 4.6 .15 22     15000 260    900   2200 11000 880   1400   5800 900    170 11000   9.4 360 79 9.3 340 78 10   380 83 .024 7.8 .070
busybox-1.22.0/sync_false-no-overflow.i no-overflow .27  35 2.5  .16 10   1.7 .27 16 2.8 .48 42 4.6 57   490 590 900    840 13000   .031 4.6 .23 .030 4.6 .28 3.0   140 41    55   610 580 880   690   7000 900    130 7600   9.5 360 64 8.5 360 70 8.7 350 72 .019 7.5 .14 
busybox-1.22.0/tac_false-no-overflow.i no-overflow 4.9   41 33    2.1  39   24   .69 55 10   .49 43 4.8 910   6800 13000 22    15000 260   .031 4.6 .21 .026 4.6 .26 22     15000 330    900   6900 10000 880   800   9300 .80 46 9.5 8.4 330 68 8.9 340 73 9.3 350 76 .016 7.2 .089
busybox-1.22.0/tee_false-no-overflow.i no-overflow .33  41 3.1  .87 27   12   1.3  110 17   .50 41 4.5 900   3500 9400 22    15000 300   .029 4.6 .21 .034 4.6 .20 22     15000 290    900   3700 12000 880   3700   11000 .78 48 9.4 7.7 330 67 8.7 360 69 8.6 340 70 .023 7.8 .072
busybox-1.22.0/test-incomplete_false-no-overflow.i no-overflow 23     68 220    880    670   6100   2.8  170 37   .51 43 5.6 33   590 360 900    15000 7800   .038 4.6 .15 .030 4.6 .21 3.3   170 41    32   570 430 880   580   8700 .83 60 8.6 9.3 360 78 9.0 360 65 8.4 350 71 .025 7.6 .11 
busybox-1.22.0/touch_false-no-overflow.i no-overflow 4.5   46 40    2.2  110   28   .60 35 7.3 .53 44 5.5 910   6600 11000 22    15000 320   .029 4.6 .19 .026 4.6 .37 22     15000 240    910   6700 13000 880   700   7400 1.6  120 19   9.2 370 79 8.3 340 67 9.2 350 82 .022 7.6 .17 
busybox-1.22.0/uname_false-no-overflow.i no-overflow 1.1   42 14    .81 120   9.8 .52 32 7.7 .51 42 4.7 910   6500 12000 22    15000 300   .025 4.6 .23 .048 4.6 .30 22     15000 270    910   6800 13000 880   630   8400 .77 49 9.1 8.5 350 68 8.6 350 76 8.7 360 73 .024 7.6 .092
busybox-1.22.0/uniq_false-no-overflow.i no-overflow 4.4   42 37    1.6  34   25   .71 77 9.3 .53 43 5.0 900   6900 11000 22    15000 250   .030 4.7 .17 .033 4.7 .26 22     15000 260    910   6900 14000 880   710   7200 1.3  73 14   8.7 340 64 8.6 360 77 8.7 340 70 .022 7.8 .13 
busybox-1.22.0/usleep_false-no-overflow.i no-overflow .41  37 4.1  .18 12   2.2 .58 39 7.9 .51 41 4.9 900   1400 6000 900    760 11000   .029 4.6 .18 .027 4.6 .26 3.4   180 50    900   1400 5200 880   480   6400 900    140 8500   8.5 360 69 8.4 330 64 8.5 340 65 .023 8.0 .092
busybox-1.22.0/uudecode_false-no-overflow.i no-overflow 9.1   46 55    5.0  77   80   2.0  210 25   .51 42 5.3 3.2 220 26 22    15000 270   .034 4.6 .21 .033 4.6 .26 22     15000 250    3.3 230 29 880   810   6400 1.9  100 20   9.4 360 72 9.2 370 79 8.8 370 67 .046 7.4 .075
busybox-1.22.0/wc_false-no-overflow.i no-overflow .34  42 3.4  880    620   7800   .28 23 4.3 .54 44 5.0 910   6300 11000 22    15000 260   .030 4.6 .25 .027 4.6 .20 22     15000 290    910   6200 12000 880   1100   9400 .89 58 9.9 9.1 350 63 8.6 320 65 8.3 350 78 .021 7.2 .12 
busybox-1.22.0/who_false-no-overflow.i no-overflow 1.3   42 12    .57 22   7.1 .76 67 9.5 .52 43 5.5 910   6900 11000 22    15000 300   .059 4.5 .26 .029 4.6 .19 22     15000 280    910   7000 13000 880   670   7900 1.0  58 12   8.2 350 72 8.6 320 66 9.2 340 76 .020 7.8 .11 
busybox-1.22.0/whoami-incomplete_false-no-overflow.i no-overflow .30  37 3.2  .18 11   2.3 .28 27 3.1 .54 43 5.1 900   950 6100 900    1000 11000   .040 4.6 .15 .025 4.6 .21 3.0   140 39    900   1100 6700 880   480   9800 900    130 7500   7.2 330 65 8.6 340 73 8.4 360 72 .021 7.9 .10 
busybox-1.22.0/yes_false-no-overflow.i no-overflow .29  37 3.2  .18 12   2.3 .57 80 7.2 .53 42 4.3 900   1200 6700 190    860 2000   .031 4.6 .26 .032 4.8 .14 3.4   160 49    900   1200 6500 880   560   8200 900    90 11000   8.0 330 63 8.9 360 70 8.3 360 65 .022 7.3 .12 
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .22  32 2.2  880    6000   7300   7.5  500 110   .48 41 4.5 900   1000 5500 900    660 10000   .045 4.6 .18 .054 4.6 .14 900     990 9300    900   1100 4600 880   620   9800 900    380 8100   180   2600 2000 900   890 11000 180   920 1900 .044 7.6 .097
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i no-overflow .31  37 2.7  .21 12   3.2 .19 18 2.6 .51 43 5.0 100   750 920 900    800 10000   .035 4.7 .24 .030 4.6 .21 3.0   140 37    110   740 1000 880   680   7500 900    130 8300   8.2 350 75 8.2 340 65 8.2 340 62 .024 7.4 .17 
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow .46  38 4.7  .28 14   3.3 .96 68 14   .52 43 5.3 900   1400 6200 900    1600 10000   .026 4.6 .19 .032 4.6 .34 3.0   150 39    900   1200 6300 880   690   6900 900    58 14000   8.3 360 62 8.3 320 67 8.4 330 70 .020 7.2 .088
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 11     50 89    5.8  76   68   .79 76 8.6 .50 43 6.0 910   6500 12000 22    15000 280   .031 4.6 .22 .033 4.6 .18 22     15000 290    910   6700 13000 880   760   7000 1.7  80 16   8.1 350 75 9.1 350 69 9.1 360 72 .023 7.7 .16 
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .41  47 4.2  2.3  120   34   .72 55 7.9 .51 42 5.1 900   3500 10000 22    15000 250   .033 4.6 .25 .033 4.6 .17 22     15000 230    900   3500 10000 880   3900   12000 2.9  150 24   9.4 360 68 9.5 350 72 8.7 370 76 .022 7.8 .088
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i no-overflow .23  31 1.9  620    13000   8100   .17 13 2.0 .50 42 5.4 900   5300 9900 900    1800 10000   .045 4.6 .18 .032 4.7 .12 900     11000 10000    910   5000 10000 880   700   7100 900    980 12000   140   2700 1400 900   1000 7500 160   1100 1600 .023 7.5 .12 
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i no-overflow 5.8   45 53    54    200   490   .46 38 5.9 .51 42 4.7 900   3300 11000 22    15000 250   .054 4.6 .12 .028 4.6 .34 22     15000 270    900   3400 10000 880   3800   12000 3.1  120 21   9.8 360 81 9.4 360 79 8.4 330 68 .023 7.5 .11 
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i no-overflow .41  38 4.8  880    3100   7300   .65 86 8.6 .50 42 4.8 910   860 8200 900    1600 11000   .029 4.6 .17 .031 4.6 .18 4.2   240 46    910   860 8500 880   560   7300 900    430 6800   8.4 340 64 8.7 340 69 8.4 360 77 .023 7.7 .10 
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 24     71 220    29    190   400   .36 33 5.5 .51 43 4.9 910   6600 12000 22    15000 270   .031 4.8 .20 .024 4.6 .20 22     15000 280    900   6500 13000 880   840   7600 3.1  100 23   9.2 350 82 9.2 330 71 8.2 350 62 .021 7.9 .15 
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i no-overflow 4.8   42 33    2.9  44   36   .36 30 4.2 .52 43 4.9 900   830 10000 22    15000 260   .055 4.5 .15 .028 4.6 .19 22     15000 320    900   670 10000 880   730   6500 1.0  60 11   8.3 330 65 8.6 340 68 9.2 360 73 .022 7.6 .13 
busybox-1.22.0/head_true-no-overflow_true-valid-memsafety.i no-overflow .37  40 3.3  2.9  48   33   .59 50 7.8 .49 42 5.3 600   1000 4000 23    15000 270   .032 4.6 .31 .029 4.7 .19 22     15000 280    620   1100 4000 880   490   7800 .61 54 7.0 8.5 360 70 8.8 370 65 8.3 360 74 .023 7.1 .096
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i no-overflow .22  34 2.0  550    13000   6500   .16 15 1.6 .51 43 4.8 540   15000 6600 900    1800 10000   .028 4.6 .20 .031 4.6 .13 900     14000 11000    550   15000 7600 880   910   7400 900    500 10000   18   550 150 33   750 290 19   520 160 .020 7.9 .14 
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i no-overflow .31  37 2.4  .19 13   2.2 .20 18 2.5 .50 42 4.7 230   830 1900 220    860 2200   .030 4.6 .19 .052 4.6 .14 3.0   150 35    230   840 2300 880   720   7600 900    52 13000   7.8 350 66 8.9 350 69 8.8 340 70 .022 7.3 .14 
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 180     180 2300    2.6  45   40   1.1  120 13   .51 43 4.7 900   3100 11000 22    15000 310   .031 4.8 .20 .027 4.6 .28 22     15000 240    910   3100 12000 880   3900   11000 20    300 94   9.4 330 83 10   340 80 10   360 91 .022 7.4 .099
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i no-overflow 2.0   43 19    880    1600   4800   .53 33 6.3 .50 42 4.5 910   6700 12000 23    15000 260   .032 4.5 .18 .037 4.6 .23 22     15000 300    900   6600 11000 880   660   7300 1.1  81 16   8.5 340 68 8.8 360 82 8.8 360 65 .023 7.6 .15 
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow .26  36 2.6  .21 12   2.4 .17 17 2.2 .52 42 5.0 170   800 1600 900    2000 9400   .031 4.6 .21 .029 4.6 .19 3.0   140 38    170   810 1700 880   670   7100 900    54 11000   8.5 360 62 7.7 330 61 8.4 340 67 .027 7.6 .078
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 540     340 6200    880    670   4300   .78 61 9.4 .51 43 5.2 910   6800 12000 23    15000 300   .030 4.6 .15 .028 4.6 .30 22     15000 260    910   6700 12000 880   1000   8200 13    340 65   8.9 340 74 9.6 370 80 9.6 350 79 .025 7.6 .11 
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .50  43 4.1  18    98   220   .25 24 3.1 .55 42 5.7 210   15000 2000 900    3500 7800   .033 4.6 .19 .027 4.6 .21 3.0   150 45    210   15000 1900 880   460   9800 .27 18 3.4 9.5 360 84 8.5 360 72 9.0 360 74 .027 7.4 .15 
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i no-overflow 2.1   41 25    .64 24   8.1 .87 69 10   .51 43 4.6 900   6900 12000 22    15000 330   .032 4.6 .18 .052 4.6 .20 22     15000 290    910   7100 11000 880   670   7300 .95 54 13   9.0 360 73 9.0 350 75 8.5 360 68 .031 7.5 .12 
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i no-overflow .31  37 3.8  .23 12   3.6 .95 61 14   .53 43 4.9 900   1400 7100 900    2100 7600   .028 4.6 .17 .029 4.7 .25 3.0   140 44    900   1400 8000 880   670   6500 900    71 12000   8.6 360 71 8.2 360 63 7.8 340 68 .021 7.8 .17 
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i no-overflow 5.0   45 41    880    300   11000   .71 71 9.8 .53 44 5.4 910   6400 11000 23    15000 260   .034 4.6 .23 .030 4.8 .22 22     15000 330    910   6400 11000 880   750   8800 1.8  110 16   8.2 350 69 8.9 360 72 8.2 330 67 .021 7.6 .11 
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i no-overflow 1.1   40 14    .50 16   6.2 .48 30 6.7 .54 43 5.0 910   6700 11000 22    15000 290   .046 4.6 .16 .031 4.7 .29 22     15000 270    900   7000 12000 880   670   6500 .26 17 3.8 7.9 340 66 8.3 340 65 8.3 360 66 .033 7.7 .15 
busybox-1.22.0/sleep_true-no-overflow_true-valid-memsafety.i no-overflow .72  39 9.0  .69 24   8.6 .72 85 9.8 .51 42 5.1 7.9 320 66 890    680 10000   .037 4.6 .12 .030 4.7 .24 3.5   170 55    7.8 330 76 880   730   7300 .27 17 2.7 8.9 360 74 8.7 350 73 8.9 360 74 .027 7.7 .12 
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 48     110 450    56    160   550   3.4  180 47   .49 42 4.7 900   2200 10000 23    15000 250   .030 4.7 .18 .028 4.7 .18 22     15000 280    900   2200 11000 880   1400   6700 900    170 13000   9.9 370 77 10   360 82 10   370 79 .022 7.6 .12 
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i no-overflow .27  35 2.7  .17 10   1.8 .24 16 2.7 .54 43 4.7 40   620 460 900    870 11000   .027 4.7 .19 .046 4.6 .18 3.0   140 50    40   640 430 880   680   6800 900    130 8200   8.2 360 65 7.9 340 61 8.3 340 69 .025 7.2 .13 
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i no-overflow 4.5   41 38    2.1  39   28   .68 55 8.0 .58 42 4.4 900   6800 12000 23    15000 300   .035 4.6 .29 .032 4.8 .11 22     15000 260    900   7000 11000 880   680   7600 .78 45 9.2 8.8 330 71 9.5 340 72 8.4 340 72 .022 7.3 .092
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i no-overflow .33  41 3.7  .87 28   12   1.3  110 19   .52 42 5.6 900   3600 11000 22    15000 280   .031 4.6 .19 .028 4.6 .14 22     15000 250    900   3500 11000 880   3700   13000 .78 48 6.9 8.9 360 69 9.2 360 74 9.6 370 76 .032 7.1 .10 
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 23     68 250    880    670   5500   2.7  170 40   .53 42 4.8 30   570 310 900    15000 8000   .031 4.6 .13 .029 4.6 .21 3.3   170 50    30   560 330 880   420   6600 .82 61 10   9.4 360 64 9.2 350 68 8.8 360 74 .027 7.2 .082
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 4.1   47 46    2.2  110   32   .59 35 8.8 .52 42 5.4 910   7500 11000 23    15000 300   .031 4.6 .23 .034 4.6 .21 22     15000 300    910   6900 9000 880   720   7100 1.6  120 16   8.8 360 75 9.1 340 75 9.5 360 78 .025 7.4 .13 
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i no-overflow 1.1   41 11    .85 120   11   .50 32 6.5 .50 43 4.5 900   6600 11000 22    15000 270   .029 4.6 .20 .045 4.7 .16 22     15000 270    900   6600 9900 880   640   8100 .77 54 8.6 7.8 340 69 8.5 360 68 8.5 360 66 .021 7.5 .12 
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i no-overflow 4.2   42 38    1.6  34   23   .70 77 11   .52 43 5.4 900   6800 11000 23    15000 330   .031 4.8 .20 .060 4.6 .21 22     15000 280    900   6900 11000 880   730   6400 1.2  72 13   9.1 360 79 8.6 360 70 8.4 350 69 .023 7.3 .11 
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i no-overflow .38  37 4.8  .18 12   2.3 .57 39 6.8 .51 43 5.4 140   800 1700 900    810 11000   .038 4.6 .14 .029 4.6 .26 3.4   180 44    140   790 1200 880   510   8900 900    150 9300   8.6 350 69 8.0 320 59 7.9 340 60 .018 7.5 .11 
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i no-overflow 8.7   46 100    4.9  76   55   2.0  210 23   .55 42 5.2 910   6500 12000 22    15000 260   .028 4.6 .22 .042 4.7 .16 22     15000 250    910   6600 13000 880   780   7100 2.0  99 22   9.0 370 72 8.5 340 70 8.9 350 77 .022 7.5 .18 
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .38  42 3.4  880    610   7200   .29 23 3.7 .51 42 5.6 910   6200 11000 22    15000 240   .030 4.6 .15 .045 4.6 .17 22     15000 260    910   6300 13000 880   1100   5100 .90 58 12   8.9 350 73 8.5 350 72 8.6 350 74 .022 7.7 .091
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i no-overflow 1.3   42 13    .56 22   7.3 .77 67 13   .53 44 5.1 910   7000 11000 22    15000 260   .035 4.8 .22 .031 4.7 .17 22     15000 310    910   7500 12000 880   660   8400 1.0  58 11   8.7 350 76 9.0 350 79 8.7 360 77 .021 7.2 .12 
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow .29  37 3.0  .18 12   2.1 .27 27 4.3 .56 44 5.1 300   15000 2300 900    920 12000   .031 4.6 .14 .029 4.6 .16 3.0   140 39    310   15000 2700 880   460   7900 900    130 7500   8.7 350 67 8.5 360 73 8.6 340 69 .027 7.2 .10 
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i no-overflow .30  37 3.4  .18 12   2.0 .61 80 6.7 .50 42 4.5 900   1100 5700 170    850 1800   .033 4.6 .16 .062 4.7 .22 3.4   160 44    900   970 7000 880   560   6600 900    93 11000   8.1 330 60 8.3 360 71 8.5 330 71 .021 7.6 .14 
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i unreach-call 3.0   290 25    3.1  220   26   260    15000 2100   53    1700 470   21   910 180 16    40 210   2.5   240   31    2.3   230   29    15     4700 170    380   1700 2800 860   940   12000 4.1  62 62   61   1000 520 65   1000 550 570   4700 7400 53     870   580    
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i unreach-call 2.6   260 28    880    1900   5300   .50 42 6.7 26    720 220   960   9300 7600 48    140 570   1.6   210   22    1.7   210   21    .43  130 5.0  68   2300 690 71   520   690 .96 50 14   900   4100 8400 450   2500 5900 900   3700 8200 900     1900   7700    
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i unreach-call 2.6   330 21    600    4000   5400   .73 60 9.3 32    1100 270   960   7500 8300 140    300 1800   1.7   210   19    1.7   210   22    .87  210 13    81   1600 600 16   300   210 2.4  140 17   900   5100 7400 240   2900 2500 900   5200 9200 900     1200   8100    
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i unreach-call 1.3   110 10    120    2100   820   2.9  130 29   900    8500 9000   960   6100 10000 900    3100 8000   1.8   210   26    1.8   210   27    24     2000 260    250   2500 2100 890   730   8000 900    2900 9400   900   2400 11000 900   2400 12000 900   6600 10000 86     1100   920    
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i unreach-call 98     15000 1000    880    3900   6900   5.6  470 63   100    3600 910   19   680 170 7.4  30 100   1.8   210   28    1.8   210   24    40     3000 440    490   2800 5000 49   300   560 1.3  31 16   11   390 87 11   380 76 12   380 90 140     1200   1600    
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i unreach-call 3.0   120 25    880    2100   6700   340    15000 2900   900    8200 11000   89   2600 800 380    8000 3600   1.7   210   20    1.7   210   23    160     15000 1900    250   2700 2600 13   280   170 900    2800 8200   900   5600 11000 270   2500 2800 900   5500 7400 730     890   7300    
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i unreach-call .72  61 5.0  880    2100   4200   9.0  810 100   900    4500 11000   960   9200 7400 2.7  170 29   1.7   210   22    1.6   210   25    47     1000 590    910   6400 8900 14   300   180 1.3  75 14   900   4000 9500 900   3400 9900 900   3300 10000 270     3000   2600    
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i unreach-call 22     1400 140    880    2900   4600   6.6  400 78   900    11000 5300   170   4100 1800 900    6800 7500   1.8   210   23    1.7   210   26    900     6500 9300    170   2200 2300 70   2000   940 10    250 83   900   8700 5600 900   4400 9300 900   8400 5500 900     990   10000    
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i unreach-call 130     15000 970    880    1900   11000   350    2400 5300   39    1100 340   140   4200 1400 18    1300 220   2.0   220   29    2.0   220   24    6.2   1300 97    370   2500 3300 900   2800   10000 3.1  49 43   900   7000 10000 900   5800 9300 900   6700 11000 58     640   480    
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i unreach-call 1.3   68 12    880    2000   4500   330    15000 3400   900    7600 11000   29   990 250 1.0  330 11   8.7   440   120    1.7   210   21    1.0   320 11    81   1600 970 13   220   160 .84 56 10   900   3500 9600 260   2300 3000 900   4800 11000 73     750   780    
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i unreach-call .47  52 5.1  22    97   320   12    140 200   900    11000 7200   23   810 180 5.5  180 67   8.5   430   120    1.6   200   21    4.9   250 59    49   1600 560 7.4 150   94 .60 29 7.1 510   4800 4700 240   2900 2600 500   5100 4500 710     2200   8300    
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i unreach-call .53  54 4.0  110    3000   1600   5.4  180 81   900    7500 9900   620   6200 6500 .93 140 12   8.8   430   110    1.6   200   20    1.1   140 13    55   1600 550 18   190   250 .63 34 8.8 94   1500 820 900   1800 9700 420   3100 5900 170     1200   2100    
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i unreach-call .40  47 3.3  1.2  83   14   380    15000 4000   910    11000 7800   150   2800 1500 900    780 11000   8.5   430   110    1.6   200   20    1.4   130 21    75   1900 700 10   190   120 3.7  32 49   900   2200 11000 150   2400 1600 900   4300 11000 690     4500   7300    
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i unreach-call .42  47 3.7  2.6  210   33   1.0  75 13   910    11000 7400   930   5900 9100 .64 120 7.3 1.6   200   21    1.6   200   20    .63  120 8.9  83   1700 860 18   220   240 900    2200 13000   150   2000 1400 210   2400 2500 430   3500 5700 300     1000   3500    
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i unreach-call 36     420 260    880    4100   6900   210    15000 2200   18    510 140   100   1600 1300 900    12000 7900   1.7   210   24    1.7   210   22    880     15000 5900    77   1200 620 42   690   500 1.6  100 16   36   1200 280 240   2900 2500 36   1000 290 43     1000   340    
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i unreach-call 3.2   290 18    9.7  470   110   250    15000 2900   27    880 240   110   3600 1300 16    40 230   2.5   240   36    2.3   230   27    62     15000 700    460   3400 3500 150   400   1400 4.2  63 60   64   1000 540 63   1000 520 520   4200 6500 180     3000   1900    
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i unreach-call 1.6   130 19    880    5300   5000   180    15000 2400   12    470 95   120   3800 1200 900    3100 8300   1.7   200   21    1.6   200   23    900     2200 6300    47   2400 470 6.3 170   81 900    2900 7100   28   840 230 120   1800 1300 31   760 260 58     2000   510    
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i unreach-call 26     5400 240    880    3300   7300   320    15000 2400   12    460 100   98   1500 1000 900    10000 6600   1.6   210   22    1.6   210   24    900     10000 7500    36   1200 330 5.6 180   82 .59 25 7.6 30   1100 230 900   2600 7000 30   1100 240 29     670   240    
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i unreach-call .61  59 5.4  880    1700   5700   100    2700 840   19    640 150   150   2300 1900 900    9500 12000   1.6   200   19    1.6   200   20    900     1800 11000    900   9700 9100 7.4 220   110 900    3200 13000   67   2500 780 900   3500 8600 33   930 280 150     6000   1500    
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i unreach-call 4.9   460 32    5.9  360   50   8.9  540 80   37    1500 320   120   2300 1200 24    49 320   2.5   250   32    2.6   250   35    19     6100 220    910   1700 4400 900   12000   8500 6.1  88 68   900   5300 13000 900   5400 12000 900   5300 13000 760     6200   9200    
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i unreach-call .33  39 3.0  2.3  180   27   180    15000 2500   8.3  330 73   8.7 450 69 900    2100 6500   8.3   430   95    1.6   200   22    900     1800 8100    97   2500 910 4.1 100   57 .40 21 5.9 16   540 130 25   720 200 17   540 120 22     620   180    
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i unreach-call .63  64 4.3  .99 51   12   180    15000 1300   15    510 130   99   1300 1300 900    2500 6100   8.9   440   120    1.7   210   24    3.5   230 43    75   1500 980 6.9 170   81 .69 38 8.2 39   2200 350 220   4400 2300 40   2000 370 60     2900   530    
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i unreach-call .27  42 2.4  880    1100   9900   240    15000 2300   11    460 83   960   6600 7000 1.2  67 14   8.4   430   120    1.6   200   20    .33  39 3.7  18   1200 150 880   370   9400 900    74 9700   21   590 180 17   630 140 21   660 170 17     260   150    
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i unreach-call 2.0   210 15    330    13000   4100   66    890 880   15    500 130   100   1700 1200 900    5000 8100   9.0   440   110    1.7   210   23    900     3800 6300    120   1500 1800 15   350   190 1.6  110 16   34   920 290 130   4200 1600 34   920 290 40     970   350    
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i unreach-call 53     880 280    880    4100   4900   3.6  250 38   25    820 200   100   2500 1200 900    7800 7300   1.7   210   21    1.8   210   23    900     2300 6600    95   1300 730 43   420   520 2.3  180 22   43   1300 380 160   4000 1500 45   1600 430 51     1100   410    
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i unreach-call 1.6   110 13    880    3800   3900   250    15000 2200   13    360 110   100   2400 1300 900    8400 9300   8.6   440   120    1.7   200   21    89     1400 940    52   1500 600 8.5 170   120 .83 56 9.0 120   3600 1400 550   4700 6700 120   2700 1600 40     960   320    
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i unreach-call .29  40 3.1  .64 60   8.6 12    920 140   12    480 110   180   4500 1600 .37 62 4.5 8.4   430   120    1.6   200   20    .35  57 4.0  180   3100 1500 880   610   8600 900    66 9600   53   1100 410 95   1300 1000 180   3500 1900 30     440   320    
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i unreach-call 2.8   110 18    880    2400   4700   150    15000 1300   12    470 95   100   1600 1300 560    15000 6200   8.5   430   120    1.6   200   20    900     9400 7000    79   1500 1000 6.1 170   77 .72 46 8.4 10   380 81 9.3 380 83 10   380 77 75     1100   820    
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i unreach-call 1.3   86 12    140    2900   900   280    15000 2200   18    520 140   100   1400 1400 900    3400 6000   9.0   440   120    1.6   210   21    640     3700 4400    130   1600 1500 8.2 170   110 1.5  74 18   42   1500 410 130   2500 1400 41   1500 370 42     950   340    
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i unreach-call .60  45 5.6  880    1200   4400   140    15000 1600   8.9  390 82   100   4400 780 900    8400 11000   8.6   430   110    1.6   200   22    12     240 160    38   1400 410 4.5 110   55 .51 23 7.2 20   590 160 230   4700 2700 20   580 170 31     760   280    
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i unreach-call .99  51 10    880    1200   5000   1.1  100 14   13    490 110   23   700 210 440    15000 5800   8.5   430   110    1.6   200   21    900     14000 12000    910   7100 11000 6.8 180   88 900    260 12000   25   760 210 78   1900 680 25   770 220 33     860   260    
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i unreach-call 7.2   96 56    880    2500   4300   8.9  660 79   19    650 170   100   2200 1300 900    13000 6300   9.2   440   110    1.7   210   20    360     15000 2900    170   1900 1700 39   440   550 4.4  160 48   14   340 120 15   340 110 15   330 120 23     450   200    
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i unreach-call .35  43 3.7  .69 60   9.6 11    810 130   52    2600 500   940   5900 10000 900    600 14000   8.7   550   96    1.6   200   24    900     5800 11000    27   1200 230 880   750   6800 24    44 290   56   1200 450 130   1700 1500 56   1100 500 27     450   250    
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i unreach-call .98  59 8.9  16    710   180   110    8400 1300   22    680 180   100   2800 1000 900    13000 8400   8.7   430   120    1.6   200   19    480     15000 4400    49   1400 550 890   1400   9400 900    2800 8800   100   2000 850 160   2900 1500 900   4900 11000 82     2800   760    
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i unreach-call .56  47 4.7  880    970   7000   230    15000 2100   18    580 160   960   7600 11000 1.2  110 14   8.5   430   110    1.6   200   25    1.9   130 23    960   7100 8600 890   520   7700 900    65 9500   900   5500 6200 130   1100 1400 900   5400 6400 820     960   10000    
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i unreach-call 1.6   83 12    100    14000   1000   99    7800 980   17    540 150   110   4200 920 900    3800 8400   1.7   210   24    1.7   200   23    150     3600 1600    84   1600 580 11   180   150 1.4  69 13   40   1200 320 75   1700 670 39   1200 390 160     1900   1900    
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i unreach-call 1.4   76 10    880    2800   5800   1.2  100 13   13    470 100   100   1800 1300 700    11000 8400   8.5   430   120    1.6   210   23    21     570 200    39   1300 450 7.2 170   100 .88 79 10   44   1500 370 150   2700 1700 43   1400 380 49     1600   420    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 110     15000 830    880    4800   6000   5.9  450 55   37    1500 330   960   6900 11000 31    1700 350   2.3   250   28    2.3   250   29    62     2300 660    890   2500 4800 310   980   3200 12    310 130   600   15000 7900 900   4800 9800 550   15000 6400 260     2800   2900    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb_false-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call .55  52 6.2  510    13000   6200   470    15000 4600   31    1100 280   51   1100 500 19    150 250   8.5   440   130    1.6   200   19    7.0   150 95    62   1600 630 880   330   6000 .47 25 5.8 72   2300 660 220   2700 2900 86   2800 770 98     1100   1000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 1.5   75 13    48    13000   590   320    15000 2500   58    1900 440   900   4400 7300 8.8  250 110   9.6   440   140    1.6   210   19    900     6600 14000    110   1900 1200 31   300   480 1.0  59 12   900   2500 11000 900   2100 11000 900   3000 10000 71     880   710    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--isdn--capi--kernelcapi.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 1.1   110 8.0  880    1700   5300   1.2  110 11   18    660 140   11   440 84 1.1  180 10   1.7   210   24    1.7   210   24    .99  170 9.0  240   2700 2500 890   1300   10000 1.2  30 15   13   390 100 14   390 110 12   370 96 94     760   1200    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 2.7   250 21    85    13000   1100   3.6  270 37   23    840 180   79   2900 1100 2.4  430 28   9.4   460   130    1.9   220   24    2.3   420 26    380   4000 4100 900   5900   9900 900    1100 4100   10   490 83 9.6 490 74 10   500 78 280     2600   3000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 340     6100 3900    880    2100   4400   2.1  190 17   35    930 280   970   9000 8400 110    280 1100   9.6   460   140    1.8   220   29    900     330 12000    960   5900 6800 89   870   1000 5.3  190 50   900   3600 12000 900   2500 13000 900   2100 10000 100     15000   1100    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--mem2mem_testdev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call .89  68 7.3  65    13000   790   .80 58 8.0 14    510 120   12   520 100 39    110 460   9.0   440   120    1.7   210   22    .48  120 6.5  58   1500 600 9.9 200   130 1.2  46 14   400   5000 4400 720   3500 8300 400   4300 4000 80     1100   970    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--vivi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 1.1   84 8.1  68    14000   860   88    4000 540   31    1000 240   960   7700 9800 47    130 530   8.9   440   110    1.7   210   26    .59  140 5.5  270   2100 2700 880   280   11000 .96 60 11   900   4400 9300 900   4700 14000 900   5300 7800 640     1300   4700    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--mtd--chips--cfi_cmdset_0001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 1.5   130 14    880    740   8300   880    4200 11000   13    530 110   12   440 95 74    190 800   9.1   450   120    1.7   210   21    .89  150 11    240   2700 2200 14   190   210 1.2  32 19   480   2900 3100 180   850 1900 470   2900 3100 900     320   12000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 1.1   79 9.1  51    13000   580   3.5  330 44   20    620 160   46   2000 420 900    600 11000   1.7   210   20    1.7   210   25    2.4   140 27    170   2000 1800 23   260   300 .89 52 10   900   3400 8900 900   4800 6900 900   4400 9300 56     1200   610    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 320     190 3500    880    4300   4800   2.2  210 30   14    520 120   13   530 95 .71 100 8.4 8.9   440   100    1.7   210   22    .65  94 6.9  230   1800 2800 24   410   310 .77 28 9.1 900   4400 11000 170   1200 1800 900   4500 13000 90     1100   1000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 110     15000 830    880    8300   7200   8.7  600 79   42    1400 370   55   1100 510 15    990 170   12     520   170    2.3   250   31    900     1700 12000    910   1700 4700 900   1500   7100 3.0  73 36   650   5300 8100 900   3900 11000 650   5300 8400 900     2500   5200    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 110     15000 860    880    2600   5600   4.2  320 40   19    570 140   360   1300 3000 1.3  220 13   9.4   450   130    1.8   220   27    1.5   220 15    960   5400 7300 900   11000   11000 900    3100 8500   110   1900 1100 500   2500 7400 160   4700 1900 39     450   350    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call .52  56 4.5  35    2200   330   17    600 190   9.8  510 83   8.4 400 80 .40 65 5.7 8.4   440   110    1.6   200   23    .34  58 4.6  29   1200 300 7.0 120   83 .70 22 9.3 48   870 380 110   620 1400 47   830 430 45     680   490    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--storage--usb-storage.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 900     15000 10000    880    1700   11000   8.3  570 73   17    570 140   23   780 220 1.3  220 13   9.2   450   120    1.8   220   25    1.2   210 12    320   2900 3600 900   4700   10000 1.5  51 16   440   5200 5000 810   4800 8600 450   5100 6100 42     500   340    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--vhost--vhost_net.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 110     3000 1100    880    6800   5700   3.0  230 35   20    610 160   14   550 120 5.2  270 76   1.8   220   21    1.8   220   22    7.2   310 85    290   1600 2400 35   720   460 1.8  78 25   900   6200 7000 510   2400 5000 900   6000 5800 190     1400   2300    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call 13     1100 97    880    4300   5900   2.6  180 23   900    6200 11000   960   7600 9000 900    1900 8300   9.4   460   130    1.8   220   22    190     910 1600    960   5900 9200 900   410   11000 3.0  130 43   900   5100 8700 900   4000 11000 900   6400 12000 330     6400   2300    
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.i unreach-call 1.2   180 10    830    2300   8700   200    15000 2500   9.7  720 83   9.9 730 82 20    190 280   9.2   440   140    1.8   210   26    .42  110 4.9  9.8 710 76 7.7 140   96 1.0  33 13   17   530 130 16   510 150 17   500 140 45     380   400    
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i unreach-call 2.1   260 18    39    12000   570   5.0  240 57   44    2300 410   86   4000 760 25    250 330   1.9   210   21    1.9   210   24    .73  180 7.7  540   4100 3200 12   210   160 900    2600 9000   18   660 160 18   650 140 17   580 140 180     2900   2000    
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.i unreach-call 560     1400 5700