Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution [2017-12-01 08:19:20 CET; 2017-12-01 10:20:37 CET; 2017-11-30 11:20:26 CET] [2017-12-01 08:19:34 CET; 2017-12-01 11:16:27 CET; 2017-11-30 11:20:26 CET] [2017-12-01 08:37:17 CET; 2017-12-01 08:43:54 CET; 2017-11-30 11:20:26 CET] [2017-12-01 08:43:39 CET; 2017-12-01 08:51:01 CET; 2017-11-30 11:20:26 CET] [2017-12-01 08:22:21 CET; 2017-12-01 10:49:29 CET; 2017-11-30 11:20:26 CET] [2017-12-01 09:05:19 CET; 2017-12-01 13:07:37 CET; 2017-11-30 16:01:31 CET] [2017-12-02 00:00:31 CET; 2017-12-02 06:23:16 CET; 2017-12-01 08:49:27 CET] [2017-12-02 11:31:00 CET; 2017-12-02 18:23:42 CET; 2017-12-01 12:59:33 CET] [2017-12-05 13:45:25 CET; 2017-12-05 13:47:25 CET; 2017-12-05 07:52:24 CET] [2017-12-02 23:08:57 CET; 2017-12-03 04:09:48 CET; 2017-12-01 22:41:19 CET] [2017-12-03 04:39:25 CET; 2017-12-03 11:17:40 CET; 2017-12-02 01:06:24 CET] [2017-12-03 04:40:15 CET; 2017-12-03 11:17:40 CET; 2017-12-02 02:33:02 CET] [2017-12-03 07:53:44 CET; 2017-12-03 08:43:49 CET; 2017-12-02 17:23:13 CET]
Run set 2ls.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cbmc.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cpa-bam-bnb.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cpa-bam-slicing.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] depthk.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] esbmc-incr.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] esbmc-kind.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] interpchecker.[sv-comp18; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] symbiotic.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] uautomizer.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] ukojak.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety] utaipan.[sv-comp18.Systems_BusyBox_MemSafety; sv-comp18.Systems_BusyBox_NoOverflows; sv-comp18.Systems_DeviceDriversLinux64_ReachSafety]
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --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)
busybox-1.22.0/basename_false-valid-deref.i valid-deref valid-free valid-memtrack .31  32 2.8  55    870 490   .49 41 3.9 .46 40 3.6 3.5 270 30 900   1300 5900 780     1300 8200    400     1200 4000    .45 39 4.1 2.0  310 23   7.6 230 61 7.6 230 64 8.2 230 62
busybox-1.22.0/head_false-valid-deref.i valid-deref valid-free valid-memtrack .41  41 4.5  5.0  65 56   .49 41 4.9 .47 41 4.5 4.4 270 36 900   2900 9900 5.0   210 78    .23  34 2.5  .44 40 3.8 18    3200 200   900   4700 10000 900   5500 12000 900   5100 9500
busybox-1.22.0/sleep_false-valid-deref.i valid-deref valid-free valid-memtrack 2.3   39 24    1.7  49 23   .48 41 4.7 .43 40 4.1 4.2 270 37 900   2500 11000 5.6   230 76    .19  32 2.3  .43 40 4.2 .22 12 2.8 900   2000 10000 900   3600 12000 900   4700 9900
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i valid-deref valid-free valid-memtrack .47  37 4.6  .84 45 8.8 .49 41 3.8 .45 40 4.1 4.3 290 39 900   3100 6000 4.8   190 58    .17  31 2.0  .43 40 3.8 2.5  410 30   900   1800 10000 900   2900 12000 900   4700 12000
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .31  32 2.6  870    2200 4300   .48 44 4.9 .49 40 4.4 4.0 290 30 890   1300 6000 900     1100 10000    900     1300 10000    .47 40 4.2 900    560 11000   7.8 220 64 8.0 230 61 7.7 230 66
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.4   38 12    1.1  44 14   .49 40 4.4 .46 41 3.8 4.4 270 40 900   880 11000 4.8   190 57    .21  31 2.3  .44 41 3.8 900    900 13000   900   2200 11000 900   4100 15000 900   4800 10000
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 35     87 470    8.9  110 110   .48 41 4.1 .43 38 3.4 4.7 270 39 44   46 550 4.8   200 69    .22  38 2.5  .41 40 3.9 42    6300 530   900   2600 11000 900   5600 13000 900   5900 10000
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .50  46 3.9  4.3  160 51   .47 41 4.3 .41 40 4.2 5.1 270 44 49   50 640 4.9   210 74    .24  41 3.2  .42 40 4.5 130    13000 1400   8.5 230 70 8.9 230 72 8.8 230 69
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .27  31 3.0  730    12000 9400   .49 40 4.4 .46 40 3.9 3.9 290 33 890   980 5100 900     4400 10000    900     3800 9300    .44 41 4.3 900    2300 10000   7.7 230 68 7.6 230 64 7.7 230 65
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 18     69 200    69    260 710   .49 41 4.1 .44 40 3.8 5.1 300 46 45   47 570 4.8   210 78    .23  38 2.7  .43 40 4.3 45    6100 500   900   13000 7200 900   5300 10000 900   5200 9400
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 1.1   38 12    870    9900 4100   .48 40 4.1 .45 40 4.3 4.3 290 39 890   750 12000 7.0   330 99    .22  32 2.1  .41 40 4.3 900    1500 10000   900   2500 10000 900   3900 14000 900   4800 10000
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 120     130 850    38    270 420   .50 41 4.8 .42 41 4.0 4.9 280 39 46   47 620 5.7   250 67    .25  40 2.5  .44 40 4.0 180    11000 2300   900   3600 10000 900   5600 12000 900   5600 9800
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 14     62 170    4.8  66 74   .48 41 3.9 .45 40 3.7 4.8 270 37 42   45 570 5.6   250 75    .23  37 2.9  .41 40 3.7 79    4900 840   900   2500 7200 900   4800 11000 900   5000 13000
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .26  34 2.4  870    6500 10000   .48 41 4.3 .43 40 4.0 3.9 290 30 890   1100 7900 900     1600 12000    900     1800 13000    .41 41 3.8 900    2300 12000   900   1800 12000 900   1900 11000 900   2700 11000
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .45  37 3.9  .78 44 8.2 .48 40 4.1 .47 40 4.3 4.4 290 35 900   920 10000 4.8   190 57    .18  31 1.9  .43 40 3.7 900    500 13000   900   2300 11000 900   2100 12000 900   3700 12000
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 900     340 5500    870    710 4000   .45 40 4.8 .47 41 4.1 5.6 290 45 58   59 670 .20  50 2.3  .24  50 2.3  .43 40 4.1 900    320 10000   9.5 240 73 9.3 240 70 9.6 240 75
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 6.5   45 70    870    1200 3800   .47 41 4.2 .43 40 4.4 4.9 270 41 43   45 510 4.9   200 77    .21  38 2.8  .44 40 4.0 30    4300 380   900   3200 6300 900   5100 13000 900   5600 12000
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .44  35 3.5  .83 43 7.6 .46 40 4.2 .44 39 4.0 4.1 300 35 900   3000 11000 4.8   190 56    .19  30 1.9  .43 40 4.2 900    1400 11000   900   3200 9800 900   2200 11000 900   3700 11000
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 900     630 11000    870    800 4800   .45 40 4.6 .47 40 4.2 6.4 310 53 61   56 720 5.0   220 56    .29  52 3.7  .42 40 4.1 150    15000 1800   6.1 310 52 5.6 280 42 5.9 300 49
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .56  45 5.2  26    140 300   .50 43 4.2 .47 41 4.1 4.7 270 37 900   2600 9600 4.9   200 58    .23  37 1.9  .42 40 4.0 .26 13 2.5 290   2900 3000 900   5500 15000 900   5100 10000
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 6.5   43 78    1.6  50 18   .47 40 4.3 .48 41 3.9 4.5 270 40 40   43 470 4.8   200 74    .24  36 2.1  .43 41 4.1 27    3900 360   900   2100 9100 900   3500 11000 900   4700 10000
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .48  37 5.1  .86 45 8.6 .46 40 4.1 .43 40 4.1 4.1 270 32 900   3900 11000 4.8   190 63    .21  31 2.1  .44 40 3.7 900    1500 9400   900   2000 10000 900   2100 13000 900   3600 8500
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 16     68 170    870    340 11000   .49 40 4.1 .46 41 4.2 5.1 290 47 43   46 570 4.9   200 61    .22  38 2.5  .46 41 4.3 40    5600 510   900   2400 9200 900   3700 14000 900   4800 11000
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 4.1   40 52    1.5  57 18   .49 41 4.2 .46 41 4.0 4.4 280 36 39   43 480 .13  35 1.2  .13  35 1.3  .43 38 4.0 .24 13 2.5 8.5 230 76 8.6 240 79 8.5 230 64
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 250     210 2300    69    230 660   .48 41 4.2 .47 41 4.0 2.5 180 24 900   2500 12000 5.7   250 71    .32  52 3.6  .44 41 4.0 51    15000 740   9.3 310 79 9.5 310 73 9.9 300 75
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .37  35 3.8  .66 42 8.4 .48 41 4.1 .49 40 3.9 3.9 270 33 890   1300 6300 4.8   190 71    .19  30 1.8  .43 40 4.6 900    360 12000   360   2100 4300 900   2100 14000 900   3600 12000
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 13     58 140    3.9  59 48   .46 41 4.1 .45 41 4.6 4.6 270 43 40   43 560 4.8   200 63    .20  36 2.2  .42 40 3.5 27    3800 320   900   4700 10000 900   4700 13000 900   4900 12000
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 8.4   49 95    2.0  53 24   .45 41 4.1 .45 40 4.1 4.5 270 34 40   43 480 4.8   200 64    .20  36 2.2  .41 40 3.9 29    4000 410   900   13000 5800 900   5200 9200 900   5200 9000
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 98     130 880    870    730 6700   .47 41 4.4 .44 40 4.2 4.9 290 46 890   1600 6200 5.6   310 70    .24  37 2.4  .43 38 3.7 12    2300 140   8.5 240 78 8.7 240 77 9.2 240 81
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 16     67 170    4.0  150 51   .48 40 4.1 .46 40 4.1 4.9 270 36 46   47 690 4.9   210 55    .23  39 2.9  .44 41 4.0 68    9300 800   900   3500 11000 900   5600 12000 900   5400 11000
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 4.1   41 37    1.9  170 22   .49 43 4.5 .47 40 3.8 5.3 290 37 40   43 540 4.8   200 64    .22  36 2.3  .43 41 4.2 23    3500 250   900   4800 9600 900   5500 12000 900   5900 11000
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 13     57 150    3.1  51 37   .47 41 3.8 .44 40 4.1 4.6 270 42 41   44 540 4.8   200 74    .23  37 1.8  .45 41 4.0 35    5000 510   900   2500 8200 900   4100 12000 900   4800 9700
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .81  37 9.6  .76 44 6.5 .45 40 4.2 .46 40 3.7 4.2 270 36 890   1400 7100 5.2   230 65    .17  31 2.1  .41 40 3.8 900    930 13000   900   1800 12000 900   2500 14000 900   3500 12000
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 28     81 300    8.4  110 110   .45 41 4.1 .43 40 3.8 2.7 180 27 46   48 620 4.9   210 71    .24  40 2.7  .43 42 4.1 74    10000 880   8.9 240 70 9.1 240 76 8.9 240 74
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .38  41 3.4  870    750 6600   .49 40 3.9 .44 40 4.1 5.1 290 36 41   44 520 5.6   250 77    .22  37 2.8  .43 41 4.0 30    4400 340   900   1900 11000 900   4400 14000 900   5000 12000
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack 4.7   41 43    1.6  52 21   .48 40 4.2 .47 40 4.1 4.8 290 45 40   44 480 4.8   200 74    .23  36 2.1  .43 41 4.1 27    3900 370   9.0 230 77 8.6 240 67 8.6 240 65
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .47  37 3.9  870    5500 9300   .47 41 3.9 .42 40 3.8 4.2 270 35 890   1200 6100 4.8   190 62    .17  31 2.5  .43 39 3.8 900    2400 10000   900   4900 10000 900   1900 12000 900   3900 11000
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack .44  37 4.3  .75 44 8.6 .48 40 4.4 .41 40 4.1 4.4 290 32 900   1200 10000 5.3   210 69    .17  31 1.9  .43 40 3.6 900    670 14000   900   2300 10000 900   2000 12000 900   3600 9800
busybox-1.22.0/chgrp-incomplete_false-no-overflow.i no-overflow .32  37 3.0  .76 44 7.3 .45 42 4.5 .47 40 4.2 900   1700 5700 900   2700 6500 3.5   150 39    .14  31 1.7  .42 42 4.1 900    330 14000   270   1600 2800 900   2500 12000 900   6400 12000
busybox-1.22.0/chroot-incomplete_false-no-overflow.i no-overflow .58  37 6.7  1.0  44 9.8 .46 40 4.6 .46 40 3.9 38   520 430 900   930 8200 3.4   150 50    .15  31 2.0  .41 39 4.0 900    210 11000   380   1700 3800 310   3300 3900 900   6000 13000
busybox-1.22.0/cut_false-no-overflow.i no-overflow 13     51 120    7.2  93 93   .46 40 4.1 .47 40 4.5 900   6100 12000 48   500 660 3.5   160 52    .18  38 2.5  .43 40 3.7 .47 23 6.7 900   2200 7100 900   5200 11000 900   5900 12000
busybox-1.22.0/date_false-no-overflow.i no-overflow .43  46 3.1  3.5  150 39   .50 41 4.6 .43 40 4.1 900   3300 10000 51   500 660 3.5   170 57    .21  40 3.0  .42 41 3.6 .60 33 7.3 4.3 230 34 4.3 240 34 4.5 240 35
busybox-1.22.0/du_false-no-overflow.i no-overflow 6.8   44 58    55    240 530   .45 40 4.4 .46 40 4.3 900   3400 9900 46   500 700 3.5   160 47    .22  38 2.0  .42 40 4.0 .47 24 6.4 900   12000 7400 900   4200 9800 900   5600 8600
busybox-1.22.0/echo_false-no-overflow.i no-overflow .50  38 5.0  870    4600 4300   .47 41 4.0 .47 40 4.1 900   1100 11000 890   700 9400 4.7   240 57    .16  32 1.9  .44 41 3.9 900    330 12000   900   3000 7600 900   5200 13000 900   6400 12000
busybox-1.22.0/expand_false-no-overflow.i no-overflow 31     72 300    30    250 320   .50 43 4.6 .44 40 4.2 900   5900 9200 60   940 730 4.0   190 59    .23  39 2.2  .45 40 4.0 .58 30 6.4 900   2700 6000 900   5400 13000 900   5700 12000
busybox-1.22.0/fold_false-no-overflow.i no-overflow 5.6   42 48    3.9  58 46   .46 41 4.5 .42 40 4.2 900   1100 9800 46   550 630 4.0   180 51    .22  37 2.7  .45 40 3.8 .43 19 5.3 900   1900 8000 900   5100 12000 900   4700 12000
busybox-1.22.0/head_false-no-overflow.i no-overflow .39  40 3.2  4.3  61 54   .47 40 4.2 .46 40 4.6 900   1300 6800 900   2400 10000 3.6   170 47    .19  34 2.1  .41 40 3.9 .35 16 5.3 900   5500 8700 900   4900 11000 900   6300 14000
busybox-1.22.0/logname_false-no-overflow.i no-overflow .32  37 3.2  .67 44 6.7 .47 42 4.6 .46 40 4.2 900   1300 5500 900   1000 13000 3.5   150 45    .14  31 1.6  .42 40 3.8 900    130 13000   76   1100 800 47   1000 430 900   6500 11000
busybox-1.22.0/ls-incomplete_false-no-overflow.i no-overflow 230     190 2100    870    710 3400   .49 40 4.1 .46 40 3.9 900   3100 11000 58   59 710 .20  50 2.2  .23  50 2.7  .48 40 4.1 .98 64 11   4.5 230 32 4.5 230 40 4.6 230 34
busybox-1.22.0/mkdir_false-no-overflow.i no-overflow 2.6   43 23    870    2200 2500   .43 40 4.3 .43 40 3.7 900   6200 10000 47   500 560 3.5   160 42    .19  38 2.0  .41 40 4.0 .44 19 4.6 900   1900 6700 900   5000 11000 900   5800 13000
busybox-1.22.0/mkfifo-incomplete_false-no-overflow.i no-overflow .30  36 2.8  .74 43 7.6 .49 45 4.6 .41 40 4.5 110   780 1100 900   1200 9600 3.5   150 45    .18  30 1.5  .43 42 4.0 900    220 13000   130   1200 1600 69   1500 690 900   6500 12000
busybox-1.22.0/od_false-no-overflow.i no-overflow 750     320 7200    870    890 7700   .49 41 4.6 .47 40 4.1 900   6300 11000 63   1700 750 3.6   180 46    .31  52 2.8  .42 40 3.8 .91 65 10   6.9 320 52 5.7 290 41 5.6 290 47
busybox-1.22.0/printf_false-no-overflow.i no-overflow .54  42 4.4  20    130 260   .47 41 4.2 .46 40 4.6 490   910 3100 900   2000 12000 3.5   150 44    .21  37 1.9  .44 41 3.9 .27 13 2.9 230   2000 1800 900   4800 13000 900   6100 12000
busybox-1.22.0/readlink_false-no-overflow.i no-overflow 2.8   40 23    1.4  49 16   .51 43 4.4 .45 39 4.1 900   6300 11000 39   43 470 3.5   160 45    .18  36 2.0  .43 40 3.8 .37 17 4.4 900   1800 8400 900   5000 11000 900   6000 14000
busybox-1.22.0/realpath_false-no-overflow.i no-overflow .36  37 3.1  .78 44 7.5 .48 41 4.4 .44 40 3.9 900   1500 6000 900   1200 13000 3.5   150 50    .18  31 1.6  .42 40 3.8 900    400 14000   160   1500 1600 110   2300 1200 900   6500 12000
busybox-1.22.0/rm_false-no-overflow.i no-overflow 6.4   44 60    870    400 11000   .47 40 4.0 .45 40 4.0 900   6200 11000 44   500 520 3.5   160 49    .21  38 2.0  .44 40 3.7 .46 21 5.5 900   1300 8900 900   6100 11000 900   6100 11000
busybox-1.22.0/seq_false-no-overflow.i no-overflow 1.6   40 15    1.3  57 13   .49 41 4.9 .44 40 3.6 900   6400 9900 42   500 630 .13  35 1.4  .15  35 1.4  .43 41 3.9 .25 13 2.8 4.4 240 39 4.5 240 38 4.3 230 34
busybox-1.22.0/sleep_false-no-overflow.i no-overflow .91  39 12    1.5  49 15   .46 41 4.4 .43 40 4.2 6.5 320 56 900   1000 9100 4.0   170 51    .20  32 1.9  .45 40 3.9 .24 12 3.0 570   2200 5800 280   3600 3600 900   5100 12000
busybox-1.22.0/stty_false-no-overflow.i no-overflow 73     120 670    53    210 670   .50 41 4.3 .43 40 3.8 2.5 180 22 900   2000 10000 4.2   200 54    .27  51 3.7  .42 40 4.2 900    370 13000   4.6 290 37 4.4 290 36 5.0 300 42
busybox-1.22.0/sync_false-no-overflow.i no-overflow .27  35 3.3  .65 42 6.9 .49 40 4.4 .44 40 3.9 46   580 490 890   1300 5700 3.4   140 45    .17  30 1.5  .42 40 4.2 900    150 15000   200   1400 2400 110   1800 1400 910   6300 10000
busybox-1.22.0/tac_false-no-overflow.i no-overflow 5.4   41 51    3.2  52 37   .50 41 4.4 .44 41 4.7 900   6200 8400 42   500 560 3.5   160 46    .19  36 2.1  .43 40 4.7 .39 16 4.0 900   3600 7700 900   5000 12000 900   5800 12000
busybox-1.22.0/tee_false-no-overflow.i no-overflow .35  41 3.3  1.7  52 19   .46 41 4.4 .42 38 3.7 900   3300 11000 43   500 620 3.5   160 50    .21  36 2.3  .43 42 4.0 .38 16 5.3 900   12000 7000 900   4500 11000 900   5300 7900
busybox-1.22.0/test-incomplete_false-no-overflow.i no-overflow 32     74 280    870    760 7100   .48 42 4.5 .46 40 3.8 900   4300 11000 890   1600 8000 3.8   180 48    .18  37 2.1  .41 40 3.5 .41 18 5.0 4.5 230 33 4.4 240 38 4.5 240 33
busybox-1.22.0/touch_false-no-overflow.i no-overflow 5.7   45 49    3.2  140 38   .46 40 3.5 .45 40 3.7 900   6200 9900 47   500 630 3.5   160 44    .23  39 2.4  .44 40 4.2 .52 26 5.6 900   2400 5900 900   5300 13000 900   6200 13000
busybox-1.22.0/uname_false-no-overflow.i no-overflow 1.6   41 14    1.6  160 18   .46 40 4.1 .45 40 4.3 900   6000 11000 43   510 610 3.5   160 46    .18  36 2.1  .43 40 3.9 .57 78 5.8 900   3100 7100 900   5400 10000 900   5900 11000
busybox-1.22.0/uniq_false-no-overflow.i no-overflow 5.5   41 43    2.6  50 29   .46 40 3.8 .43 40 4.2 900   6300 12000 44   510 550 3.5   160 49    .21  37 2.3  .42 40 3.7 .41 19 5.6 900   1300 8600 900   5000 13000 900   6100 12000
busybox-1.22.0/usleep_false-no-overflow.i no-overflow .47  37 4.1  .70 45 6.5 .47 40 4.3 .46 42 4.0 900   1200 5800 890   1400 5800 3.9   180 48    .18  31 1.5  .41 41 4.0 900    97 12000   200   3000 2300 200   2900 2500 900   4800 10000
busybox-1.22.0/uudecode_false-no-overflow.i no-overflow 11     48 94    6.9  98 73   .48 41 4.1 .46 40 4.3 2.6 190 22 50   500 710 3.5   160 51    .22  40 2.5  .41 40 3.5 .51 23 5.8 4.5 230 34 4.7 240 42 4.5 240 35
busybox-1.22.0/wc_false-no-overflow.i no-overflow .35  42 3.2  870    780 5000   .48 41 4.6 .45 40 4.6 900   5800 9600 45   510 550 4.0   180 48    .23  37 2.1  .45 40 3.9 .42 18 4.7 900   1800 8200 900   4900 13000 900   5500 11000
busybox-1.22.0/who_false-no-overflow.i no-overflow 1.7   42 14    1.3  50 16   .50 45 4.3 .44 40 4.4 900   6300 9400 40   44 510 3.5   160 42    .20  36 1.9  .44 40 3.9 .40 19 5.1 4.5 230 37 4.4 230 35 4.3 230 34
busybox-1.22.0/whoami-incomplete_false-no-overflow.i no-overflow - - - - - - - - .40 40 3.5 - - - -
busybox-1.22.0/yes_false-no-overflow.i no-overflow .33  37 3.0  .70 44 6.4 .49 43 4.8 .51 40 3.8 900   1300 7900 900   1200 9900 3.9   160 49    .16  31 1.9  .44 39 3.8 900    140 12000   190   1500 1900 53   1100 490 900   6700 11000
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .24  32 2.0  870    6800 4700   .47 41 4.6 .41 40 4.2 900   3400 11000 890   1300 5800 900     960 8800    900     1100 9000    .44 40 4.0 900    130 11000   3.9 220 33 4.2 230 36 4.0 230 33
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i no-overflow .29  37 3.5  .75 44 7.3 .49 40 4.0 .44 40 4.1 250   15000 2000 900   2700 7600 3.5   150 50    .17  31 1.8  .41 37 3.5 900    320 12000   380   1500 4000 900   2500 10000 900   6400 11000
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow .59  37 6.1  1.0  44 11   .46 40 4.7 .44 41 3.9 33   520 340 900   930 12000 3.5   150 49    .15  31 1.7  .42 40 3.9 900    210 13000   340   1800 2900 900   4700 10000 900   6000 14000
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 14     51 110    7.2  93 75   .46 41 3.9 .45 40 4.1 900   6100 11000 48   500 650 3.5   160 57    .22  38 2.2  .43 41 3.8 .48 23 5.4 900   2000 6800 900   5200 13000 900   5900 11000
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .45  46 3.4  3.5  160 40   .47 41 4.4 .44 40 4.1 900   3300 10000 49   49 630 3.5   170 44    .22  41 2.4  .44 40 3.8 .62 33 7.9 4.5 230 35 4.2 230 37 4.2 240 37
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i no-overflow .24  31 1.7  550    12000 6400   .46 40 3.8 .44 40 4.4 900   5200 9500 890   960 7500 900     9900 11000    900     9300 11000    .45 41 4.2 900    790 11000   4.1 230 32 3.9 230 36 3.9 230 34
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i no-overflow 6.8   44 57    52    240 550   .47 40 4.3 .47 40 4.1 900   3300 11000 47   510 540 3.5   160 45    .22  39 2.3  .44 40 4.2 .49 24 6.5 900   10000 5600 900   4300 9800 900   5500 9900
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i no-overflow .48  38 5.0  870    4600 3900   .46 40 4.5 .53 40 4.3 900   1000 9600 890   700 11000 4.7   240 66    .20  32 1.9  .44 40 4.2 900    320 11000   900   2900 8400 900   5300 11000 900   6500 11000
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 30     71 260    32    250 290   .48 45 4.5 .45 40 4.7 900   5900 11000 61   940 750 4.1   190 41    .24  40 2.5  .42 40 4.2 .59 30 7.9 900   2700 7700 900   5100 13000 900   5600 12000
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i no-overflow 5.4   42 41    4.0  56 48   .47 40 4.0 .46 41 4.2 900   930 10000 46   550 550 4.0   180 50    .20  37 2.3  .41 39 3.7 .41 19 4.4 900   2200 6800 900   5000 12000 910   4700 12000
busybox-1.22.0/head_true-no-overflow_true-valid-deref.i no-overflow .42  40 2.6  4.3  61 49   .46 40 3.8 .44 40 4.1 150   880 1200 900   2400 11000 3.7   170 47    .21  34 2.1  .44 40 4.5 .38 16 4.9 230   4100 2200 900   5000 12000 900   6600 11000
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i no-overflow .26  34 1.9  560    12000 7400   .50 44 4.5 .44 40 4.0 530   15000 5900 900   1100 5300 900     12000 11000    900     12000 10000    .42 40 4.2 900    980 13000   9.6 480 74 18   700 150 9.7 450 81
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i no-overflow .34  36 2.6  .68 44 6.3 .48 41 4.6 .46 40 4.2 290   15000 2000 900   1000 9900 3.5   150 43    .18  31 1.7  .44 38 3.9 900    140 14000   130   1000 1500 65   1200 640 900   6500 12000
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 230     190 2000    870    700 4200   .47 42 4.2 .44 41 4.4 900   3100 9100 58   59 680 .22  50 2.3  .23  50 2.1  .45 41 4.4 .97 63 14   4.8 230 38 4.9 250 39 4.4 230 34
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i no-overflow 2.6   43 20    870    2400 4500   .42 40 4.5 .47 40 4.2 900   6400 11000 47   510 670 3.5   160 47    .19  38 2.5  .44 40 4.0 .41 18 5.7 900   2100 6700 900   5100 12000 900   5900 12000
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow .30  36 2.4  .73 43 8.4 .45 40 4.6 .47 41 4.0 900   1300 5800 900   1200 13000 3.5   150 46    .17  30 1.8  .42 40 4.1 900    230 12000   160   1100 1600 81   1700 830 910   6600 12000
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 760     320 7400    870    830 4300   .48 40 4.0 .48 40 4.1 900   6300 10000 64   1700 760 3.6   180 47    .31  52 3.1  .45 41 3.6 .89 65 12   6.2 320 52 5.9 300 51 5.9 300 46
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .55  43 4.1  20    130 220   .50 43 4.5 .47 40 4.3 260   850 2200 900   2000 9500 3.5   150 46    .19  37 2.3  .43 40 4.0 .28 13 2.8 330   1900 2400 900   4800 12000 900   6200 12000
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i no-overflow 2.5   41 26    1.4  49 15   .48 42 4.1 .46 41 4.1 900   6200 13000 40   45 500 3.5   160 53    .18  36 2.5  .42 40 4.3 .40 17 4.2 900   2400 11000 900   5000 12000 900   6000 13000
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i no-overflow .33  37 3.5  .77 44 7.7 .47 41 4.2 .43 40 4.7 900   1500 6800 900   1200 12000 3.5   150 51    .15  31 1.8  .45 39 3.9 900    400 13000   190   1300 2100 120   3500 1300 900   6500 14000
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i no-overflow 6.0   43 55    870    400 10000   .49 43 4.6 .46 40 4.1 900   6400 11000 45   510 540 3.5   160 41    .19  38 2.1  .45 40 4.3 .46 21 5.2 900   2000 10000 900   5200 11000 900   6100 13000
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i no-overflow 1.6   40 14    1.3  57 14   .48 41 4.4 .44 40 4.3 900   6300 12000 42   500 490 .13  35 1.5  .12  35 1.4  .42 40 3.7 .23 13 2.9 4.5 240 34 4.4 230 35 4.4 240 32
busybox-1.22.0/sleep_true-no-overflow_true-valid-deref.i no-overflow .97  38 8.1  1.4  47 16   .45 42 3.8 .43 40 4.1 6.5 340 65 900   1500 11000 4.0   170 57    .16  32 2.0  .44 41 4.1 .23 12 3.0 630   3900 6400 280   3900 3900 900   5100 12000
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 70     120 600    54    210 470   .48 40 4.3 .41 40 3.4 2.8 200 27 900   2000 9300 4.2   200 59    .32  52 3.2  .44 42 4.1 900    210 14000   4.7 290 44 5.0 290 39 4.9 280 37
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i no-overflow .30  35 2.6  .66 42 6.4 .49 41 4.3 .41 40 4.1 40   700 530 890   1300 5700 3.4   140 45    .14  30 1.7  .44 40 3.8 900    150 12000   170   1400 1700 100   1700 1200 900   6400 11000
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i no-overflow 5.4   41 45    3.2  51 40   .49 43 4.3 .47 41 4.4 900   6300 10000 43   510 490 3.5   160 45    .18  36 2.1  .43 40 4.0 .36 16 4.1 900   3100 7600 900   5000 12000 900   6000 13000
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i no-overflow .36  41 2.8  1.7  53 16   .47 41 4.6 .43 40 4.2 900   3300 13000 43   510 550 3.5   160 45    .20  36 2.2  .40 40 3.6 .36 16 4.7 900   9900 6100 900   4500 9800 900   5600 9200
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 29     73 330    870    760 6400   .46 41 4.1 .43 40 4.0 900   4600 10000 890   1600 8300 3.8   180 49    .21  37 2.5  .43 39 4.0 .38 18 5.1 4.1 230 36 4.4 240 38 4.3 230 34
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow 5.7   45 54    3.2  140 37   .48 40 4.4 .46 40 3.7 900   6200 12000 48   510 650 3.5   170 44    .20  39 2.9  .47 40 4.3 .55 26 5.6 900   2200 6800 900   5300 11000 900   6000 12000
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i no-overflow 1.6   41 13    1.6  160 17   .50 41 4.4 .46 40 3.8 900   6000 12000 43   500 470 3.5   160 45    .17  35 2.0  .43 41 3.8 .58 77 6.7 900   3100 6700 900   5300 11000 900   5900 13000
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i no-overflow 5.0   42 47    2.6  50 30   .47 42 4.1 .45 40 3.7 900   6200 11000 44   500 650 3.5   160 46    .21  37 2.4  .42 40 3.8 .41 18 4.5 900   1400 9000 900   5000 11000 900   6100 11000
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i no-overflow .46  37 4.1  .74 44 7.1 .49 40 3.8 .44 40 4.3 210   880 1500 890   1400 8500 3.9   180 57    .17  31 1.6  .46 39 4.3 900    98 13000   210   2700 2200 190   2900 2500 900   4800 11000
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i no-overflow 11     49 93    6.7  98 77   .46 40 3.8 .42 40 3.7 2.4 170 21 51   500 700 3.5   160 42    .21  40 2.4  .44 40 3.8 .53 22 5.4 4.4 230 38 4.3 240 38 4.5 240 36
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow .34  42 3.1  870    800 4800   .49 40 4.4 .40 40 4.2 900   5800 11000 45   500 650 4.0   180 49    .22  37 2.0  .43 39 4.3 .41 18 5.6 900   2100 8900 900   5000 12000 900   5400 12000
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i no-overflow 1.6   41 15    1.3  51 17   .50 43 4.4 .45 40 4.1 900   6200 12000 40   44 560 3.5   160 41    .20  36 1.9  .43 40 4.0 .43 19 5.1 4.4 230 33 4.5 240 36 4.1 230 31
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow .32  37 3.0  660    12000 6800   .46 40 4.0 .45 40 4.3 900   2200 12000 890   1200 8500 3.5   150 47    .17  31 1.9  .43 40 4.1 900    940 11000   13   610 100 29   860 290 13   570 110
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i no-overflow .34  36 3.0  .74 45 6.6 .48 40 4.2 .48 41 4.1 900   1200 6900 900   1200 12000 3.9   160 50    .15  31 1.8  .43 40 3.9 900    130 12000   170   1600 2000 57   1100 550 900   6600 12000
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i unreach-call 1.7   270 12    4.2  250 39   36    1100 290   21    600 190   20   860 140 180   15000 2300 14     4700 150    14     4800 160    27    880 200   900    150 14000   7.7 480 61 8.2 490 57 7.7 480 57
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i unreach-call 2.2   250 25    370    13000 2500   24    770 200   15    660 130   29   680 260 570   450 7100 .39  120 4.6  .40  120 5.2  120    3700 1200   900    520 12000   900   3300 6700 900   4900 10000 900   5300 11000
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i unreach-call 2.0   250 21    72    1600 960   15    540 110   13    510 92   900   8300 7600 600   1000 8000 .74  210 11    .69  210 7.3  900    2600 12000   900    180 14000   900   5300 8400 900   5400 11000 900   6100 8300
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i unreach-call .87  100 6.1  70    2300 460   900    7500 9100   55    1400 430   900   5400 9700 280   450 3600 25     1600 270    8.8   660 94    200    3900 2600   900    420 13000   640   2100 5300 900   4800 10000 900   4800 7200
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i unreach-call 90     15000 770    880    6200 7200   900    9700 7600   24    760 200   30   690 260 10   350 130 33     2800 320    8.6   700 110    110    3500 1200   560    120 7000   6.2 340 53 5.8 350 44 5.4 350 41
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i unreach-call 2.4   120 18    870    3500 4300   17    550 130   13    490 110   130   1400 1400 620   1900 7500 150     15000 1300    69     15000 880    20    590 150   900    440 10000   600   1500 7800 900   4800 10000 160   1400 1300
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i unreach-call .62  55 4.6  1.5  75 15   60    1900 520   12    480 100   900   8400 7400 120   700 1300 900     6800 10000    900     5900 7600    340    4700 3700   900    120 14000   900   3500 6200 900   5000 12000 900   4900 9100
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i unreach-call 21     1400 170    2.0  88 24   910    11000 5700   910    6700 10000   290   5300 2400 820   9800 9100 2.4   800 32    2.2   780 27    940    7600 9900   900    740 10000   130   2100 1100 900   5100 9900 170   3200 1800
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i unreach-call 110     15000 1000    870    4700 6300   460    6500 4100   100    4100 890   110   1100 1100 230   15000 2400 4.5   1300 54    5.2   1300 64    410    5600 4600   900    530 9700   900   6800 8300 900   2600 9000 900   6200 12000
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i unreach-call .38  37 4.4  5.7  240 59   900    6300 12000   250    5600 2400   33   670 350 21   210 270 1.8   79 19    3.7   130 42    88    3400 950   900    94 11000   21   710 170 900   3600 10000 32   720 300
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i unreach-call .42  40 3.7  870    1000 7700   910    8300 9000   900    9700 10000   900   5300 9200 7.2 410 96 4.2   100 38    6.3   160 73    120    3800 1200   900    110 11000   900   4500 6000 900   4800 11000 900   5500 12000
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i unreach-call 1.1   79 8.6  870    3000 4300   900    7700 10000   13    500 120   18   540 130 92   1000 1100 .73  320 11    .75  320 9.6  20    730 150   900    550 14000   87   2100 670 900   5200 11000 900   5000 11000
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i unreach-call .64  48 7.8  23    3300 220   910    11000 5700   510    7200 4100   220   1900 2100 17   470 200 1.9   150 19    1.5   130 14    40    1300 310   900    140 11000   58   1900 420 900   4900 9700 78   1900 590
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i unreach-call .93  55 12    62    13000 800   910    7700 8700   57    2700 490   900   5700 9100 900   780 12000 1.7   150 17    3.9   200 50    46    1600 370   900    120 14000   800   3300 8900 900   5200 9200 610   6200 6200
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i unreach-call .45  43 4.0  47    620 520   910    11000 6400   23    870 180   320   5300 3500 31   250 380 .49  98 7.1  .44  97 4.9  33    920 280   900    130 13000   900   3700 11000 900   5200 8400 900   5500 11000
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i unreach-call .75  54 6.0  3.1  260 34   900    9600 8000   900    9400 7300   66   1100 740 460   400 5900 3.5   180 39    9.2   260 110    36    940 250   900    2400 11000   89   2700 820 900   5200 8900 280   4900 2600
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i unreach-call 34     410 270    870    4800 7700   15    510 130   6.7  280 58   100   2900 1100 620   2100 8000 4.2   380 52    3.4   360 47    19    730 140   900    160 14000   28   900 220 900   4800 14000 900   4200 12000
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i unreach-call 1.8   270 13    870    6100 8300   25    890 190   10    520 120   120   4200 1100 190   15000 2200 60     15000 580    50     7800 520    36    1100 260   900    560 9700   120   2900 1300 900   5300 9000 45   4700 390
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i unreach-call 1.3   110 9.8  870    950 3600   9.9  460 72   4.7  280 48   100   3700 1000 530   9100 6900 900     5900 12000    17     430 230    46    1700 360   .63 29 7.4 41   2000 310 900   1500 7600 92   5200 1000
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i.pp.i unreach-call 24     4500 240    870    4200 4600   10    390 79   6.4  290 61   97   2300 1000 570   250 6400 900     12000 6900    900     12000 6900    13    510 98   900    420 12000   15   560 110 900   5600 13000 21   660 160
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i unreach-call .55  55 3.9  640    2500 3900   18    590 140   5.3  290 48   900   6000 8100 85   260 1000 900     15000 7400    900     13000 12000    200    5600 1800   140    590 2000   130   5800 970 900   2200 8900 900   4800 11000
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i unreach-call 2.6   410 21    870    2600 7200   29    1200 230   11    850 110   120   1800 1300 180   12000 1900 400     15000 3400    23     6300 310    35    1500 260   900    470 11000   910   10000 11000 900   5300 8500 900   6100 9000
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i unreach-call .20  35 1.4  870    3800 2700   7.3  330 55   5.0  280 44   30   700 240 900   1400 12000 900     2100 7000    900     2100 7100    7.7  440 63   580    96 7900   12   490 96 900   4300 11000 15   610 120
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i unreach-call .46  60 4.0  870    620 4500   11    490 90   5.1  280 48   98   1600 1300 890   3600 8800 900     8100 6300    2.0   190 23    16    610 130   .94 22 14   49   3400 460 900   1800 10000 840   5300 11000
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i unreach-call .84  85 6.8  1.3  79 13   15    520 120   6.7  280 61   100   2600 1200 470   3100 5100 900     8700 8700    2.5   440 26    22    830 180   900    2300 13000   33   930 270 710   2100 8900 29   1000 240
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i.pp.i unreach-call .20  38 1.6  870    1600 4700   9.2  450 83   10    440 78   7.2 390 52 250   140 3100 900     4700 8800    .24  40 2.6  16    610 120   900    3700 11000   14   580 110 12   500 100 14   570 110
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i unreach-call 2.2   230 14    16    210 230   13    470 96   6.5  280 60   100   3700 1100 590   11000 5000 800     15000 6100    79     4200 760    23    820 170   900    330 13000   25   860 190 900   5100 11000 31   1900 230
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i unreach-call 34     820 230    870    7000 5300   20    550 160   7.7  290 79   100   3100 1100 630   5500 7000 700     15000 6000    370     13000 3800    29    950 230   900    250 12000   35   1100 270 900   5400 7900 47   4200 490
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i unreach-call 3.5   110 31    870    14000 6700   15    500 120   6.3  280 63   100   2500 1200 730   6900 8400 250     15000 2700    19     1300 210    33    1200 210   900    340 12000   33   1500 300 900   4800 12000 32   1700 270
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i unreach-call 1.7   120 12    880    4900 5100   11    500 92   5.8  290 58   100   2700 1200 900   4400 11000 900     13000 8700    18     460 250    25    790 180   900    180 12000   28   850 220 900   1800 7100 60   3700 610
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i unreach-call .29  36 2.5  870    2400 6200   8.3  440 67   73    4300 620   13   530 110 4.1 200 54 2.0   74 19    3.8   120 40    21    600 180   900    95 12000   48   1500 350 900   4000 11000 300   4900 3200
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i unreach-call 2.5   110 23    870    3800 7000   9.6  420 82   6.3  290 53   100   2800 960 4.8 15000 52 81     1700 920    28     730 280    28    1200 220   900    310 12000   20   750 160 900   4800 10000 27   1200 220
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i unreach-call 11     200 140    870    5200 5200   15    500 120   6.8  290 69   100   3700 1100 900   5500 8400 230     15000 2900    21     1600 260    27    1000 190   900    460 11000   28   880 230 900   5300 9800 37   3000 340
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i unreach-call 460     110 1800    870    1200 4200   7.2  360 65   4.9  290 46   100   4800 830 690   15000 6700 570     1800 5300    21     150 180    23    830 180   1.9  22 26   20   740 150 900   5100 7600 23   1400 190
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i unreach-call 1.3   84 11    870    2100 5800   11    490 88   5.4  290 52   910   7800 11000 510   4000 6400 .42  91 4.9  330     15000 4700    23    900 180   900    130 11000   20   730 140 900   4800 11000 23   1200 180
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i unreach-call 7.1   150 50    3.2  160 37   16    510 110   7.3  290 73   100   3700 1100 540   3300 5000 270     15000 2700    98     15000 940    35    1200 230   900    200 13000   10   290 79 9.5 290 80 10   290 85
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i unreach-call .29  39 3.5  .40 45 4.0 38    1600 320   8.4  430 66   14   510 110 900   300 9000 900     6900 9100    900     7100 9500    150    2900 1600   900    100 14000   72   2800 610 900   5000 11000 110   3700 960
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i unreach-call .64  54 5.5  870    1200 12000   13    520 100   9.4  440 83   100   2800 1000 890   1600 7000 1.0   220 14    2.6   280 34    54    2000 400   900    95 11000   49   1600 370 900   5300 9700 63   2400 490
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i unreach-call .96  48 12    60    240 630   16    640 130   600    7800 6300   900   7100 9300 55   1100 670 .35  76 3.7  .33  77 3.1  440    4900 5700   900    99 13000   680   950 7900 900   4900 9600 77   1100 770
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i unreach-call 2.9   140 28    870    14000 7300   15    510 110   7.0  290 66   100   3800 1100 520   2400 5000 50     730 570    12     420 110    20    840 140   900    470 12000   34   1100 250 900   5300 9700 47   4300 470
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i unreach-call 1.9   210 14    870    2700 5100   12    490 95   6.2  280 63   100   3600 1100 900   1900 10000 900     5900 8100    17     390 180    19    680 150   900    190 13000   34   1300 250 900   2900 7500 900   5000 12000
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.c unreach-call 100     15000 830    880    4600 7600   32    1300 220   20    810 190   64   1000 500 890   14000 10000 29     2100 300    120     15000 1400    28    1500 210   900    1600 10000   820   15000 8300 900   3300 12000 900   7300 9600
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.c unreach-call .72  53 7.7  39    13000 510   19    740 140   13    510 100   39   900 360 890   1100 6400 44     490 540    42     400 470    24    770 180   900    93 14000   900   1900 7300 510   2300 6200 900   6400 11000
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.c unreach-call .93  73 9.8  20    490 240   34    1100 290   19    710 150   35   700 330 890   2100 4800 13     350 140    900     11000 12000    900    4300 12000   13    56 150   900   4800 9300 900   5300 8200 900   4900 8300
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.c unreach-call .72  97 5.9  1.7  130 20   15    580 110   8.2  350 67   48   570 470 900   670 11000 .97  170 8.7  1.4   170 13    12    530 96   1.6  27 19   5.8 360 45 6.6 360 49 5.7 350 49
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.c unreach-call 2.0   230 17    82    14000 1000   20    880 160   23    1200 220   65   2300 710 900   1100 11000 1.4   390 14    1.5   390 18    28    1000 180   480    140 6600   900   5200 10000 900   4700 11000 900   6300 9900
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.c unreach-call 46     4700 380    870    3200 4800   27    900 200   12    470 140   900   7900 7200 890   3200 11000 .47  160 5.0  .47  160 5.3  49    1600 400   900    320 13000   900   5900 9700 900   2100 10000 900   6700 11000
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.c unreach-call .85  80 7.5  1.2  63 11   11    480 86   9.0  470 79   9.9 440 83 890   1100 7200 .17  50 1.6  .17  50 1.5  8.7  480 66   4.4  29 56   12   310 94 11   320 85 11   320 95
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.c unreach-call 1.4   120 13    5.7  240 62   25    710 190   14    520 130   38   740 360 900   2400 8300 .20  67 2.1  .19  67 2.0  330    4700 3700   900    300 11000   900   5300 13000 900   1700 8600 900   5400 11000
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.c unreach-call 1.1   100 9.4  870    980 6900   12    530 89   8.1  400 72   11   400 82 880   6000 12000 .63  140 6.3  .72  150 6.2  25    800 160   900    300 10000   200   1100 1600 900   1000 10000 26   850 190
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.c unreach-call 1.9   160 19    40    14000 450   17    570 140   9.7  460 95   24   570 180 900   1500 13000 3.0   140 33    8.6   460 110    31    860 230   900    99 12000   900   5100 7500 900   4800 9900 900   4900 7900
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.c unreach-call 380     200 3400    870    5200 6300   12    520 93   9.6  450 85   9.8 400 83 86   420 760 .93  93 7.4  1.2   110 11    26    980 230   900    99 11000   160   1100 1300 900   4900 10000 38   1200 290
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.c unreach-call 110     15000 870    880    4100 6200   28    990 220   16    500 160   31   960 240 900   2800 12000 15     1100 160    900     1800 11000    21    920 160   900    840 11000   800   3700 7900 900   3700 9000 160   5200 1700
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.c unreach-call 120     15000 980    870    4300 5900   18    590 150   8.6  380 79   900   5400 7300 60   3000 550 1.2   210 13    1.7   220 17    13    530 100   900    310 12000   900   4700 9300 900   4800 9400 900   7600 7400
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.c unreach-call .54  51 5.3  47    13000 650   8.5  480 62   7.7  350 83   7.7 350 64 4.0 130 48 .39  60 4.4  .51  66 6.0  7.0  370 59   900    100 12000   28   580 220 380   900 4600 17   550 140
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.c unreach-call 290     7900 2000    870    3300 11000   15    550 110   9.8  430 92   26   640 190 900   9200 5500 1.2   210 12    1.4   210 12    13    520 97   1.9  34 22   900   5500 8100 900   2400 11000 900   5500 10000
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.c unreach-call 100     2500 660    140    1200 1300   17    700 150   14    510 140   13   450 100 890   14000 8900 5.5   260 67    13     610 160    32    1100 230   900    310 10000   900   4000 8600 900   1800 11000 900   6900 5700
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.c unreach-call 900     1100 11000    870    4100 6300   84    3000 750   34    1300 280   930   9800 7700 900   6200 8400 900     3600 9600    900     3100 9300    940    6500 11000   900    3300 12000   900   9900 8000 900   2100 11000 900   6300 12000
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c unreach-call 1.7   180 16    6.2  380 72   35    940 280   24    920 210   40   1000 360 500   640 5700 .42  120 4.7  .43  120 4.0  960    6300 13000   .76 26 9.2 12   530 94 13   530 96 12   540 89
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.c unreach-call 1.1   170 9.4  580    2800 3300   18    670 140   19    910 160   20   810 170 500   6200 6200 .40  110 4.4  .37  110 4.5  19    930 150   1.5  29 20   11   480 87 11   490 84 11   490 90
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c unreach-call 2.4   250 24    9.0  620 110   31    1100 220   13    1400 130   35   1400 320 42   540 540 .68  180 5.9  .62  180 8.3  900    6300 13000   900    130 15000   13   600 110 12   630 97 13   610 91
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c unreach-call 120     1000 800    5.0  230 50   37    1200 310   39    1800 310   68   1500 700 12   15000 150 .71  200 8.1  .74  200 7.1  900    4700 12000   2.3  160 27   14   650 100 14   650 110 13   650 93
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c unreach-call 2.7   270 22    870    2900 5500   27    910 230   29    1700 210   55   1200 510 28   270 370 1.5   300 18    1.5   300 15    45    2300 370   900    100 12000   13   610 110 13   640 100 13   630 92
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c unreach-call 1.8   210 15    3.4  170 32   26    820 210   12    1200 120   79   930 820 27   340 390 .53  160 7.0  .57  160 5.2  26    1100 190   .77 32 9.4 12   590 100 12   590 95 13   590 96
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c unreach-call 1.4   220 13    3.6  200 34   24    760 170   10    1300 100   56   1300 570 24   320 310 1.3   250 13    1.3   250 10    21    1200 160   .65 25 7.6 12   590 120 12   590 99 12   600 94
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--misc--sgi-xp--xpc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 120     15000 980    140    2000 1600   36    1000 270   21    630 190   900   9500 8000 900   14000 9600 1.1   400 12    900     1500 10000    900    2500 11000   1.9  75 26   900   3200 11000 900   1600 11000 900   5000 15000
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--net--wireless--orinoco--orinoco_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 1.6   170 14    870    4300 6000   26    850 180   16    610 130   930   10000 8000 280   4400 2700 160     15000 1500    900     3700 11000    940    5600 14000   150    160 2300   170   1100 1300 900   4800 11000 250   1400 2000
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 7.8   740 64    10    380 120   900    9400 7700   200    6400 1600   900   6200 8800 570   13000 6100 900     3700 6500    760     15000 5500    900    4300 10000   900    290 11000   900   7000 8200 900   1800 12000 900   3800 9200
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .79  61 6.4  300    6400 2700   20    710 160   18    690 150   37   970 320 38   420 450 270     15000 2500    20     450 260    32    1100 230   900    3800 7000   900   5900 9400 900   3600 10000 900   5100 10000
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 15     1800 140    870    4300 4400   31    1000 230   16    520 150   47   1400 430 550   3700 5200 460     15000 3700    73     15000 770    31    990 220   900    190 11000   110   1200 920 900   3800 13000 62   1300 650
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--pch_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 50     7000 410    880    8500 5000   21    700 170   14    530 130   15   490 130 900   6800 6300 280     14000 2700    44     1800 490    51    1900 400   900    130 13000   90   1500 660 900   4900 10000 130   1800 1300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .27  36 3.1  48    13000 670   5.0  300 40   4.5  290 45   4.7 290 41 900   760 10000 900     2000 9100    .28  38 3.2  5.4  290 42   .37 15 4.6 12   530 88 440   1300 2900 21   2100 210
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .20  32 1.3  870    1600 7000   5.3  300 45   4.4  280 42   4.9 290 45 25   290 280 900     2000 8300    .26  34 2.8  8.5  440 65   .29 14 2.9 7.9 380 69 18   790 150 9.2 480 76
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .36  36 2.8  53    13000 710   5.7  300 42   4.6  280 43   5.5 300 44 890   1000 5700 900     1700 8900    .29  37 3.3  6.2  320 48   .33 14 3.8 13   520 97 400   1600 2900 20   1700 160
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .28  39 2.4  870    14000 5700   5.5  300 47   5.6  280 52   5.2 300 41 10   280 100 900     3100 9800    .48  48 5.7  6.3  330 59   900    98 11000   13   530 110 310   1300 3300 20   1400 160
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_netcell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .22  38 1.8  870    4400 5800   5.1  290 45   5.6  280 53   4.0 290 30 8.1 300 76 900     1500 11000    .25  40 2.3  6.0  320 49   900    3900 8100   11   470 95 220   860 2400 16   990 130
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .41  61 3.3  370    15000 2300   5.4  300 46   3.6  280 28   10   500 93 450   170 5500 900     1600 11000    .28  33 3.4  29    1500 250   .30 12 4.0 11   570 97 54   620 620 430   5100 5800
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864bfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .20  35 1.9  870    13000 13000   5.1  300 39   4.8  290 44   3.9 260 34 890   510 6700 900     2700 7200    .23  37 2.1  5.4  300 50   .32 15 3.8 9.9 440 73 180   900 2200 16   800 130
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .18  29 1.2  880    3200 3700   4.3  290 40   2.9  270 28   3.3 260 32 5.3 280 44 900     1300 12000    .18  31 1.6  4.8  280 40   .21 12 2.8 6.4 300 55 7.1 350 65 6.1 300 48
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--aten.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .21  38 2.0  870    14000 6600   6.8  310 60   3.5  270 36   98   4100 960 320   5100 3900 900     5700 8400    1.2   72 16    8.3  450 74   900    3700 8500   12   540 98 47   850 440 17   570 130
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 3.0   320 29    870    14000 4500   13    480 98   4.4  270 44   100   3900 1000 890   12000 10000 900     3600 9500    170     1000 1100    36    1300 290   900    120 14000   23   850 170 160   2200 1800 29   920 230
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--comm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .33  49 3.2  870    14000 6600   9.0  380 74   3.8  270 38   100   4400 950 890   2800 9100 900     5500 8100    3.8   140 39    12    560 100   900    160 13000   16   560 130 93   1200 1000 21   650 190
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .45  56 3.4  870    14000 5800   11    430 91   3.9  280 30   110   4300 1000 900   8200 11000 900     4100 7800    4.3   140 56    16    710 130   900    3400 8000   17   650 130 89   1600 910 22   660 220
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 1.4   150 13    870    14000 7500   11    460 94   4.0  280 40   120   4200 1000 890   14000 11000 900     6000 8700    41     410 300    28    1100 250   900    3700 7700   22   700 160 140   4500 1700 24   720 210
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .79  83 8.5  870    14000 5400   9.1  390 79   4.0  280 36   99   4200 960 900   11000 11000 900     8800 7800    17     310 150    16    670 130   900    3300 7300   16   570 120 130   1200 1400 22   670 180
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .20  34 1.6  870    14000 7300   6.0  300 55   3.4  270 36   95   3000 940 390   7800 4700 900     5200 7800    .76  55 9.7  7.3  440 65   .32 13 3.2 11   510 80 45   790 540 13   530 110
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .31  44 2.3  870    14000 6300   8.0  350 60   3.8  270 34   97   3000 1100 360   4100 4400 900     5400 7800    2.2   100 23    11    480 100   900    3500 8000   13   540 110 74   990 750 20   570 190
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--friq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .81  82 6.6  870    14000 4700   13    470 94   4.2  270 45   100   4000 1100 900   15000 9900 900     4300 7300    17     280 120    21    1200 180   900    3600 8500   23   720 170 140   1400 1400 26   830 240
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--frpw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .76  73 5.4  870    14000 8600   11    500 97   4.3  270 45   100   4000 1100 900   15000 10000 900     4800 11000    14     280 110    20    930 160   900    3500 7800   21   640 160 100   1400 1000 25   780 200
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--kbic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .69  90 7.5  870    14000 6400   11    480 97   4.2  270 45   100   4200 870 900   8800 13000 900     5100 7200    17     340 170    18    810 140   900    140 12000   19   680 160 210   1200 2300 26   900 230
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--ktti.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .21  36 2.0  870    14000 7000   6.2  310 51   3.4  270 30   97   4300 940 560   6400 6600 900     6800 8300    .78  58 8.7  8.2  460 69   .33 14 3.3 12   530 90 47   830 480 15   550 120
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .48  70 4.1  870    14000 6900   11    480 87   3.8  270 35   99   2300 1400 740   9800 8700 900     4900 7000    4.0   140 44    16    740 140   900    3200 6100   19   650 150 84   1600 800 23   690 170
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 1.5   170 13    870    14000 6100   21    650 170   5.7  280 68   110   2700 1200 900   10000 11000 900     4500 7100    68     620 460    41    2100 360   900    3800 12000   33   1100 250 130   3500 1300 35   1100 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--hw_random--virtio-rng.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .16  28 1.0  870    14000 4200   4.6  300 40   3.6  280 33   5.5 290 46 8.3 280 76 900     3800 12000    .47  33 5.1  4.9  280 43   .24 12 2.8 8.6 370 67 64   540 670 11   510 110
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .33  42 2.7  870    13000 4400   6.2  320 43   4.2  280 37   95   2300 1100 22   330 230 800     4800 8400    .47  51 5.5  7.3  340 57   900    3800 8400   22   1100 180 900   1500 7500 80   5400 1000
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ramoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .33  35 2.4  870    3600 3300   4.6  290 38   3.0  270 29   3.8 290 31 480   280 5700 900     1200 8400    .23  35 2.5  4.8  280 44   .27 13 2.6 7.0 320 61 15   450 160 10   430 96
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--uv_mmtimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call 1.9   510 26    880    12000 13000   6.3  310 54   4.6  280 41   6.4 310 53 500   3000 6200 900     13000 8100    .93  73 10    7.8  430 70   .37 15 4.6 10   500 84 30   600 310 13   510 100
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unreach-call .20  29 1.7  870    6000 4300   4.1  270 34   2.9  270 28   3.5 260 28 5.6 270 52 720     1300 8600