Tool CPAchecker 1.6.1-svn 22870
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
OS Linux 4.4.0-34-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135148 MB
Run set bmc-bitprecise.BMC.DeviceDriversLinux64 k-induction-bitprecise.k-Induction.DeviceDriversLinux64 predicateAnalysis-bitprecise.PredicateAbstraction.DeviceDriversLinux64 impact-bitprecise.Impact.DeviceDriversLinux64
Options -heap 10000M -noout -bmc -setprop solver.solver=MATHSAT5 -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.bounds.maxLoopIterationsUpperBound=0 -setprop cpa.bounds.maxLoopIterations=1 -setprop cpa.bounds.maxLoopIterationAdjusterFactory=INCREMENT -heap 10000M -noout -sv-comp16--k-induction -setprop limits.time.cpu.thread=10000s -heap 10000M -noout -predicateAnalysis-PredAbsRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -heap 10000M -noout -predicateAnalysis-ImpactRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.forcedCovering=cpa.predicate.PredicateForcedCovering
test/programs/benchmarks/ status cputime (s) walltime (s) memUsage host k BMC formula creation (s) SMT check (s) Bounds check (s) status cputime (s) walltime (s) memUsage host k BMC formula creation (s) SMT check (s) Invariant generation Bounds check (s) Induction formula creation (s) Induction check (s) status cputime (s) walltime (s) memUsage host Refinement (s) Precision adjustment (s) CPA algorithm (s) Post operator (s) Prec operator (s) Boolean abstraction (s) Abstraction (s) Solving (s) Model enumeration (s) SMT without itp (s) status cputime (s) walltime (s) memUsage host Attempted forced coverings Successful forced coverings Refinement (s) Precision adjustment (s) CPA algorithm (s) Post operator (s) Prec operator (s) Boolean abstraction (s) Abstraction (s) Solving (s) Model enumeration (s) SMT without itp (s) Forced covering (s)
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i 60.7  34.7  1204920320 1 2.50  1.73  107    54.3  2250895360 1 5.41  3.88  15.111 60.6  36.1  1216806912 6.99  4.84  6.29  .903 4.78  4.53  4.78  4.22  .283 4.51  71.6  44.4  1236635648 28 0 10.9   1.68  8.88  1.39  1.63  1.45  1.62  1.31  .133 1.66  5.19 
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i 934    817    6261026816 9 795     .017 6.40  902    452    6162137088 1 3.47  .001 0.006 1.61  1000    951    2566221824 986    937    2226429952 143 40 433     296     410     15.8   295     265     295     233     32.0   266     84.7  
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i 32.7  17.6  770629632 1 7.69  902    845    5259116544 1 21.5   1.23  0.004 427     124    105    1668608000 6.77  81.6   88.8   4.58  81.3   75.0   81.3   72.3   2.17  74.4   125    106    1676402688 74 2 12.3   70.2   85.2   4.45  70.0   65.5   70.0   65.4   .058 66.2   8.67 
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i 33.4  17.2  807284736 1 2.27  902    763    6835351552 1 14.0   .933 0.004 184     34.6  17.8  901603328 .015 1.79  1.53  .003 .00  .00  .00  .00  34.5  17.7  830902272 0 .034 1.61  1.29  .005 .003 .00  .00  .00  .00 
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i 157    130    1528774656 2 7.24  49.5   23.8   902    452    5174603776 1 7.77  4.87  0.003 28.7   914    872    2128818176 612     218     231     6.24  218     213     218     163     50.2   213     902    867    1461833728 613 54 133     66.4   717     7.09  66.0   63.6   66.0   49.2   14.3   67.7   635    
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i 29.5  15.1  666611712 1 3.52  1000    876    7091998720 191    173    2311127040 6.80  23.4   25.5   1.31  23.2   22.4   23.2   22.1   .270 22.3   193    175    2312216576 1 0 6.55  24.1   27.0   1.73  24.0   23.1   23.9   22.9   .247 23.1   .083
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i 917    840    6295363584 33 815     .002 10.9   954    478    6275264512 1 2.39  .017 344.379 .383 1000    943    4348968960 902    866    1522188288 1771 924 38.1   238     820     31.0   237     216     236     163     52.8   216     529    
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i 102    60.1  1738416128 1 31.8   .248 911    724    6298091520 1 56.1   .336 606.092 904    842    4267368448 7.69  618     820     105     600     542     596     529     12.6   542     904    855    2321518592 562 501 1.13  171     839     32.7   169     155     168     152     3.37  155     616    
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i 51.0  26.0  960679936 1 5.71  902    454    9108426752 286.584 46.6  23.8  1010552832 .071 3.04  2.29  .010 .001 .00  .00  .00  47.4  24.2  972439552 0 .067 2.83  2.18  .008 .001 .00  .00  .00  .004
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i 34.6  24.8  783122432 3 2.24  1.84  .758 919    835    4242034688 3 5.82  6.08  0.004 4.08  3.71  11.9   941    914    1942986752 220     644     648     1.75  644     640     644     18.1   619     637     623    611    14999998464
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i 933    882    6936346624 14 174     267     414     903    452    5611683840 6 19.4   12.2   0.005 21.7   311     77.5   902    863    5063659520 242     586     616     12.0   582     395     580     323     45.6   368     903    870    1653497856 6204 330 249     57.1   614     5.43  56.8   45.5   56.6   36.3   8.68  182     546    
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i 25.9  14.2  862994432 1 1.99  .228 68.9  35.4  1291759616 1 5.03  1.60  0.005 230    195    1788678144 31.9   105     127     12.8   104     88.4   104     77.3   10.7   88.0   82.0  60.6  946515968 48 17 12.1   30.7   38.5   4.85  30.4   27.2   30.4   21.4   5.59  27.4   1.01 
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i 772    759    3449262080 1 2.63  .275 1000    501    7211855872 903    851    4374192128 134     541     696     58.2   524     361     519     274     80.6   355     903    864    1576603648 3901 150 419     131     421     12.9   131     108     130     74.3   32.6   132     267    
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i 40.0  26.7  1375903744 1 3.78  .273 923    817    5563191296 1 10.6   2.72  0.010 1000    969    11744747520 1000    972    11762851840
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i 30.5  18.6  624975872 2 2.71  1.01  .101 911    831    4138872832 2 5.93  2.35  0.013 .964 14.0   11.2   903    879    2429284352 29.5   821     844     7.28  820     793     820     366     427     793     902    890    990625792 19 5 3.07  5.88  882     1.70  5.77  5.00  5.74  4.46  .497 5.08  872    
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i 77.6  58.6  1216905216 2 7.70  6.23  .865 902    453    5922521088 1 7.24  3.43  0.006 13.2   154     264     948    911    2556301312 308     528     549     8.03  527     495     526     250     244     494     908    882    1411571712 264 91 66.2   59.3   803     4.43  58.9   54.9   58.8   35.9   18.8   57.6   734    
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i 47.0  25.0  868589568 1 8.70  904    863    2184445952 1 21.5   .00  0.003 814     911    762    6401490944 24.5   743     591     6.82  .711 .00  .00  .00  913    784    5955477504 0 26.5   764     544     5.99  .496 .00  .00  .00  4.00 
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i 917    799    7039877120 4 701     .00  63.7   902    452    4880236544 1 8.20  .001 0.003 21.9   91.6  52.3  1641988096 .554 11.9   28.6   11.7   11.4   9.44  11.1   9.14  .269 9.41  125    83.8  1628581888 0 .654 41.2   60.8   14.3   40.7   35.7   40.5   34.4   1.24  35.6   .080
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i 913    779    5197684736 6 679     .002 88.8   903    452    4825284608 1 4.89  .00  365.637 4.21  1000    796    10847252480 92.4   735     195     17.8   1.40  .00  .00  .00  911    832    5830074368 0 28.7   819     527     6.81  .245 .00  .00  .00  3.22 
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i 22.7  11.8  581898240 2 2.75  .00  .102 902    803    5358993408 2 6.23  .00  0.006 6.31  723     52.5   20.0  10.4  581902336 .117 1.70  .900 .037 .001 .00  .00  .00  20.5  10.6  566992896 0 .126 2.08  1.32  .040 .00  .00  .00  .00  .013
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i 23.6  12.3  521248768 1 4.16  902    806    5059964928 1 15.1   .00  0.004 13.8   18.8  9.70 513695744 .081 1.26  .867 .008 .001 .00  .00  .00  20.0  10.4  528957440 0 .575 1.70  .777 .009 .00  .00  .00  .00  .003
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i 907    847    4977680384 3 110     .00  698     447    225    4240166912 1 14.7   .00  0.004 172     201    149    1913552896 .983 98.5   116     11.2   98.0   95.2   97.8   94.7   .420 95.1   194    149    1834131456 0 .987 103     116     7.44  103     99.1   103     98.1   .687 98.8   .090
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i 11.4  6.21 387313664 1 1.11  902    780    7471841280 1 7.79  .001 0.007 6.97  9.96 5.48 393056256 .019 .678 .441 .003 .001 .00  .00  .00  9.56 5.28 357531648 0 .032 1.00  .840 .003 .001 .00  .00  .00  .001
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i 904    863    3937955840 9 135     .00  716     104    52.8  1593077760 1 10.5   .00  0.004 28.2   125    105    871501824 .807 89.3   94.4   3.12  89.1   88.0   89.0   86.8   1.21  88.0   139    116    846536704 0 .691 98.2   106     4.63  98.0   96.8   98.0   94.6   2.15  96.8   .057
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i 924    801    7938768896 3 710     .00  64.6   909    455    5618364416 1 11.3   .00  328.417 9.43  118    78.9  1902948352 .119 21.5   63.8   22.1   19.6   12.5   18.9   11.7   .467 12.2   209    171    1881604096 0 .067 118     156     20.2   115     88.4   115     83.5   3.83  87.3   .285
ldv-linux-3.0/module_get_put-drivers-net-pppox.ko_true-unreach-call.cil.out.i.pp.i 906    892    3480756224 44 2.84  692     175     909    455    5833183232 31 5.23  224     0.005 93.0   4.38  111     10.5  5.74 418009088 .051 .102 1.23  .830 .078 .050 .077 .034 .006 .040 10.8  5.78 381620224 0 .050 .122 1.19  .844 .082 .049 .079 .038 .006 .044 .002
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i 920    786    7895232512 3 712     .00  53.5   902    452    6366011392 1 12.2   .00  362.611 6.90  97.8  59.9  1560399872 1.20  20.8   49.4   14.6   19.0   14.0   18.3   13.4   .434 13.8   113    74.4  1506512896 0 1.30  31.0   64.2   18.5   29.1   21.2   28.4   19.9   .686 20.6   .392
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i 921    811    7297720320 2 665     .00  123     903    452    5994160128 1 105     .00  0.006 235     905    793    6945755136 13.1   307     767     307     266     220     257     203     17.5   221     907    829    5324267520 0 17.6   814     702     3.99  .322 .00  .00  .00  15.8  
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i 908    865    5893922816 2 147     .00  702     902    452    5185064960 1 12.7   .001 363.855 51.2   931    791    8416428032 102     756     179     13.7   1.13  .00  .00  .00  914    841    5954449408 0 24.3   820     543     6.03  .303 .00  .00  .00  3.03 
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i 79.4  55.0  1772494848 2 20.2   .00  25.9   902    452    6314860544 1 25.1   .00  366.732 38.1   23.7  12.3  588410880 .391 4.74  2.44  .097 .020 .00  .00  .00  25.5  13.2  598749184 0 .995 5.55  2.40  .215 .069 .00  .00  .00  .046
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i 905    889    3005980672 19 5.53  767     97.2   912    457    5561020416 14 8.93  281     0.006 73.9   10.8   65.2   18.2  11.5  497000448 .808 4.50  6.36  .784 4.39  3.71  4.37  2.97  .704 3.67  402    393    14999998464
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i 924    781    9571565568 5 600     .00  157     902    452    6268399616 1 6.02  .00  0.009 7.24  913    748    9887698944 149     731     157     26.1   2.65  .00  .00  .00  921    769    8387440640 0 58.1   747     462     11.0   .493 .00  .00  .00  5.79 
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i 907    855    6708146176 4 394     .001 445     902    452    5455011840 1 17.5   .00  373.521 30.4   694    629    5447958528 4.38  389     609     72.2   357     313     350     301     11.1   312     903    789    5008941056 0 4.82  164     775     498     153     137     150     131     5.37  136     1.65 
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i 911    858    6170062848 13 153     .001 683     251    127    4522676224 3 5.08  .00  0.006 8.01  88.3   2.59  39.0  20.9  840687616 .609 5.41  14.8   5.65  4.66  2.90  4.26  2.65  .077 2.73  41.0  21.9  832630784 0 .511 5.85  16.2   5.43  5.23  3.23  4.99  2.87  .093 2.96  .238
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i 15.8  8.28 464551936 1 1.87  903    862    2933530624 1 14.3   .00  0.011 805     14.8  7.91 470945792 .104 1.40  .947 .009 .001 .00  .00  .00  13.8  7.30 443355136 0 .067 1.37  1.01  .016 .001 .00  .00  .00  .00 
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i 911    847    6015315968 2 333     .00  495     904    453    4961816576 1 70.4   .001 0.009 357     308    261    2579210240 1.72  192     245     30.1   189     168     188     163     4.67  168     338    291    3176140800 0 1.50  202     276     44.4   199     174     198     168     5.48  174     .612
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i 816    463    11893612544 932    473    12117499904 7 10.8   9.32  258.213 19.3   320     105     13.5  7.36 463056896 .130 .675 2.57  1.31  .587 .429 .552 .385 .033 .418 12.9  7.04 421511168 0 .151 .548 2.22  .734 .423 .302 .408 .261 .029 .290 .012
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i 934    808    7867584512 3 642     .609 146     219    110    4111577088 1 19.1   .00  0.005 20.0   347    300    2305671168 86.9   128     177     22.3   123     103     122     83.7   18.3   102     124    91.3  1358303232 191 175 8.60  37.3   70.9   8.07  36.5   32.6   36.4   31.1   1.21  32.4   20.8  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i 15.3  8.13 438669312 1 1.81  902    694    7393546240 1 56.6   4.03  0.004 35.7   77.6  49.5  1684226048 3.35  42.1   23.3   1.10  .228 .00  .00  .00  82.4  55.5  1682038784 0 3.39  49.4   31.5   .758 .178 .00  .00  .00  .607
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i 926    803    7977570304 2 716     .001 61.8   902    452    6519160832 1 44.4   .00  0.007 141     909    812    6471503872 10.9   479     785     124     447     368     437     356     10.4   367     904    793    7360458752 0 11.0   281     769     248     253     193     246     183     8.79  192     74.3  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i 22.9  11.8  518803456 1 3.27  37.7  19.5  763846656 1 4.42  0.005 17.4  9.01 527675392 .108 1.59  .922 .009 .001 .00  .00  .00  17.4  9.11 484573184 0 .136 1.65  .953 .031 .001 .00  .00  .00  .005
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 55.7  28.6  1220767744 1 3.81  903    453    7794565120 314.095 52.5  27.0  1241448448 .089 1.59  1.04  .046 .037 .00  .00  .00  50.4  25.8  1203310592 0 .057 1.61  1.01  .007 .001 .00  .00  .00  .004
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 374    348    14999998464 904    454    6945583104 4 20.6   11.4   398.365 73.7   114     219     129    115    14999998464 163    147    14999998464
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 32.8  17.1  658612224 1 7.84  440    220    14999998464 182    162    14999998464 181    163    14999998464
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 38.2  19.6  871378944 1 3.98  124    70.2  1641365504 1 26.6   11.6   0.004 32.6  17.5  922550272 2.09  .018 .836 .526 .006 .001 .00  .00  .00  31.7  17.1  881958912 0 2.21  .035 .771 .523 .002 .00  .00  .00  .00  .003
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 98.3  67.8  2611486720 1 3.88  2.89  223    113    3727749120 1 9.56  10.8   51.456 50.9  28.3  1128402944 3.37  2.69  4.70  1.44  2.58  2.35  2.57  2.34  .007 2.35  57.5  31.8  1122877440 0 4.86  2.81  5.30  1.82  2.77  2.45  2.76  2.43  .011 2.44  .007
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 54.7  29.4  1357213696 1 12.7   952    478    5509685248 1 249     367.458 69.3  41.3  1453137920 .307 25.6   16.7   .085 .002 .00  .00  .00  63.4  37.9  1380577280 0 .191 22.5   14.5   .049 .001 .00  .00  .00  .019
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 28.0  15.1  637960192 1 3.99  .056 70.7  35.8  1043070976 1 14.7   .474 6.364 17.7  9.41 611364864 .438 .031 1.05  .626 .002 .00  .00  .00  .00  17.4  9.36 590012416 0 .581 .039 .941 .462 .005 .001 .00  .00  .00  .002
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 222    190    14999998464 934    470    6079315968 2 31.6   10.3   379.359 18.3   285     88.7   234    219    14999998464 240    220    14999998464
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 34.3  18.7  934100992 1 2.23  .056 83.7  42.3  1517883392 1 5.67  .154 0.009 30.7  16.9  928198656 .953 .121 .708 .350 .096 .051 .094 .041 .00  .041 29.3  16.2  900845568 0 1.11  .088 .573 .319 .069 .032 .067 .026 .001 .027 .00 
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 231    214    6343303168 1 3.72  .481 659    330    10311720960 1 10.9   2.76  278.879 44.0  30.3  1574096896 2.06  1.48  3.36  1.03  1.35  1.12  1.34  1.08  .031 1.11  46.9  31.8  1588031488 0 2.54  1.50  3.54  1.30  1.40  1.16  1.39  1.11  .046 1.15  .004
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 23.6  12.2  659570688 1 2.52  89.5  48.5  1423253504 1 13.2   .129 0.005 18.4  9.62 661590016 .024 .698 .462 .003 .00  .00  .00  .00  18.1  9.52 611475456 0 .040 .753 .478 .004 .001 .00  .00  .00  .002
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 57.5  29.5  1186639872 1 4.53  998    501    8033050624 338.310 80.9  54.6  1458794496 23.5   2.38  3.48  .734 2.36  2.23  2.35  2.21  .016 2.22  84.0  57.5  1434779648 0 25.9   2.66  4.03  .964 2.65  2.52  2.64  2.50  .015 2.51  .002
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 39.9  20.6  835264512 1 3.87  1000    861    6685556736 1 9.41  518     0.004 913    891    882466816 913    893    859066368
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 19.3  10.4  579915776 1 1.47  .052 47.4  24.2  927203328 1 3.87  .320 3.580 16.0  8.74 598683648 .870 .021 .578 .386 .002 .00  .00  .00  .00  16.3  8.97 575467520 0 .809 .025 1.07  .415 .004 .001 .00  .00  .00  .00 
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 53.5  27.7  1094832128 1 12.6   419    313    7843180544 1 16.2   45.8   0.004 33.0  17.4  943050752 1.49  .041 1.28  .781 .003 .001 .00  .00  .00  32.5  17.1  894406656 0 1.89  .044 1.15  .699 .006 .00  .00  .00  .00  .00 
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 167    139    14999998464 418    210    4456914944 1 20.5   3.28  147.640 137    120    14999998464 132    117    14999998464
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 110    71.6  3008258048 1 49.5   906    455    5099962368 1 371     380.887 903    871    1988755456 .610 846     854     4.62  845     836     845     834     3.23  837     903    873    1662894080 0 3.63  847     854     3.41  847     839     847     837     2.92  840     .064
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 41.3  21.5  856100864 1 5.62  902    454    10076798976 270.404 56.9  37.6  1716101120 .947 18.4   22.9   2.37  18.2   16.9   18.2   16.4   .445 16.9   61.0  39.3  1708564480 0 .964 17.0   23.4   2.88  16.9   15.6   16.9   15.2   .408 15.6   .011
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 30.9  15.9  666664960 1 5.71  904    700    7799005184 1 24.1   .00  0.004 73.2   26.0  13.4  694738944 .181 .224 1.50  .725 .154 .095 .144 .086 .004 .090 22.6  11.7  640987136 0 .165 .241 1.80  1.12  .162 .101 .155 .090 .008 .098 .006
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 913    837    7515643904 2 277     .00  528     907    456    6014976000 1 387     335.037 904    861    4840226816 .937 731     844     67.5   728     633     727     619     13.9   633     903    867    3165032448 0 .690 794     851     35.9   793     703     793     685     17.8   703     .263
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 914    856    8341127168 3 362     .00  477     941    472    6646403072 1 28.8   .00  360.882 94.4   471    434    1736708096 237     150     166     8.92  149     138     149     135     3.35  138     388    357    1596686336 90 0 137     179     198     7.69  178     164     178     160     3.99  164     5.75 
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 29.0  14.9  796651520 1 2.96  1000    853    6210318336 27.0  14.0  784982016 .150 1.56  .931 .028 .002 .00  .00  .00  24.8  12.8  768053248 0 .103 1.44  .757 .009 .003 .00  .00  .00  .020
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 926    774    9453572096 2 724     .001 26.7   974    760    8299024384 1 21.9   .00  0.004 58.8   23.8  12.3  756084736 .143 1.60  .999 .007 .001 .00  .00  .00  24.8  12.8  731148288 0 .097 1.66  .878 .012 .002 .00  .00  .00  .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--apei--einj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    873    3381170176 41 31.3   .007 829     28.3  14.6  614182912 1 5.76  .001 0.008 .578 13.3  7.53 478973952 .295 .912 1.99  .665 .814 .662 .802 .647 .011 .658 14.0  7.89 466391040 0 .285 .967 2.73  1.27  .910 .748 .898 .732 .011 .743 .016
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--bgrt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    894    6000504832 61 2.57  .003 885     12.8  6.87 426356736 1 .817 0.010 10.6  5.95 390045696 .104 .308 1.36  .733 .235 .168 .230 .160 .004 .164 9.99 5.59 361062400 0 .098 .254 1.39  .446 .221 .164 .219 .157 .004 .161 .003
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 905    888    3629273088 60 3.98  .002 876     13.6  7.20 443142144 1 1.06  0.004 10.4  5.66 387780608 .049 .133 .777 .390 .105 .069 .100 .062 .002 .064 10.1  5.51 376623104 0 .044 .134 1.29  .390 .108 .063 .094 .059 .002 .061 .003
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 906    880    4141322240 8 57.3   .002 815     18.3  9.54 448405504 1 2.53  .00  0.005 1.07  10.2  5.64 384352256 .095 .852 1.59  .449 .322 .240 .313 .225 .008 .233 10.7  5.84 359403520 0 .094 .422 1.71  .909 .368 .252 .360 .241 .005 .246 .004
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 905    889    4160356352 25 5.07  .003 878     21.6  11.3  506511360 1 3.83  .001 0.005 .506 10.7  5.91 433119232 .070 .489 1.75  .468 .421 .325 .414 .309 .010 .319 11.5  6.36 413065216 0 .074 .509 1.95  1.01  .433 .334 .426 .320 .010 .330 .003
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 906    882    4416319488 32 21.0   .002 852     31.8  16.3  660992000 1 4.51  .00  0.006 2.94  12.6  6.78 459436032 .060 .386 1.81  .985 .332 .250 .324 .231 .010 .241 11.9  6.46 435032064 0 .060 .428 1.63  .906 .383 .266 .372 .247 .009 .256 .006
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 905    890    3994329088 51 5.58  .003 877     13.8  7.26 460353536 1 .744 0.016 11.2  6.03 433983488 .048 .144 1.34  .496 .130 .087 .122 .075 .002 .077 11.1  6.02 405245952 0 .041 .155 1.29  .888 .127 .080 .125 .075 .003 .078 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--atm--adummy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    882    4282650624 45 16.5   .003 854     27.8  14.2  584499200 1 3.73  .00  0.006 2.10  13.5  7.23 471191552 .104 .242 1.74  .568 .198 .140 .192 .134 .004 .138 13.3  7.12 429858816 0 .100 .289 1.67  .967 .250 .152 .233 .145 .004 .149 .004
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 913    886    11151650816 40.3  20.7  963756032 1 4.08  .008 0.005 2.21  6.16  .976 10.5  5.82 371822592 .109 .570 1.65  .712 .483 .364 .477 .356 .002 .358 10.5  5.80 344731648 0 .073 .518 1.81  .870 .446 .324 .422 .315 .002 .317 .024
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 907    892    6100185088 52 3.57  .002 883     13.0  6.94 424415232 1 .973 0.011 10.6  5.82 407650304 .049 .638 1.49  .522 .151 .102 .144 .090 .004 .094 10.2  5.59 374153216 0 .047 .192 1.33  .889 .153 .111 .150 .103 .003 .106 .003
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 904    888    3394867200 1009 10.1   .059 839     9.86 5.34 335626240 1 .134 0.006 8.38 4.66 351150080 .067 .201 .827 .510 .176 .124 .174 .117 .001 .118 8.34 4.64 316059648 0 .080 .196 .914 .191 .155 .104 .146 .098 .002 .100 .00 
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 911    880    5954936832 4 102     .00  767     92.8  47.1  1682685952 1 6.37  .001 0.011 16.6   12.1  6.74 484794368 .077 .840 2.11  .822 .783 .649 .768 .597 .032 .629 12.4  6.97 455593984 0 .060 .936 2.24  .864 .829 .695 .819 .655 .033 .688 .005
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 915    864    9957609472 2 152     .00  691     903    452    7293669376 1 29.0   .00  0.013 186     221    198    2554105856 .072 176     187     6.02  175     170     175     165     5.44  170     231    206    2521997312 0 .068 185     196     5.88  184     178     184     173     5.82  178     .049
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 914    862    7295098880 3 205     .00  642     267    135    4508438528 1 11.0   .001 0.006 15.7   18.3  10.4  674275328 .056 2.68  4.16  .762 2.56  2.29  2.54  2.17  .086 2.25  19.2  10.8  646332416 0 .079 2.61  4.75  1.38  2.47  2.19  2.44  2.10  .082 2.18  .009
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 916    831    8168652800 3 278     .00  533     133    67.3  2166214656 1 12.0   .00  0.005 23.2   27.6  18.3  1281769472 .056 9.38  11.1   .880 9.26  8.75  9.24  7.64  1.09  8.72  26.8  17.8  1239453696 0 .078 9.02  11.1   1.28  8.91  8.48  8.90  7.39  1.07  8.46  .016
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 925    819    9639821312 3 608     .001 186     944    473    7145517056 1 19.2   .00  362.278 32.8   114    95.9  1882116096 .068 79.3   87.3   4.18  78.9   76.9   78.8   73.3   3.55  76.9   116    97.3  1842020352 0 .069 80.5   88.6   4.36  80.2   78.1   80.0   74.5   3.62  78.1   .122
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 1000    797    8946831360 902    452    6512283648 1 12.7   .001 337.223 10.1   34.6  21.2  717135872 .080 10.5   14.5   2.09  10.4   9.50  10.3   9.04  .415 9.46  35.9  21.9  678895616 0 .086 11.6   15.8   2.39  11.3   10.4   11.3   9.93  .445 10.4   .031
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 914    882    8647639040 6 91.8   .00  778     44.6  23.0  988291072 1 5.54  .00  0.005 8.48  11.9  6.65 434352128 .047 .632 1.94  .937 .579 .463 .569 .415 .033 .448 11.2  6.27 407023616 0 .051 .650 1.85  .853 .575 .468 .567 .422 .033 .455 .005
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 1000    824    8954314752 52.7  26.9  1088237568 1 8.17  .077 0.007 9.15  15.2  8.63 610172928 .061 1.71  3.54  1.12  1.62  1.44  1.61  1.34  .088 1.43  15.7  8.89 586194944 0 .068 1.77  3.58  1.11  1.67  1.48  1.65  1.38  .091 1.47  .005
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 924    814    8560635904 3 599     .001 192     370    186    6583402496 1 11.6   .001 0.005 41.1   35.6  20.0  994045952 .106 5.87  10.1   1.90  5.68  5.04  5.62  4.69  .322 5.01  39.5  21.6  976330752 0 .076 6.21  11.7   2.77  5.98  5.28  5.89  4.92  .302 5.22  .022
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 928    805    8672448512 3 685     .00  95.5   293    148    5143429120 1 13.1   .00  0.007 27.1   35.3  19.5  989052928 .082 6.44  10.3   1.88  6.28  5.53  6.25  5.12  .325 5.44  34.9  19.0  940093440 0 .085 5.97  10.1   2.31  5.79  5.09  5.75  4.74  .310 5.05  .033
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 926    751    8225001472 3 667     .00  60.0   902    452    6702620672 1 14.0   .001 344.806 24.3   30.5  17.1  953475072 .091 4.25  8.18  1.92  4.11  3.58  4.04  3.28  .265 3.55  33.4  18.2  923078656 0 .096 5.42  10.0   2.31  5.25  4.62  5.21  4.31  .280 4.59  .012
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 910    878    7185367040 7 110     .00  757     68.7  35.0  1282117632 1 5.16  .00  0.008 11.2   12.1  6.75 450871296 .063 .659 1.96  .510 .601 .507 .593 .457 .034 .491 11.7  6.51 426156032 0 .064 1.07  1.93  .459 .599 .482 .586 .443 .032 .475 .003
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 909    879    6261714944 4 62.4   .00  804     65.5  33.4  1162362880 1 11.2   .001 0.005 6.44  29.1  16.9  893464576 .064 5.43  8.00  1.20  5.30  5.00  5.28  4.81  .178 4.99  24.7  14.7  845164544 0 .073 4.98  7.61  1.54  4.85  4.52  4.82  4.33  .177 4.51  .014
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 911    875    10185060352 2 99.6   .00  754     255    129    4320083968 1 17.5   .00  0.004 69.3   80.8  59.4  2349658112 .089 38.5   46.8   2.46  38.3   37.0   38.2   33.1   3.86  36.9   81.3  60.1  2320007168 0 .094 39.7   47.9   2.32  39.1   37.8   39.0   33.8   3.97  37.8   .028
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 9.38 5.12 330072064 1 .581 904    882    3792863232 14 7.89  .001 0.012 261     9.19  596     8.19 4.50 339636224 .026 .746 .603 .005 .001 .00  .00  .00  8.39 4.63 318431232 0 .018 .774 .262 .002 .001 .00  .00  .00  .00 
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 906    883    4399677440 9 34.2   .00  842     107    54.2  1891667968 2 5.65  .00  0.008 18.9   18.7   3.67  13.1  7.38 450539520 .119 1.14  2.12  .610 1.07  .923 1.07  .891 .024 .915 14.2  7.94 436772864 0 .083 1.28  2.75  1.02  1.18  1.02  1.16  .993 .027 1.02  .006
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 905    890    5381230592 843 8.70  .057 851     10.9  5.79 380751872 1 .691 0.006 9.44 5.32 374472704 .124 .357 1.06  .226 .310 .239 .305 .229 .005 .234 9.57 5.35 351916032 0 .128 .342 1.30  .773 .309 .236 .305 .227 .005 .232 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--tpm--tpm_nsc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 969    864    7405260800 4 435     .001 413     74.8  38.1  1299079168 1 10.7   .00  0.008 16.0   19.6  11.0  521388032 .252 2.55  5.35  1.69  2.42  1.93  2.40  1.81  .076 1.88  16.7  9.53 477175808 0 .224 2.08  4.53  1.55  1.94  1.57  1.91  1.48  .049 1.53  .008
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 904    887    2325368832 13 6.73  .001 873     24.5  12.7  572039168 1 4.57  0.011 12.9  7.41 490332160 .228 .918 2.55  .671 .861 .707 .846 .681 .022 .703 13.5  7.79 461377536 0 .245 .947 2.67  1.10  .884 .724 .864 .698 .022 .720 .002
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 903    889    1991991296 48 4.52  .002 879     13.9  7.42 414097408 1 1.20  .001 0.012 1.28  9.57 5.58 396095488 .266 .402 1.35  .683 .364 .260 .354 .252 .002 .254 9.01 5.17 370380800 0 .224 .403 1.48  .794 .365 .265 .350 .258 .002 .260 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--cpufreq_powersave.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    898    6700437504 100 3.55  .008 888     8.75 4.74 324587520 1 .314 0.006 7.60 4.22 326897664 .038 .101 .755 .140 .070 .039 .068 .033 .00  .033 7.57 4.23 299606016 0 .510 .098 .373 .160 .072 .036 .068 .031 .00  .031 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    878    3543576576 9 36.5   .00  832     33.2  17.0  765415424 1 4.98  .001 0.003 2.42  15.8  8.70 548315136 .089 1.12  2.59  .925 1.05  .894 1.04  .865 .024 .889 16.9  9.26 524058624 0 .108 1.16  3.51  1.11  1.07  .875 1.05  .838 .028 .866 .006
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 911    877    8581472256 777 111     .029 397     11.3  6.02 366665728 1 .999 .001 0.005 .085 8.58 4.77 348913664 .062 .179 .894 .566 .150 .053 .144 .044 .001 .045 9.03 4.95 321785856 0 .055 .158 1.02  .668 .136 .058 .131 .050 .001 .051 .016
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--firmware--google--gsmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    878    4741976064 7 47.8   .00  819     853    428    6813646848 4 30.2   .001 0.004 157     164     62.9   26.5  15.2  696250368 .470 4.91  7.76  1.51  4.70  4.18  4.63  4.10  .051 4.15  28.5  16.5  663740416 0 .497 4.63  8.70  2.38  4.47  3.99  4.42  3.92  .057 3.98  .010
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--firmware--google--memconsole.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    875    5561245696 96 64.2   .006 775     14.0  7.42 380997632 1 1.89  .00  0.005 .322 9.05 5.08 357896192 .128 .275 1.27  .269 .229 .157 .223 .141 .006 .147 9.48 5.26 340045824 0 .116 .320 1.36  .788 .284 .205 .272 .195 .003 .198 .011
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    4053901312 24 4.94  .003 877     17.1  9.01 450887680 1 2.79  0.005 11.0  6.15 437571584 .078 .394 1.67  .871 .339 .254 .335 .234 .011 .245 11.1  6.17 406863872 0 .046 .414 1.92  1.04  .348 .250 .336 .235 .012 .247 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    894    3289042944 45 2.87  .022 885     11.0  5.88 381407232 1 .496 0.005 9.38 5.18 364077056 .090 .168 1.05  .660 .121 .076 .117 .065 .002 .067 9.73 5.32 343732224 0 .088 .177 1.25  .361 .131 .081 .124 .074 .002 .076 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    888    3149819904 18 4.44  .002 878     18.0  9.43 439480320 1 3.51  0.012 10.6  5.95 440348672 .089 .601 1.79  .847 .548 .384 .539 .359 .013 .372 10.9  6.09 406609920 0 .068 .594 1.94  .925 .503 .380 .495 .365 .013 .378 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-tps65912.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    890    4060315648 30 4.66  .005 879     12.5  6.66 385327104 1 1.42  0.013 8.99 5.03 376684544 .048 .234 1.16  .691 .213 .155 .209 .140 .005 .145 9.37 5.16 349728768 0 .054 .298 1.29  .338 .256 .180 .242 .170 .005 .175 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    881    3654246400 10 38.5   .00  836     27.1  14.0  571842560 1 5.02  .00  0.007 2.72  11.2  6.33 430284800 .051 .721 2.14  .984 .670 .551 .657 .501 .014 .515 10.8  6.07 398204928 0 .067 .678 1.98  .489 .619 .488 .608 .463 .018 .481 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--drm_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    894    9330782208 422 6.29  .021 870     13.7  7.18 434040832 1 .321 0.019 10.9  5.85 431263744 .053 .415 1.08  .383 .042 .021 .041 .017 .001 .018 10.9  5.81 397627392 0 .063 .078 .992 .686 .042 .021 .039 .019 .001 .020 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    884    3162148864 7 19.4   .001 857     68.3  34.9  1274982400 1 12.4   .00  0.009 11.7   20.1  12.1  697987072 .047 4.03  6.16  1.33  3.96  3.55  3.95  3.48  .059 3.53  20.3  12.1  675651584 0 .048 3.78  6.56  1.80  3.71  3.40  3.70  3.33  .059 3.39  .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    897    9459945472 10.9  5.89 386961408 1 0.010 10.2  5.66 389652480 .043 .075 1.03  .310 .038 .018 .036 .010 .00  .010 9.42 5.19 364638208 0 .039 .063 .954 .393 .041 .019 .039 .010 .00  .010 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--stub--poulsbo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 909    894    6485782528 392 6.92  .030 869     10.9  5.87 385282048 1 .219 0.006 9.70 5.29 365420544 .040 .090 1.07  .791 .062 .031 .058 .019 .001 .020 9.33 5.11 344076288 0 .036 .082 .946 .361 .046 .021 .044 .015 .001 .016 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-cherry.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    3892117504 38 5.26  .006 877     13.0  6.90 383082496 1 1.26  0.006 10.4  5.73 394596352 .076 .340 1.65  .976 .266 .161 .257 .150 .005 .155 10.4  5.67 368283648 0 .076 .285 1.69  .626 .231 .164 .222 .158 .005 .163 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-chicony.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    888    6350675968 58 17.5   .003 859     19.7  10.3  446877696 1 3.40  0.007 12.2  6.62 408358912 .054 .382 2.42  .821 .209 .135 .197 .126 .004 .130 12.6  6.86 384045056 0 .083 .325 2.77  1.25  .234 .138 .220 .127 .005 .132 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    901    10484838400 98 3.03  .004 891     9.48 5.09 359780352 1 .205 0.004 8.42 4.67 355717120 .068 .075 .823 .506 .056 .031 .053 .026 .001 .027 9.20 5.06 325648384 0 .044 .106 1.05  .766 .072 .033 .068 .029 .001 .030 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    890    4458479616 38 5.08  .001 878     12.5  6.66 391241728 1 1.12  0.006 10.2  5.60 377446400 .087 .288 1.36  .488 .244 .167 .236 .156 .006 .162 10.1  5.60 358699008 0 .095 .265 1.59  .484 .232 .157 .209 .144 .006 .150 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    885    4263145472 40 11.5   .001 866     17.7  9.22 442294272 1 2.11  0.011 11.7  6.41 412340224 .058 .432 2.18  .737 .339 .188 .301 .164 .005 .169 12.3  6.66 400801792 0 .069 .313 2.63  1.50  .189 .126 .180 .118 .005 .123 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 911    894    7923408896 63 4.30  .003 883     10.5  5.64 376680448 1 .438 0.009 9.96 5.47 370896896 .042 .187 1.33  .875 .138 .095 .134 .088 .004 .092 9.69 5.27 344457216 0 .045 .672 1.34  .414 .162 .120 .158 .113 .003 .116 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-keytouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 860    842    14999998464 11.0  5.94 370642944 1 .633 0.005 9.11 5.06 365432832 .065 .056 .995 .754 .039 .015 .034 .012 .00  .012 8.43 4.69 317022208 0 .038 .066 .796 .560 .045 .016 .037 .012 .00  .012 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-lcpower.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    887    6377242624 65 11.1   .006 866     14.1  7.48 414568448 1 1.03  0.006 11.0  6.05 393011200 .061 .263 1.74  .986 .200 .115 .180 .103 .004 .107 10.6  5.81 370135040 0 .080 .288 1.79  .678 .184 .108 .149 .100 .004 .104 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-monterey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    3859939328 40 6.06  .007 875     13.1  6.96 371245056 1 1.44  0.007 9.98 5.53 385544192 .047 .260 1.56  .887 .181 .118 .174 .108 .005 .113 10.5  5.75 372051968 0 .081 .212 1.65  .607 .165 .114 .161 .106 .004 .110 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ortek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    900    13729939456 10.4  5.59 361299968 1 .576 0.006 9.14 5.06 360828928 .038 .120 .973 .624 .088 .051 .081 .046 .002 .048 9.07 4.98 346296320 0 .050 .520 1.05  .303 .477 .044 .473 .038 .001 .039 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-petalynx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    887    4998836224 26 7.62  .003 873     17.8  9.33 461852672 1 2.70  0.006 11.2  6.24 422973440 .053 .509 2.08  .643 .410 .335 .399 .286 .014 .300 11.5  6.36 400953344 0 .051 .525 2.28  1.18  .426 .298 .418 .282 .011 .293 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-primax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 9.79 5.31 338558976 1 .688 904    836    6745485312 7 13.9   .001 0.007 62.8   326     424     8.43 4.63 353562624 .019 .752 .624 .005 .001 .00  .00  .00  8.86 4.82 323022848 0 .026 .779 .645 .001 .00  .00  .00  .00  .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-saitek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    901    14795141120 10.8  5.75 373866496 1 .715 0.015 8.84 4.82 362135552 .088 .170 1.09  .739 .142 .075 .113 .066 .002 .068 9.03 4.92 334217216 0 .042 .180 1.11  .755 .124 .081 .120 .068 .003 .071 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-samsung.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    886    4941258752 18 9.45  .003 870     23.4  12.1  531898368 1 3.52  0.007 13.9  7.82 521781248 .092 1.02  3.07  .878 .839 .695 .827 .647 .033 .680 14.5  8.08 505663488 0 .066 1.07  3.50  1.51  .965 .822 .953 .784 .035 .819 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-speedlink.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    3749662720 161 4.40  .008 875     10.9  5.81 380239872 1 .367 0.005 10.0  5.47 372273152 .038 .079 1.16  .400 .047 .023 .046 .015 .002 .017 9.66 5.27 334716928 0 .042 .082 1.06  .738 .057 .024 .051 .018 .002 .020 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-sunplus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    889    4079190016 38 4.50  .001 878     11.3  6.02 375074816 1 .621 0.018 10.0  5.51 384786432 .043 .220 1.48  .945 .183 .127 .176 .119 .004 .123 10.2  5.54 364359680 0 .049 .246 1.51  .468 .197 .146 .191 .137 .005 .142 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-tivo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    885    6325944320 57 11.4   .002 865     13.9  7.30 378548224 1 1.06  0.006 10.6  5.84 387338240 .048 .256 1.80  1.04  .177 .109 .167 .101 .004 .105 10.6  5.79 364937216 0 .062 .213 1.74  .682 .163 .109 .158 .102 .004 .106 .012
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-topseed.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 909    887    6649221120 62 20.7   .005 852     19.9  10.4  471330816 1 2.75  0.005 12.5  6.82 412004352 .099 .317 2.52  1.41  .196 .124 .187 .113 .005 .118 13.2  7.13 374861824 0 .117 .385 2.83  1.56  .279 .173 .266 .166 .005 .171 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-twinhan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    888    6849785856 58 25.3   .010 847     24.2  12.5  599371776 1 4.53  0.009 15.6  8.37 460025856 .124 1.11  3.90  1.21  .902 .759 .892 .732 .008 .740 17.3  9.17 425852928 0 .141 .901 4.83  2.51  .657 .387 .639 .374 .008 .382 .015
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-uclogic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    896    9912680448 11.3  6.10 368803840 1 .323 0.004 9.56 5.30 360042496 .041 .633 1.16  .271 .065 .034 .062 .029 .00  .029 9.78 5.31 331714560 0 .041 .131 1.17  .788 .082 .037 .059 .033 .001 .034 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-wacom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 19.9  10.4  488202240 1 3.02  945    826    8652214272 3 68.9   .00  0.010 134     491     118     14.3  7.67 464375808 .094 1.97  .971 .008 .001 .00  .00  .00  13.7  7.29 438435840 0 .094 2.23  .886 .015 .00  .00  .00  .00  .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-waltop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 10.4  5.60 360439808 1 .659 904    880    3768762368 12 6.82  .006 0.007 339     6.59  518     9.45 5.17 372740096 .041 .439 .292 .003 .001 .00  .00  .00  9.27 5.04 330145792 0 .032 .838 .680 .003 .001 .00  .00  .00  .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-zydacron.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 10.3  5.59 351440896 1 .663 905    837    7556943872 7 20.2   .003 0.005 164     308     333     9.89 5.39 379240448 .016 .856 .290 .002 .001 .00  .00  .00  9.37 5.06 350445568 0 .016 .777 .251 .002 .001 .00  .00  .00  .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--ads7871.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    887    2909442048 15 7.20  .001 874     20.3  10.6  468848640 1 3.92  0.008 11.6  6.67 445456384 .307 .698 1.57  .517 .627 .514 .620 .493 .014 .507 12.0  6.88 426770432 0 .323 .723 2.37  1.21  .667 .550 .646 .533 .014 .547 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--asus_atk0110.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 922    743    7856488448 2 708     .00  16.8   1000    606    6277140480 1 28.1   .00  0.007 63.4   76.8  59.0  1150607360 .106 42.7   50.3   4.71  42.4   39.0   42.3   37.8   1.16  39.0   76.8  58.8  1159159808 0 .106 42.5   50.5   4.71  42.2   38.9   42.2   37.7   1.11  38.8   .020
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--emc1403.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    887    3783520256 29 4.09  .002 876     17.3  9.08 447569920 1 2.42  0.006 11.1  6.25 425230336 .173 .389 1.49  .824 .336 .264 .334 .249 .007 .256 11.3  6.27 397017088 0 .204 .445 1.65  .881 .406 .313 .386 .301 .007 .308 .019
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--gpio-fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 964    763    8864419840 4 701     .001 44.9   72.4  36.8  1171513344 1 7.04  .013 0.005 7.63  15.0  8.62 482385920 .247 1.80  3.67  1.24  1.70  1.36  1.69  1.28  .051 1.34  15.4  8.76 461770752 0 .235 1.85  3.99  1.37  1.80  1.48  1.78  1.41  .050 1.46  .027
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--max1111.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    890    3933573120 24 4.17  .004 880     13.5  7.18 421281792 1 1.39  0.026 10.4  5.80 416702464 .221 .302 1.46  .850 .269 .186 .265 .171 .008 .179 10.8  6.05 386072576 0 .228 .328 1.59  .929 .263 .184 .257 .171 .009 .180 .014
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pcf8591.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    889    3597402112 24 4.66  .003 878     18.9  9.88 467918848 1 3.46  0.005 11.4  6.33 421801984 .089 .463 1.62  .798 .381 .295 .379 .276 .008 .284 11.2  6.20 404926464 0 .077 .411 1.72  .909 .366 .283 .362 .271 .008 .279 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pmbus--max16064.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    891    3408244736 124 4.36  .009 879     10.4  5.59 373260288 1 .487 0.012 9.23 5.07 361111552 .062 .098 .914 .670 .073 .041 .071 .026 .001 .027 8.91 4.93 324669440 0 .063 .106 1.10  .262 .068 .036 .064 .034 .00  .034 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pmbus--max8688.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    884    2884046848 50 4.82  .005 872     12.4  6.59 385654784 1 1.26  0.005 10.1  5.55 387760128 .054 .316 1.20  .302 .270 .191 .266 .167 .014 .181 10.0  5.47 336465920 0 .050 .181 1.34  .833 .152 .089 .134 .082 .002 .084 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--smsc47b397.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    890    4051034112 32 4.06  .00  879     20.8  10.9  470028288 1 4.13  0.008 12.4  6.93 439951360 .121 .728 1.70  .564 .649 .563 .643 .545 .009 .554 12.8  7.11 408109056 0 .113 .722 2.21  .576 .678 .592 .670 .579 .009 .588 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--algos--i2c-algo-pca.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 1000    795    8739659776 522    262    5209669632 1 21.7   .001 0.005 5.11  26.1  14.1  653651968 .723 3.40  8.19  2.11  3.09  2.51  3.04  2.43  .071 2.50  29.6  16.0  678588416 0 .406 3.22  10.7   3.71  3.02  2.50  2.97  2.42  .061 2.48  .079
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--busses--i2c-diolan-u2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 914    858    8521273344 3 196     .001 648     541    271    5030453248 1 15.3   .00  0.012 12.0   76.2  54.2  1160503296 1.05  31.2   47.7   8.50  30.6   27.1   30.4   25.9   1.14  27.0   88.9  65.4  1328517120 0 1.31  37.5   59.0   12.6   36.9   32.8   36.8   31.3   1.39  32.7   .092
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--busses--i2c-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 15.7  8.91 501342208 1 2.13  .00  1.14  44.1  22.6  939651072 1 6.21  .00  3.934 8.49  11.6  6.26 411815936 .133 .152 1.27  .686 .111 .043 .098 .041 .00  .041 12.1  6.53 402522112 0 .124 .125 1.90  1.27  .073 .034 .066 .030 .00  .030 .015
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--busses--i2c-tiny-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    883    3213553664 6 20.3   .001 856     53.3  27.2  987709440 1 6.14  .00  0.006 9.49  13.8  7.95 473772032 .208 1.32  2.58  .767 1.27  1.10  1.26  1.05  .037 1.09  13.5  7.67 441712640 0 .180 1.32  3.00  1.13  1.27  1.11  1.26  1.07  .033 1.11  .008
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--i2c-smbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    889    4074745856 32 4.27  .004 879     16.8  8.87 455311360 1 2.67  0.007 10.7  5.91 420896768 .053 .349 1.07  .425 .295 .212 .280 .192 .006 .198 10.8  5.96 396259328 0 .053 .332 1.58  .938 .273 .191 .261 .178 .007 .185 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ide--cmd640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    881    2333982720 5 14.1   .00  858     668    336    6061318144 3 13.6   .001 0.004 88.9   126     90.5   52.5  32.6  1102041088 .622 12.7   26.0   7.50  12.0   11.1   11.8   11.0   .161 11.1   53.4  32.8  1037664256 0 .366 13.7   26.8   7.71  12.7   11.8   12.5   11.6   .171 11.8   .218
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ide--ide-pnp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    883    3364732928 24 18.6   .00  857     18.9  9.95 502501376 1 3.55  0.005 11.1  6.12 422166528 .051 .368 1.66  .919 .323 .221 .305 .210 .007 .217 11.4  6.22 395857920 0 .051 .344 1.84  1.04  .300 .223 .291 .212 .007 .219 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--gameport--lightning.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 924    801    8439185408 9 558     .00  221     110    55.7  1900072960 1 2.63  .00  0.013 .454 11.8  6.38 389525504 .074 .639 2.04  .509 .543 .350 .511 .316 .012 .328 11.6  6.38 357523456 0 .045 .659 2.18  1.09  .541 .335 .513 .305 .015 .320 .030
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--magellan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    874    5910548480 10 136     .00  728     60.1  30.5  1001275392 1 4.02  .024 0.013 3.57  11.8  6.56 431013888 .061 .789 1.73  .510 .719 .548 .710 .516 .016 .532 11.8  6.56 402583552 0 .054 .834 2.32  1.04  .777 .628 .768 .585 .032 .617 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--spaceball.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    882    4409716736 11 21.1   .002 854     45.3  23.4  978046976 1 5.16  .009 0.005 11.3   13.1  7.45 481259520 .060 1.09  2.28  .598 1.02  .824 1.01  .791 .027 .818 13.0  7.37 464990208 0 .115 1.16  2.79  1.14  1.10  .920 1.09  .887 .027 .914 .006
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--spaceorb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 924    811    7270965248 7 668     .001 128     87.8  44.5  1483153408 1 5.58  .00  0.011 7.49  13.8  7.67 476708864 .076 1.40  3.01  .719 1.32  1.08  1.30  1.02  .035 1.05  14.2  7.89 460345344 0 .119 1.31  3.21  1.28  1.21  .968 1.18  .916 .034 .950 .013
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--stinger.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    890    5323456512 25 6.07  .002 877     19.3  10.1  458227712 1 3.54  0.005 10.8  6.00 432795648 .056 .455 1.74  .942 .348 .256 .336 .233 .011 .244 10.8  5.97 404590592 0 .049 .393 1.77  .951 .355 .258 .351 .242 .012 .254 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--turbografx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 983    744    7250518016 5 533     .002 196     77.5  39.2  1442009088 1 8.22  .001 0.005 5.66  14.9  8.43 479084544 .164 1.71  3.00  .770 1.62  1.35  1.60  1.29  .038 1.33  15.3  8.65 458661888 0 .128 1.77  3.68  1.23  1.70  1.43  1.69  1.38  .037 1.42  .024
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--twidjoy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 920    728    7340380160 6 578     .001 134     60.1  30.5  1019179008 1 3.73  .00  0.003 3.31  11.0  6.09 422350848 .058 .432 1.70  .876 .350 .242 .343 .227 .009 .236 11.2  6.15 396443648 0 .045 .475 1.73  .929 .401 .286 .396 .244 .015 .259 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--warrior.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    887    3420418048 14 6.20  .003 874     28.2  14.6  661786624 1 5.72  .00  0.014 .773 12.2  6.88 460623872 .119 .758 2.32  1.12  .702 .583 .694 .558 .017 .575 12.3  6.91 440098816 0 .098 .809 2.50  1.11  .687 .571 .675 .551 .017 .568 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--zhenhua.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    888    4743602176 24 5.20  .003 877     18.4  9.64 445284352 1 3.34  .00  0.016 .150 10.1  5.68 404258816 .056 .419 1.53  .836 .365 .274 .362 .249 .010 .259 10.7  5.93 375664640 0 .052 .424 1.67  .899 .342 .261 .340 .248 .009 .257 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--gpio_keys_polled.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    875    7154950144 6 134     .00  731     28.3  14.6  757100544 1 4.13  .001 0.007 4.33  11.8  6.49 432336896 .141 .560 1.52  .616 .512 .397 .495 .372 .015 .387 11.7  6.55 406568960 0 .132 .594 2.14  1.16  .532 .407 .522 .389 .013 .402 .009
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--newtonkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 911    886    7635537920 88 28.8   .028 828     22.3  11.6  517312512 1 3.59  .024 0.007 1.47  11.5  6.32 397033472 .076 .304 1.62  .963 .233 .158 .228 .146 .007 .153 11.0  6.04 371671040 0 .056 .344 1.77  .993 .281 .161 .266 .150 .006 .156 .010
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--stowaway.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 911    888    7115743232 79 26.2   .007 842     28.7  14.8  647950336 1 3.51  .00  0.008 1.62  11.0  6.03 381620224 .073 .314 1.06  .415 .271 .160 .260 .146 .005 .151 11.1  6.03 367828992 0 .057 .317 1.74  1.04  .268 .173 .264 .158 .007 .165 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--xtkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    889    7315292160 84 32.9   .005 836     23.2  12.1  546250752 1 3.53  .00  0.004 1.78  10.6  5.86 396423168 .067 .308 1.47  .835 .243 .135 .233 .124 .004 .128 11.0  5.98 372879360 0 .059 .299 1.61  .913 .231 .151 .217 .139 .005 .144 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--ab8500-ponkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    889    2671702016 25 3.61  .00  880     12.1  6.44 396390400 1 1.09  0.015 9.53 5.33 382492672 .133 .306 1.27  .734 .259 .205 .255 .190 .006 .196 9.82 5.52 361222144 0 .124 .318 1.44  .749 .277 .198 .272 .188 .007 .195 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--ad714x-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    897    10871443456 12.2  6.53 405532672 1 .618 0.012 10.2  5.58 400953344 .089 .151 1.17  .833 .105 .065 .095 .053 .003 .056 9.81 5.37 353468416 0 .071 .133 1.12  .734 .097 .059 .096 .054 .001 .055 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--ad714x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 912    896    10724335616 73 3.83  .005 885     13.9  7.39 443535360 1 1.41  0.018 10.4  5.76 403156992 .103 .151 1.13  .787 .126 .078 .115 .068 .002 .070 10.1  5.55 373469184 0 .087 .143 1.27  .858 .112 .073 .107 .065 .003 .068 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--adxl34x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    888    3470372864 24 6.37  .006 875     19.1  9.99 456237056 1 3.40  0.012 10.8  6.02 432451584 .090 .490 1.27  .502 .453 .362 .450 .344 .010 .354 11.0  6.18 406671360 0 .091 .450 1.80  1.01  .421 .345 .417 .330 .010 .340 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--apanel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    868    5803728896 20 130     .008 720     19.8  10.3  483037184 1 3.33  .00  0.014 .236 11.8  6.41 432099328 .150 .264 1.17  .624 .229 .159 .227 .145 .005 .150 12.3  6.66 399183872 0 .149 .302 1.77  1.03  .255 .165 .252 .155 .006 .161 .016
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--atlas_btns.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    886    2468024320 19 9.97  .001 871     18.4  9.61 496951296 1 2.07  .001 0.006 1.66  10.7  5.90 389505024 .050 .254 1.49  .533 .215 .154 .209 .144 .005 .149 10.2  5.66 365146112 0 .049 .261 1.38  .471 .223 .165 .217 .152 .006 .158 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--cma3000_d0x_i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    891    4821250048 38 4.59  .008 880     13.1  6.92 411918336 1 1.03  0.021 10.3  5.69 399892480 .086 .189 1.33  .337 .158 .111 .152 .096 .003 .099 9.76 5.39 381014016 0 .078 .179 1.24  .817 .159 .110 .154 .097 .004 .101 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--mma8450.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    893    6235873280 43 3.56  .006 883     13.1  6.91 428208128 1 1.09  0.008 10.6  5.80 409571328 .114 .175 1.36  .937 .157 .112 .154 .097 .005 .102 10.5  5.82 375820288 0 .107 .186 1.40  .938 .164 .110 .160 .103 .004 .107 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--mpu3050.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    885    2801643520 14 6.58  .001 872     21.1  11.0  503091200 1 3.90  0.013 13.3  7.67 474988544 .184 1.11  2.19  .634 1.07  .979 1.07  .950 .016 .966 12.9  7.39 447520768 0 .178 1.07  2.54  .630 1.03  .930 1.02  .911 .016 .927 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--pcap_keys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    887    3876380672 31 4.98  .003 876     15.3  8.16 417701888 1 2.36  0.007 9.37 5.21 391405568 .115 .250 1.22  .370 .210 .145 .208 .123 .007 .130 10.0  5.62 366039040 0 .120 .299 1.42  .755 .230 .170 .229 .159 .006 .165 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--pcf50633-input.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    892    4220252160 46 3.64  .004 882     12.1  6.40 405127168 1 .491 0.005 11.1  6.08 396914688 .100 .674 1.47  .505 .643 .098 .139 .086 .003 .089 10.6  5.73 378044416 0 .091 .167 1.44  1.05  .131 .083 .127 .074 .003 .077 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--pcspkr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    886    4043419648 36 4.75  .004 875     15.5  8.16 430182400 1 2.23  0.005 10.4  5.88 429850624 .118 .552 1.67  .401 .455 .325 .448 .302 .013 .315 10.5  5.86 412041216 0 .118 .480 1.74  .439 .420 .314 .413 .296 .013 .309 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--rotary_encoder.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    888    2445156352 9 5.48  .00  877     32.5  16.8  798642176 1 6.46  .001 0.005 3.26  13.4  8.03 509997056 .259 1.73  3.34  1.03  1.66  1.52  1.65  1.49  .022 1.51  14.2  8.42 486473728 0 .259 1.78  3.90  1.43  1.67  1.53  1.65  1.50  .022 1.52  .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--wm831x-on.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    889    3848122368 26 4.45  .00  879     14.4  7.62 424275968 1 1.81  0.004 10.0  5.60 399609856 .160 .270 1.35  .810 .246 .174 .236 .155 .007 .162 10.7  5.94 375808000 0 .180 .321 1.62  .961 .266 .176 .257 .165 .007 .172 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--xen-kbdfront.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    878    3040260096 12 36.4   .001 833     17.9  9.42 475729920 1 2.52  .00  0.005 .503 11.6  6.34 419602432 .068 .313 1.04  .379 .243 .171 .238 .159 .005 .164 11.4  6.16 389054464 0 .064 .284 1.46  .870 .227 .141 .223 .132 .004 .136 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--mouse--gpio_mouse.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    878    3474321408 14 43.2   .001 827     20.8  11.0  516263936 1 2.89  .008 0.005 .690 10.7  5.94 407838720 .107 .419 1.61  .865 .377 .294 .371 .277 .008 .285 11.4  6.28 369283072 0 .106 .437 1.89  1.12  .390 .280 .376 .260 .014 .274 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--mouse--vsxxxaa.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 923    814    9322655744 5 527     .002 263     40.7  20.9  910483456 1 7.24  .00  0.007 5.01  17.5  9.57 495976448 .095 2.29  4.14  1.01  2.18  1.78  2.14  1.69  .059 1.75  17.6  9.53 481603584 0 .062 2.38  4.83  1.59  2.24  1.82  2.21  1.73  .044 1.78  .010
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--serio--ct82c710.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    890    3866460160 48 3.37  .002 880     15.2  7.98 429457408 1 2.70  1.066 9.45 5.26 372199424 .081 .256 1.18  .648 .201 .136 .198 .121 .005 .126 9.80 5.40 345268224 0 .079 .273 1.44  .416 .199 .144 .192 .136 .004 .140 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--serio--parkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    889    5194399744 1189 13.0   .088 825     13.9  7.33 431079424 1 1.72  0.003 9.79 5.41 374751232 .092 .244 1.31  .804 .207 .147 .196 .139 .003 .142 9.57 5.31 349040640 0 .111 .198 1.32  .894 .180 .121 .170 .108 .002 .110 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--ad7879-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    880    3152678912 8 28.5   .001 845     31.4  16.1  741855232 1 5.36  .00  0.005 4.09  11.7  6.53 438288384 .107 .802 2.24  .555 .753 .627 .746 .600 .019 .619 11.9  6.66 419643392 0 .106 .835 2.30  1.05  .788 .643 .778 .610 .022 .632 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--cyttsp_spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    878    3092058112 10 40.0   .001 831     73.9  37.5  1251012608 1 4.93  .00  0.003 5.99  18.1   .569 12.6  7.05 461774848 .100 .841 1.93  .619 .753 .612 .747 .576 .024 .600 11.9  6.72 429998080 0 .099 .872 2.19  .542 .818 .657 .811 .623 .026 .649 .007
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--dynapro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    889    5246779392 25 5.82  .001 877     21.3  11.1  506687488 1 3.85  .00  0.016 1.04  10.7  5.86 404561920 .057 .417 1.75  .948 .335 .247 .325 .220 .009 .229 10.9  6.05 394272768 0 .058 .373 1.87  1.00  .320 .236 .308 .222 .009 .231 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--eeti_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    887    4169592832 23 4.76  .020 875     18.5  9.75 483389440 1 2.48  0.013 11.9  6.64 477642752 .224 .413 1.33  .617 .386 .287 .365 .268 .011 .279 12.5  6.96 448413696 0 .221 .442 1.94  1.03  .405 .317 .392 .295 .011 .306 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--egalax_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    872    4705062912 14 88.9   .003 772     41.6  21.2  871522304 1 4.16  .00  0.023 3.93  12.5  6.91 440889344 .171 .403 1.48  .721 .331 .244 .326 .218 .012 .230 12.6  6.79 400646144 0 .161 .353 2.08  1.35  .294 .220 .289 .204 .011 .215 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--fujitsu_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    890    4831621120 26 5.67  .003 878     18.2  9.51 451092480 1 3.32  0.006 10.5  5.84 419364864 .049 .450 1.62  .867 .343 .225 .307 .196 .008 .204 10.7  5.83 394321920 0 .118 .378 1.83  1.02  .314 .238 .301 .227 .008 .235 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--gunze.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    890    5292421120 24 5.66  .009 878     19.0  9.91 437256192 1 3.60  0.013 11.3  6.22 431570944 .051 .508 1.79  .953 .457 .339 .448 .316 .013 .329 10.7  5.96 405032960 0 .102 .425 1.69  .863 .379 .272 .373 .258 .011 .269 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--hampshire.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    890    4804964352 25 5.68  .001 877     21.4  11.1  487092224 1 4.28  0.007 11.5  6.36 424357888 .068 .464 1.98  1.07  .394 .267 .376 .247 .009 .256 11.4  6.32 402067456 0 .070 .419 1.99  1.11  .343 .247 .333 .235 .010 .245 .017
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--inexio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    890    5819588608 29 5.74  .001 878     18.1  9.49 439644160 1 3.21  0.009 10.6  5.92 404246528 .055 .378 1.51  .759 .314 .233 .309 .209 .009 .218 10.5  5.86 390856704 0 .050 .367 1.71  .965 .306 .210 .301 .198 .008 .206 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--max11801_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    884    2180907008 13 13.0   .00  865     18.5  9.60 474755072 1 3.40  0.005 11.5  6.32 427130880 .105 .342 1.28  .487 .297 .211 .291 .198 .008 .206 11.5  6.36 397316096 0 .102 .342 1.81  1.04  .288 .197 .268 .182 .009 .191 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--mk712.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 909    890    6622519296 129 5.38  .005 874     14.4  7.58 405831680 1 1.90  0.011 10.2  5.72 389582848 .137 .393 1.41  .692 .286 .207 .279 .199 .004 .203 10.1  5.64 369311744 0 .121 .385 1.57  .422 .340 .210 .334 .202 .003 .205 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--mtouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    889    5735936000 24 5.81  .004 877     17.5  9.25 447754240 1 2.88  0.009 10.3  5.81 430755840 .108 .501 1.60  .730 .444 .350 .437 .330 .012 .342 10.7  6.00 413097984 0 .083 .526 1.80  .890 .464 .371 .457 .353 .013 .366 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--penmount.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    880    4232159232 8 31.1   .001 841     37.9  19.7  949334016 1 5.94  .00  0.007 6.40  20.9  14.5  552951808 .053 7.88  9.22  .699 7.81  7.52  7.79  7.48  .038 7.51  21.5  14.7  540573696 0 .074 7.81  10.1   1.46  7.75  7.48  7.73  7.43  .039 7.47  .006
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--stmpe-ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    3317932032 14 6.71  .00  875     19.3  10.1  474124288 1 2.03  0.006 13.2  7.55 509108224 .358 .925 2.08  .676 .863 .726 .851 .697 .021 .718 14.4  8.11 487063552 0 .368 1.17  3.04  1.26  1.13  .987 1.12  .960 .021 .981 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchit213.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    890    4863565824 24 5.30  .003 878     19.9  10.4  490143744 1 3.27  .00  0.006 1.20  11.7  6.64 433278976 .054 .570 1.99  1.01  .511 .421 .504 .376 .013 .389 11.1  6.23 413908992 0 .050 .521 1.89  .556 .476 .382 .470 .366 .012 .378 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchright.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    890    5470097408 27 5.60  .001 878     19.3  10.2  471642112 1 3.68  0.007 9.95 5.58 414322688 .057 .402 1.53  .369 .344 .252 .335 .229 .009 .238 10.3  5.74 386076672 0 .066 .378 1.82  1.07  .307 .236 .304 .224 .008 .232 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    889    4906688512 23 5.66  .001 877     18.7  9.79 441417728 1 3.65  .00  0.005 .210 11.0  6.11 432873472 .088 .485 1.65  .812 .451 .335 .449 .312 .013 .325 10.5  5.85 401362944 0 .061 .448 1.72  .883 .406 .307 .401 .290 .013 .303 .010
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--tsc40.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    888    4601880576 20 5.39  .001 877     23.9  12.3  541716480 1 4.31  .00  0.005 1.86  11.7  6.52 438583296 .081 .606 2.08  1.01  .495 .403 .490 .361 .018 .379 10.9  6.03 403238912 0 .053 .496 1.92  .985 .441 .336 .435 .321 .012 .333 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--wacom_w8001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    884    3785973760 5 15.2   .00  862     75.4  38.6  1622274048 1 10.8   .00  0.006 17.4   24.0  15.7  812896256 .058 7.58  10.0   1.09  7.45  6.95  7.43  6.84  .100 6.94  26.8  17.1  819965952 0 .054 8.08  11.7   2.02  7.94  7.26  7.92  7.13  .107 7.24  .011
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--avm_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    887    4295081984 28 8.07  .001 873     20.7  10.8  499245056 1 4.19  0.006 10.7  5.88 426483712 .063 .345 1.29  .629 .302 .207 .293 .185 .007 .192 10.8  5.97 384606208 0 .054 .343 1.64  .865 .301 .200 .298 .189 .007 .196 .012
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--b1pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    889    6223376384 21 8.69  .001 874     37.1  19.1  916561920 1 6.34  .001 0.005 5.42  14.7  8.43 550211584 .101 1.75  3.12  .652 1.68  1.41  1.67  1.35  .040 1.39  15.3  8.69 523345920 0 .137 1.89  3.87  1.14  1.79  1.56  1.78  1.50  .054 1.55  .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--b1pcmcia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    890    3230007296 865 8.25  .068 852     10.9  5.83 369053696 1 .506 0.009 9.27 5.17 373452800 .094 .177 .972 .594 .147 .095 .145 .089 .003 .092 9.08 5.08 340824064 0 .112 .176 .947 .263 .149 .103 .144 .091 .004 .095 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--t1pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    890    5340979200 21 6.31  .003 877     22.3  11.6  533282816 1 4.62  .003 0.006 .427 12.2  6.88 461316096 .132 .864 1.77  .453 .806 .626 .801 .599 .020 .619 12.2  6.91 443006976 0 .113 .764 2.48  1.14  .709 .570 .704 .548 .019 .567 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--eicon--divadidd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 916    807    7331262464 4 404     .00  386     902    452    6554103808 1 17.8   .00  0.005 8.60  155    120    1429303296 1.70  82.9   111     15.8   81.5   72.3   81.1   70.2   1.90  72.1   167    132    1474318336 0 .915 94.1   124     16.9   92.8   81.4   92.5   78.9   2.25  81.1   .210
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--avma1_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    887    4998279168 29 8.87  .00  873     20.8  10.8  512069632 1 3.63  .003 0.013 1.17  11.1  6.16 425295872 .065 .511 1.37  .518 .450 .330 .442 .308 .012 .320 11.6  6.44 399454208 0 .055 .544 2.00  1.15  .487 .339 .473 .304 .011 .315 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--elsa_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    892    3127795712 16 4.47  .001 881     22.2  11.6  519012352 1 4.07  .00  0.005 1.41  11.8  6.61 449339392 .098 .580 1.97  .953 .522 .381 .506 .358 .013 .371 11.4  6.40 412459008 0 .108 .541 2.00  1.10  .459 .358 .452 .342 .013 .355 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--sedlbauer_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    3315478528 18 4.92  .001 877     22.6  11.7  515428352 1 4.08  .00  0.007 .745 10.8  5.99 426516480 .088 .487 1.81  .945 .399 .305 .396 .287 .011 .298 11.1  6.15 414027776 0 .110 .464 1.94  1.02  .420 .321 .416 .306 .011 .317 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--teles_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    889    3544657920 19 5.33  .003 878     21.5  11.2  500191232 1 3.82  .00  0.011 1.25  11.0  6.09 437751808 .065 .526 1.83  .904 .490 .396 .483 .373 .013 .386 11.9  6.58 416870400 0 .066 .571 2.21  1.13  .488 .403 .479 .384 .013 .397 .023
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--dell-led.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    887    2555191296 17 4.59  .002 877     16.3  8.57 457863168 1 2.22  0.013 11.6  6.75 443047936 .131 1.50  2.40  .563 1.06  .958 1.05  .943 .011 .954 11.6  6.64 403107840 0 .112 1.06  2.53  1.11  1.03  .932 1.02  .918 .011 .929 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-bd2802.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 909    851    6134775808 8 182     .001 655     902    452    5684801536 3 9.00  .001 0.005 19.3   393     19.3   21.2  11.9  683081728 .338 2.08  3.69  1.02  2.00  1.67  1.98  1.60  .051 1.65  21.6  12.2  657698816 0 .366 2.28  4.55  1.54  2.19  1.89  2.18  1.82  .063 1.88  .016
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-dac124s085.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 912    851    8179093504 14 179     .00  635     19.3  10.1  501678080 1 2.94  .001 0.014 .892 10.5  5.72 403382272 .108 .308 1.45  .841 .238 .144 .217 .133 .005 .138 10.5  5.74 368181248 0 .094 .276 1.49  .900 .231 .134 .226 .123 .003 .126 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-lp5521.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    854    6605295616 8 415     .002 428     73.0  36.9  1133391872 1 3.41  .001 0.007 3.54  15.9  8.97 539635712 .165 2.02  3.28  .759 1.97  1.71  1.96  1.66  .041 1.70  16.7  9.43 520232960 0 .169 2.19  4.21  1.42  2.06  1.75  2.02  1.69  .044 1.73  .008
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-ot200.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 917    866    8478785536 24 208     .003 636     903    452    5951811584 9 11.4   .003 385.969 24.4   351     57.0   8.96 4.94 351391744 .051 .117 .955 .667 .087 .041 .083 .032 .001 .033 10.2  5.50 340250624 0 .050 .229 1.23  .847 .197 .103 .181 .090 .002 .092 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-pca9633.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    884    3595862016 8 18.1   .001 859     17.0  8.95 464367616 1 2.57  0.011 11.2  6.57 457654272 .261 .963 2.13  .882 .932 .746 .917 .694 .046 .740 11.5  6.72 442871808 0 .256 1.00  2.27  .870 .956 .768 .949 .718 .045 .763 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    3385024512 15 5.26  .003 878     20.8  10.8  563671040 1 3.80  .00  0.006 1.42  11.6  6.72 461660160 .146 1.35  2.45  .759 1.31  1.04  1.28  1.01  .020 1.03  12.1  7.02 441937920 0 .137 1.89  2.78  .503 1.46  1.24  1.45  1.21  .020 1.23  .022
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-backlight.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    893    3784601600 36 3.38  .003 883     14.0  7.40 426500096 1 1.17  0.005 11.2  6.09 410107904 .048 .187 1.43  .523 .152 .108 .150 .100 .004 .104 10.5  5.74 380817408 0 .043 .164 1.22  .732 .138 .089 .135 .082 .003 .085 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-default-on.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 910    897    7523713024 76 3.25  .010 888     9.56 5.12 338698240 1 .440 0.008 8.15 4.54 330354688 .042 .126 .903 .633 .098 .060 .095 .054 .002 .056 7.83 4.23 306950144 0 .458 .137 .434 .180 .115 .058 .111 .052 .001 .053 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    892    3421970432 27 3.44  .001 883     13.4  7.11 397545472 1 1.67  0.005 9.35 5.22 384745472 .045 .258 1.04  .601 .217 .157 .211 .149 .006 .155 9.71 5.36 364687360 0 .049 .289 1.21  .699 .239 .158 .232 .150 .004 .154 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--macintosh--mac_hid.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    888    3547176960 39 3.98  .002 878     15.8  8.27 450482176 1 2.22  .003 0.007 .327 9.86 5.40 383918080 .058 .645 1.24  .394 .171 .120 .167 .106 .003 .109 9.68 5.33 351559680 0 .104 .223 1.27  .736 .166 .116 .160 .106 .004 .110 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--md--dm-zero.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    891    4126101504 72 3.06  .003 882     11.4  6.10 394805248 1 .457 0.005 9.32 5.15 372719616 .043 .091 1.02  .692 .072 .038 .068 .032 .001 .033 9.65 5.27 358477824 0 .046 .100 1.09  .720 .077 .052 .074 .046 .002 .048 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--max2165.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    883    2878660608 5 17.6   .001 858     903    453    5864849408 3 14.2   .00  0.008 81.4   212     134     33.4  24.7  658526208 .095 16.6   19.4   1.87  16.5   15.9   16.5   15.7   .221 15.9   34.4  25.4  606199808 0 .056 17.3   20.4   2.18  17.2   16.6   17.2   16.3   .227 16.6   .011
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mc44s803.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    888    3128492032 5 10.1   .00  871     33.3  17.1  779218944 1 9.12  0.006 17.0  11.3  705994752 .077 4.75  6.12  .912 4.71  4.50  4.71  4.39  .096 4.48  17.1  11.3  673521664 0 .061 4.82  6.52  1.21  4.80  4.55  4.79  4.44  .101 4.54  .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2060.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    883    3776872448 7 28.1   .002 848     31.4  16.2  721129472 1 5.58  .001 0.009 3.62  13.6  7.86 503762944 .057 1.38  2.51  .776 1.32  1.16  1.32  1.11  .034 1.15  13.3  7.65 472215552 0 .066 1.33  2.80  1.14  1.27  1.12  1.26  1.08  .033 1.12  .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt20xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    884    3177816064 5 12.9   .00  861     241    121    4295839744 1 12.9   .00  0.005 33.0   44.9  32.5  902041600 .083 21.2   24.6   2.20  21.1   19.4   21.1   18.9   .452 19.4   43.3  30.9  914808832 0 .072 19.8   23.6   2.67  19.7   18.0   19.7   17.6   .416 18.0   .021
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2131.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    884    2837004288 4 17.8   .00  860     48.5  24.9  993345536 1 7.35  .001 0.017 9.61  17.1  10.8  647970816 .077 4.27  5.59  .947 4.23  3.88  4.22  3.79  .077 3.87  17.8  11.4  622129152 0 .062 4.78  6.66  1.04  4.75  4.36  4.72  4.26  .089 4.35  .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2266.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    885    5761007616 5 43.2   .002 835     76.8  39.3  1660571648 1 13.4   .001 0.003 18.1   22.3  14.8  753930240 .078 7.01  9.47  1.78  6.96  6.37  6.95  6.19  .171 6.36  22.5  15.0  727826432 0 .075 7.13  9.95  2.18  7.09  6.51  7.08  6.33  .175 6.50  .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mxl5007t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 918    790    8339869696 5 663     .00  109     95.3  48.2  1846874112 1 13.6   .001 0.005 8.66  121    87.9  1720152064 .070 11.8   80.2   55.8   10.7   5.54  9.62  5.28  .132 5.41  226    197    1484853248 0 .093 164     189     16.9   163     139     163     133     4.95  138     .192
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--qt1010.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 912    875    8157462528 3 218     .00  645     236    119    4338458624 1 11.0   .00  0.009 38.1   33.4  22.7  810708992 .095 12.1   14.6   1.78  12.0   11.2   12.0   10.9   .302 11.2   32.0  21.7  791801856 0 .050 11.8   14.9   2.23  11.8   10.9   11.8   10.6   .300 10.9   .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda18218.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    878    7252938752 7 139     .002 727     101    51.1  2145185792 1 10.3   .00  0.005 21.7   23.3  14.8  783200256 .062 6.69  8.72  1.44  6.63  5.97  6.62  5.77  .186 5.95  22.1  14.3  740552704 0 .083 7.11  9.48  1.85  7.01  6.19  7.00  5.98  .193 6.17  .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda8290.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 911    883    10660843520 3 99.7   .00  771     239    121    5571747840 1 25.7   .00  0.005 79.0   187    172    1673441280 .082 157     164     4.32  157     155     157     154     1.10  155     191    175    1680105472 0 .071 159     167     5.11  159     157     159     156     1.12  157     .010
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda9887.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 935    872    8414806016 6 223     .00  633     186    93.7  4474728448 1 23.8   .001 0.005 17.6   56.9  38.3  1059971072 .075 21.0   29.6   5.28  20.7   19.4   20.6   18.7   .595 19.3   47.5  32.7  1015820288 0 .102 18.0   25.2   4.20  17.8   16.6   17.7   16.0   .527 16.6   .020
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--bt8xx--dvb-bt8xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 35.1  18.1  694890496 1 6.58  925    799    7779733504 1 21.3   .00  0.004 237     32.7  17.5  807165952 .182 8.51  5.37  .017 .001 .00  .00  .00  36.2  19.2  799834112 0 .255 9.56  6.13  .042 .001 .00  .00  .00  .015
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-a800.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    889    2930774016 31 4.22  .002 877     20.5  10.6  519397376 1 2.40  0.009 14.1  7.63 478638080 .065 .266 1.33  .651 .238 .169 .233 .154 .006 .160 14.2  7.61 455966720 0 .067 .335 1.74  .999 .305 .238 .302 .220 .016 .236 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-au6610.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    887    4386394112 26 5.04  .001 874     22.0  11.4  550359040 1 2.95  0.005 14.8  8.02 525955072 .124 .511 1.43  .567 .452 .369 .449 .346 .010 .356 15.4  8.26 485281792 0 .121 .558 2.10  1.06  .528 .416 .524 .386 .011 .397 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 32.0  16.4  627572736 1 5.61  1000    968    2514042880 78.0  56.4  1217835008 4.22  8.51  12.4   2.23  8.30  6.53  8.23  6.34  .095 6.44  81.2  56.8  1223245824 0 5.03  8.91  12.9   2.36  8.70  6.89  8.64  6.70  .113 6.81  .013
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    872    4147048448 11 51.9   83.5   716     85.4  43.2  1386856448 1 4.85  1.09  0.005 2.95  23.4  12.8  637886464 .077 2.23  4.23  1.14  2.10  1.69  2.10  1.59  .069 1.66  22.9  12.5  614973440 0 .094 2.18  4.16  1.22  2.07  1.68  2.04  1.58  .058 1.64  .008
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-ce6230.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    888    3329769472 23 4.85  .001 875     23.7  12.3  578015232 1 3.14  0.005 15.6  8.40 534364160 .100 .529 1.55  .556 .502 .426 .494 .404 .011 .415 15.0  8.07 515530752 0 .086 .479 1.94  .637 .437 .332 .413 .318 .009 .327 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-cinergyT2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    878    3146264576 9 44.4   .001 825     32.9  16.9  623726592 1 5.36  .00  0.006 .977 17.7  9.55 599789568 .077 .696 1.88  .710 .658 .530 .644 .502 .017 .519 18.6  9.92 583282688 0 .100 .748 2.73  1.36  .684 .547 .681 .518 .019 .537 .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-cinergyT2.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c 905    886    3374084096 10 8.00  .002 869     27.7  14.3  602316800 1 3.80  0.006 20.5  12.2  660213760 .091 3.33  4.70  .692 3.29  3.14  3.29  3.10  .024 3.12  21.2  12.6  615858176 0 .084 3.46  5.53  1.45  3.38  3.21  3.36  3.18  .027 3.21  .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-common.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    894    11876143104 18.9  9.81 550699008 1 .578 0.007 14.6  7.74 522514432 .070 .083 .897 .456 .066 .042 .065 .038 .001 .039 14.4  7.58 497471488 0 .118 .139 1.29  .494 .096 .070 .094 .062 .003 .065 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-mb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    882    3654656000 10 10.8   .001 861     39.8  20.3  798568448 1 8.88  0.006 21.0  11.4  673869824 .344 1.18  3.42  1.31  1.11  .950 1.10  .911 .029 .940 21.4  11.5  633307136 0 .260 1.31  4.17  1.97  1.17  .946 1.16  .915 .027 .942 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-mc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    897    10208026624 15.2  7.97 476434432 1 .482 0.007 12.7  6.86 462245888 .056 .101 .785 .411 .080 .044 .079 .036 .001 .037 13.8  7.26 451825664 0 .056 .313 1.63  1.01  .280 .197 .276 .192 .002 .194 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-digitv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    872    6335799296 4 217     26.9   614     131    66.1  2626953216 1 10.0   .001 0.004 16.3   25.5  15.8  774340608 .545 5.62  7.83  1.46  5.56  5.01  5.55  4.87  .128 5.00  25.6  16.0  739164160 0 .543 5.98  8.75  2.03  5.90  5.29  5.89  5.13  .143 5.28  .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtt200u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 904    879    2875727872 13 31.1   .001 839     45.9  23.4  886587392 1 9.31  .00  0.004 1.14  21.5  11.5  622919680 .276 .847 3.11  1.39  .759 .622 .748 .598 .014 .612 23.6  12.5  621670400 0 .396 1.18  4.02  1.61  1.06  .776 1.06  .757 .016 .773 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtt200u.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c 904    882    2818609152 10 19.3   .001 854     31.4  16.1  617279488 1 5.14  0.005 21.6  11.5  614289408 .296 1.19  2.98  1.19  1.11  .947 1.10  .902 .019 .921 20.6  11.1  589828096 0 .206 1.16  3.35  1.69  1.08  .895 1.07  .873 .018 .891 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtv5100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    876    4110196736 13 47.7   .002 819     26.7  13.8  545828864 1 4.05  .001 0.005 .821 14.3  7.79 521707520 .074 .401 1.31  .503 .362 .290 .359 .274 .013 .287 15.4  8.22 494194688 0 .064 .590 2.12  1.09  .546 .449 .538 .434 .011 .445 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-gl861.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    886    4144754688 25 4.82  .00  873     22.5  11.6  547737600 1 3.59  0.005 14.6  7.93 518426624 .120 .533 1.46  .527 .508 .412 .504 .394 .010 .404 16.5  8.90 509153280 0 .116 .606 2.55  1.39  .535 .411 .518 .389 .012 .401 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-mxl111sf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 912    870    10919006208 1 121     .001 725     911    459    12434141184 1 248     .00  376.646 139     906    866    8887103488 7.43  736     843     76.5   735     708     735     707     3.77  711     906    868    8993083392 0 7.23  708     846     99.2   707     679     707     677     4.33  681     .176
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-mxl111sf.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c 903    879    2517659648 582 5.68  .033 844     41.9  21.3  876199936 4 3.39  .001 0.004 1.74  .373 .053 29.6  15.2  842903552 .378 .179 1.30  .721 .148 .090 .139 .084 .002 .086 29.9  15.3  822763520 0 .282 .286 1.42  .786 .244 .160 .242 .151 .005 .156 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-nova-t-usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    882    2835734528 9 23.6   .00  850     44.4  22.7  867696640 1 4.15  .001 0.005 4.64  14.4  7.76 492118016 .063 .445 1.58  .816 .407 .323 .401 .300 .014 .314 14.7  7.95 468041728 0 .076 .574 2.08  .693 .532 .427 .526 .385 .027 .412 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-pctv452e.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    872    8579461120 4 512     29.2   310     67.8  34.5  1276088320 1 11.3   3.85  0.006 6.28  29.9  19.0  941273088 .102 7.95  10.3   1.38  7.87  7.28  7.87  7.14  .114 7.26  30.5  19.1  920449024 0 .095 7.55  10.1   1.43  7.44  6.88  7.42  6.76  .107 6.87  .007
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-rtl28xxu.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 915    859    7945986048 7 293     .001 545     94.2  47.7  2194984960 1 6.07  .00  0.012 10.4   26.9  14.4  748953600 .104 3.05  5.58  1.34  2.92  2.45  2.89  2.40  .036 2.44  30.0  15.8  690909184 0 .101 3.09  6.52  2.02  2.98  2.42  2.95  2.38  .028 2.40  .037
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-ttusb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    882    3607404544 6 18.3   .00  854     72.5  36.7  1344114688 1 16.6   .00  0.005 6.71  33.3  20.1  943747072 .212 7.60  11.0   2.08  7.49  7.04  7.49  6.93  .092 7.03  32.4  19.7  885587968 0 .153 7.46  10.6   1.79  7.37  6.92  7.35  6.83  .084 6.91  .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-umt-010.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    889    4248576000 37 3.77  .003 877     19.4  10.1  510504960 1 2.07  0.003 13.9  7.51 492982272 .061 .285 1.10  .472 .260 .195 .258 .181 .006 .187 13.6  7.30 488267776 0 .056 .394 1.81  1.09  .348 .262 .331 .244 .006 .250 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 907    873    5092163584 5 89.7   83.5   684     99.1  50.0  1599262720 1 7.05  2.37  0.009 9.05  32.4  20.6  658857984 .078 10.4   13.4   1.87  10.2   8.92  10.2   8.50  .345 8.85  38.4  23.9  659394560 0 .069 12.4   16.8   3.02  12.3   10.7   12.2   10.3   .415 10.7   .008
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c 906    881    4258680832 7 39.2   63.6   760     182    119    3135930368 1 12.9   3.15  0.004 7.29  45.2  27.5  779755520 .078 14.9   19.7   3.05  14.8   12.6   14.6   12.0   .568 12.6   49.4  30.8  738713600 0 .068 18.0   23.1   3.36  17.8   15.2   17.7   14.4   .725 15.1   .024
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--mxl111sf-demod.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 26.0  13.7  558440448 1 4.89  905    866    6590775296 2 35.2   .00  0.004 475     49.0   288     21.5  11.3  561782784 .047 .181 4.35  2.46  .077 .041 .063 .018 .001 .019 20.4  10.8  525598720 0 .075 .169 4.23  2.48  .061 .015 .029 .011 .00  .011 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--cxd2820r.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 41.9  21.6  810020864 1 7.57  914    809    5673959424 1 775     0.007 47.0  30.7  978464768 .069 14.8   19.6   2.94  14.7   14.2   14.7   14.1   .113 14.2   46.0  30.3  946855936 0 .070 15.1   19.5   2.47  15.0   14.6   15.0   14.5   .111 14.6   .024
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dib3000mb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 42.1  23.4  897662976 1 12.0   909    874    8804950016 1 41.8   .00  0.005 805     33.0  18.7  787853312 .116 .342 10.4   8.93  .243 .185 .236 .174 .005 .179 33.9  19.3  762294272 0 .119 .340 10.2   8.69  .266 .175 .239 .170 .004 .174 .005
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dib3000mc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 38.3  21.2  786599936 1 10.0   905    865    4563730432 1 23.3   .00  0.005 810     913    897    2642706432 913    897    2616786944
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dvb_dummy_fe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 11.8  6.36 391831552 1 1.00  904    879    3522621440 15 10.3   .002 0.005 801     10.1   48.1   10.9  5.91 421904384 .058 .087 1.35  .954 .040 .024 .038 .016 .001 .017 10.6  5.79 377090048 0 .054 .075 1.15  .827 .040 .021 .037 .018 .00  .018 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--ec100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 14.0  7.49 431022080 1 1.92  904    879    4254519296 4 13.8   .00  0.010 648     14.8   192     12.3  6.66 432652288 .065 .075 1.23  .761 .034 .019 .031 .009 .001 .010 11.5  6.20 385277952 0 .076 .080 1.46  1.06  .033 .011 .025 .009 .00  .009 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--isl6405.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 867    847    14999998464 10.9  5.86 393932800 1 .211 0.005 9.42 5.14 384303104 .041 .442 .905 .316 .021 .006 .018 .003 .001 .004 9.41 5.12 334700544 0 .041 .038 .858 .643 .023 .008 .021 .004 .00  .004 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--isl6421.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 895    876    14999998464 10.2  5.44 388116480 1 0.011 9.89 5.40 378621952 .048 .050 .932 .683 .030 .009 .029 .003 .00  .003 9.99 5.44 351399936 0 .038 .044 1.05  .851 .019 .007 .019 .003 .00  .003 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--it913x-fe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 46.5  24.5  806592512 1 10.4   905    806    6837026816 1 74.9   .001 0.006 711     76.4  57.7  1558290432 .292 36.1   45.4   8.01  36.1   34.5   36.0   33.9   .591 34.5   76.5  57.0  1546854400 0 .349 35.0   45.3   8.74  34.9   33.4   34.9   32.8   .573 33.4   .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--lnbp21.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    893    12020547584 10.1  5.43 390299648 1 0.005 9.43 5.21 370409472 .040 .052 .903 .253 .026 .009 .024 .006 .00  .006 9.41 5.14 364306432 0 .041 .049 .911 .705 .036 .015 .036 .006 .001 .007 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--lnbp22.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 912    895    10449178624 2392 27.4   .165 735     11.1  5.94 373006336 1 .194 0.005 9.63 5.30 385548288 .044 .049 .521 .302 .037 .013 .028 .005 .00  .005 9.33 5.03 351281152 0 .049 .037 .803 .614 .024 .010 .023 .007 .00  .007 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--rtl2830.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 18.1  9.52 499855360 1 2.12  943    838    8803512320 1 13.4   .001 0.005 78.3   14.4  7.78 527495168 .062 .339 1.29  .623 .314 .241 .306 .222 .008 .230 15.4  8.27 507699200 0 .048 .360 1.72  1.03  .317 .246 .313 .229 .008 .237 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--stb6000.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    888    4495745024 12 11.8   .010 870     19.9  10.5  479641600 1 3.29  0.027 12.9  7.49 563871744 .086 1.32  2.47  .749 1.27  1.09  1.27  1.05  .034 1.09  12.8  7.44 527609856 0 .067 1.33  2.77  .672 1.27  1.08  1.26  1.05  .034 1.08  .004
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tda18271c2dd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    876    6548439040 3 140     .00  724     505    254    4724924416 1 11.8   .00  0.005 24.5   69.9  56.1  1087295488 .098 43.1   47.7   3.25  43.0   40.4   43.0   39.4   .942 40.3   67.7  54.7  1044791296 0 .081 42.2   46.3   2.89  42.2   39.3   42.2   38.4   .905 39.3   .018
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tda826x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 905    891    3596525568 13 8.21  .001 877     17.0  9.07 441028608 1 1.54  0.006 12.3  7.02 497926144 .098 1.02  1.91  .632 .987 .846 .981 .807 .023 .830 12.3  7.05 458784768 0 .052 .944 2.24  .518 .917 .808 .914 .784 .023 .807 .010
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tua6100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    899    3039076352 19.9  10.5  459423744 1 2.55  0.006 13.8  8.00 556093440 .076 1.30  2.54  .794 1.26  1.11  1.25  1.06  .038 1.10  12.9  7.46 520507392 0 .053 1.26  2.61  .651 1.22  1.07  1.21  1.03  .038 1.07  .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--ttpci--budget-patch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 908    886    6966337536 85 20.5   .003 840     50.4  25.7  864157696 1 4.49  .00  0.007 2.13  19.8  11.2  694476800 .096 2.00  3.29  .753 1.93  1.72  1.91  1.67  .039 1.71  20.8  11.6  669384704 0 .066 2.02  3.78  1.13  1.95  1.77  1.93  1.71  .041 1.75  .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--ttpci--budget.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 906    880    5129519104 4 36.1   .00  833     106    53.6  2407927808 1 20.7   .001 0.005 16.9   74.3  55.0  1408172032 .344 37.3   45.9   3.10  37.0   35.5   36.9   35.0   .428 35.5   80.7  58.7  1516281856 0 .390 39.8   49.7   4.52  39.5   37.9   39.4   37.4   .479 37.9   .024
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-adstech-dvb-t-pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 896    876    14999998464 8.17 4.51 310386688 1 .216 .00  0.004 .002 6.65 3.75 317964288 .417 .047 .209 .077 .029 .008 .026 .004 .00  .004 5.80 3.33 226123776 0 .039 .041 .196 .082 .024 .008 .023 .004 .00  .004 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-alink-dtu-m.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    893    12236890112 7.50 4.10 314097664 1 .076 0.012 7.55 4.26 318427136 .617 .060 .245 .112 .037 .013 .033 .005 .00  .005 6.27 3.53 278638592 0 .035 .045 .226 .089 .024 .008 .023 .001 .00  .001 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-anysee.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12058112000 7.77 4.27 317779968 1 .153 0.007 6.27 3.59 319033344 .312 .044 .180 .077 .028 .006 .026 .003 .00  .003 6.81 3.83 283582464 0 .038 .045 .213 .071 .028 .008 .026 .004 .00  .004 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-apac-viewcomp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    894    12065988608 8.03 4.44 313888768 1 .255 0.006 6.89 3.88 325632000 .443 .054 .194 .082 .030 .011 .029 .004 .00  .004 6.60 3.73 287858688 0 .041 .049 .192 .090 .028 .007 .023 .003 .00  .003 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-asus-pc39.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12059795456 7.75 4.27 323264512 1 .072 0.012 7.09 4.01 318689280 .439 .051 .198 .085 .030 .010 .028 .004 .00  .004 6.85 3.88 287961088 0 .037 .045 .192 .080 .027 .006 .025 .004 .00  .004 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-ati-tv-wonder-hd-600.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12013703168 7.99 4.35 308314112 1 .144 0.006 6.74 3.87 323219456 .546 .049 .186 .076 .031 .009 .030 .006 .00  .006 6.70 3.78 276185088 0 .037 .045 .196 .088 .023 .006 .023 .002 .00  .002 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-ati-x10.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 891    872    14999998464 7.40 4.09 307851264 1 .153 0.005 6.12 3.47 318210048 .389 .044 .159 .052 .026 .007 .023 .003 .00  .003 7.05 3.99 283381760 0 .036 .043 .180 .073 .028 .006 .025 .002 .00  .002 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-a16d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    11954282496 7.44 4.11 315346944 1 .135 0.004 6.43 3.70 318218240 .408 .049 .192 .083 .029 .008 .028 .004 .00  .004 6.58 3.69 282292224 0 .036 .038 .190 .091 .025 .010 .024 .004 .00  .004 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-cardbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 898    878    14999998464 7.84 4.29 322527232 1 .095 0.006 6.72 3.79 331726848 .333 .048 .207 .090 .027 .008 .026 .005 .00  .005 6.60 3.73 281817088 0 .037 .050 .203 .083 .027 .009 .027 .003 .00  .003 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-dvbt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 896    877    14999998464 7.74 4.31 316252160 1 .185 0.006 6.67 3.79 320843776 .463 .060 .189 .070 .042 .010 .039 .004 .00  .004 6.66 3.76 284901376 0 .038 .046 .205 .092 .030 .010 .026 .004 .00  .004 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-m135a.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12171087872 7.89 4.33 316776448 1 .316 0.005 6.82 3.81 321851392 .595 .060 .175 .059 .035 .010 .032 .004 .00  .004 6.88 3.88 283480064 0 .037 .460 .617 .094 .039 .018 .036 .003 .00  .003 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-m733a-rm-k6.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    893    12249165824 7.39 4.08 323997696 1 0.005 6.89 3.91 315842560 .527 .049 .190 .077 .029 .010 .025 .005 .00  .005 6.43 3.65 281346048 0 .034 .055 .196 .069 .035 .011 .033 .004 .00  .004 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-rm-ks.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 914    895    12069875712 7.91 4.40 308727808 1 .225 0.013 6.53 3.71 321466368 .413 .053 .207 .084 .034 .013 .030 .004 .001 .005 6.57 3.66 283914240 0 .033 .043 .186 .083 .026 .008 .023 .003 .00  .003 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12043567104 8.13 4.44 314970112 1 .190 0.011 6.76 3.82 321122304 .389 .049 .190 .067 .029 .009 .024 .005 .00  .005 6.78 3.82 284217344 0 .039 .052 .199 .080 .026 .009 .023 .003 .002 .005 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avertv-303.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    11799949312 7.76 4.25 308273152 1 0.005 6.67 3.80 313679872 .377 .048 .199 .073 .031 .008 .027 .004 .00  .004 6.47 3.66 278433792 0 .037 .051 .216 .102 .033 .008 .028 .003 .00  .003 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-azurewave-ad-tu700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12089413632 7.48 4.12 307884032 1 .039 0.004 7.05 3.98 318230528 .454 .051 .222 .102 .032 .009 .028 .004 .00  .004 6.44 3.66 278609920 0 .035 .045 .213 .101 .029 .008 .024 .004 .001 .005 .003
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-behold-columbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 914    894    12173766656 7.32 4.05 317145088 1 .155 0.005 6.97 3.95 316407808 .355 .048 .215 .087 .031 .011 .030 .005 .00  .005 6.39 3.64 277254144 0 .037 .045 .181 .078 .029 .007 .025 .003 .00  .003 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-behold.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    11987296256 7.60 4.21 312594432 1 0.005 7.04 3.99 321060864 .494 .046 .197 .079 .030 .010 .027 .005 .001 .006 6.72 3.79 288174080 0 .037 .050 .181 .078 .028 .007 .024 .003 .00  .003 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-budget-ci-old.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    892    12231598080 7.80 4.28 325054464 1 .163 0.013 6.88 3.87 317530112 .498 .055 .211 .070 .037 .011 .030 .006 .001 .007 6.61 3.72 275333120 0 .036 .052 .194 .083 .025 .008 .023 .002 .00  .002 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-cinergy-1400.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12074745856 7.74 4.30 303689728 1 0.010 6.89 3.84 322273280 .417 .046 .195 .083 .032 .007 .030 .004 .00  .004 6.76 3.82 281186304 0 .039 .051 .185 .076 .030 .009 .026 .004 .001 .005 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-cinergy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    893    12108591104 7.26 4.02 314572800 1 0.005 6.50 3.67 318377984 .383 .049 .184 .067 .034 .010 .030 .004 .00  .004 6.64 3.75 284450816 0 .040 .043 .184 .076 .027 .007 .023 .003 .00  .003 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dib0700-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 914    896    12120997888 7.61 4.19 313585664 1 .089 0.006 6.73 3.81 320778240 .466 .038 .182 .076 .029 .011 .028 .004 .001 .005 6.83 3.86 283643904 0 .038 .536 .692 .089 .032 .008 .024 .003 .00  .003 .002
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dib0700-rc5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    894    12009095168 8.03 4.40 308191232 1 0.016 7.55 4.24 317460480 .055 .046 .706 .087 .032 .015 .030 .002 .00  .002 7.27 4.09 285085696 0 .036 .499 .651 .082 .459 .440 .457 .435 .001 .436 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-digitalnow-tinytwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    11890286592 8.37 4.55 323235840 1 .218 0.005 6.91 3.94 315572224 .509 .045 .184 .080 .028 .009 .025 .004 .001 .005 6.86 3.87 291409920 0 .038 .048 .201 .077 .028 .012 .028 .003 .00  .003 .008
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-digittrade.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 898    878    14999998464 7.83 4.33 323002368 1 .213 0.005 6.42 3.70 317378560 .415 .048 .190 .083 .030 .008 .028 .005 .00  .005 6.83 3.85 282443776 0 .035 .046 .209 .100 .027 .008 .023 .004 .001 .005 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dm1105-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    12013903872 7.96 4.40 313217024 1 .233 0.010 6.75 3.84 317947904 .593 .046 .175 .069 .030 .009 .028 .005 .001 .006 6.63 3.72 279818240 0 .038 .050 .192 .074 .028 .011 .025 .006 .00  .006 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dntv-live-dvb-t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    895    11995287552 7.82 4.27 320917504 1 .155 0.005 6.76 3.82 321568768 .459 .068 .197 .076 .035 .008 .029 .004 .00  .004 6.58 3.74 287268864 0 .040 .041 .224 .091 .025 .007 .023 .002 .00  .002 .001
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dntv-live-dvbt-pro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 913    893    12206153728 7.89 4.34 319516672 1 .144 0.015 6.84 3.85 321060864 .451 .055 .188 .074 .031 .010 .027 .005 .00  .005 6.79 3.80 275066880 0 .037 .041 .204 .094 .027 .006 .025 .003 .001 .004 .00 
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-em-terratec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 914    893    12081192960 7.60 4.17 315260928 1 0.014