Tool CPAchecker 1.5-svn 20406
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 4
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-35-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-04-28 23:19:27 CEST
Run set NONE LENGTH_MIN LENGTH_MAX DOMAIN_MIN DOMAIN_MAX WIDTH_MIN WIDTH_MAX PIVOT_MIN PIVOT_MAX RANDOM DOMAIN_MIN,WIDTH_MIN WIDTH_MIN,DOMAIN_MIN
Options -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=NONE -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=LENGTH_MIN -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=DOMAIN_MIN,LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=DOMAIN_MAX,LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=WIDTH_MIN,LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=WIDTH_MAX,LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=PIVOT_MIN,LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=PIVOT_MAX,LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=RANDOM -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=DOMAIN_MIN,WIDTH_MIN,LENGTH_MAX -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -skipRecursion -setprop analysis.checkCounterexamples=false -predicateAnalysis-PredAbsRefiner-SBE -setprop cpa.predicate.refinement.performInitialStaticRefinement=false -setprop cpa.predicate.refinement.restartAfterRefinements=1 -setprop cpa.predicate.precision.sharing=GLOBAL -setprop cpa.predicate.refinement.prefixPreference=WIDTH_MIN,DOMAIN_MIN,LENGTH_MAX
test/programs/benchmarks/ status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s)
bitvector/byte_add_false-unreach-call.i 14.9  16.5  20.3  23.5  20.1  15.1  15.9  20.2  22.5  20.8  17.9  16.0 
bitvector/byte_add_1_true-unreach-call.i 15.6  15.7  19.2  18.9  21.1  19.1  14.4  28.6  20.2  21.0  17.4  16.7 
bitvector/byte_add_2_true-unreach-call.i 15.5  16.1  22.5  28.4  19.5  20.5  15.0  22.1  20.2  16.9  27.9  20.1 
bitvector/gcd_1_true-unreach-call.i 901    901    901    901    901    902    901    901    901    902    901    901   
bitvector/gcd_2_true-unreach-call.i 10.9  10.4  10.8  10.1  12.0  11.8  12.2  11.1  11.0  11.9  11.9  12.4 
bitvector/gcd_3_true-unreach-call.i 4.58 4.66 4.66 4.39 4.78 4.52 4.67 4.68 4.48 4.68 4.70 4.56
bitvector/gcd_4_true-unreach-call.i 14.9  16.1  15.2  15.9  15.4  16.0  13.8  15.3  13.2  19.5  15.5  16.2 
bitvector/interleave_bits_true-unreach-call.i 19.7  19.8  20.7  21.7  19.1  21.0  21.2  19.6  18.9  21.0  26.7  19.2 
bitvector/jain_1_true-unreach-call.i 901    901    901    901    901    901    901    902    901    902    902    901   
bitvector/jain_2_true-unreach-call.i 4.64 4.70 4.33 4.44 4.49 5.05 4.36 4.61 4.63 4.76 4.25 4.58
bitvector/jain_4_true-unreach-call.i 4.98 4.67 4.90 4.65 5.04 5.03 4.97 4.61 4.89 5.10 4.88 5.04
bitvector/jain_5_true-unreach-call.i 902    902    906    901    901    901    901    901    902    901    901    901   
bitvector/jain_6_true-unreach-call.i 4.91 4.75 5.19 4.82 5.21 5.45 4.98 4.89 5.12 4.83 4.93 5.08
bitvector/jain_7_true-unreach-call.i 4.77 4.97 4.75 4.97 4.91 4.85 4.82 5.15 4.72 4.70 4.91 5.10
bitvector/modulus_true-unreach-call.i 3.74 3.97 3.89 4.01 4.05 4.17 3.81 3.97 4.16 4.02 4.09 3.87
bitvector/num_conversion_1_true-unreach-call.i 9.21 9.77 9.08 9.90 9.85 10.1  9.63 9.98 9.96 9.92 9.45 9.58
bitvector/num_conversion_2_true-unreach-call.i 9.71 10.4  9.93 9.06 10.0  9.92 9.79 10.0  9.27 9.74 9.75 9.64
bitvector/parity_true-unreach-call.i 3.53 3.91 3.89 3.85 3.92 4.02 3.80 3.99 4.23 3.95 3.71 3.94
bitvector/sum02_true-unreach-call.i 5.94 6.12 6.18 6.29 6.08 6.01 6.26 6.00 6.17 5.84 6.32 6.02
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c 69.3  94.0  483    118    785    87.0  108    95.1  324    223    93.4  90.4 
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c 76.9  82.9  215    79.3  902    86.4  955    902    222    245    95.2  83.5 
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c 14.6  15.9  25.2  24.4  24.6  15.8  25.3  24.3  26.3  19.9  16.0  15.5 
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c 72.8  94.0  902    118    782    91.4  106    87.5  349    103    88.8  95.1 
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c 83.3  81.9  231    91.1  902    91.0  902    901    228    242    102    91.0 
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c 74.3  92.2  902    134    903    82.6  226    167    94.1  280    99.0  86.9 
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c 901    901    901    901    901    901    902    901    902    901    901    901   
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c 77.3  118    95.8  86.2  117    76.4  189    111    109    123    114    73.7 
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c 78.4  901    901    902    901    901    902    901    902    64.9  902    901   
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c 75.6  902    902    901    901    902    901    901    901    79.8  901    901   
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c 83.5  94.4  62.5  78.6  103    93.1  217    126    91.5  109    120    88.6 
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c 82.5  109    57.7  69.9  96.8  91.8  184    153    118    67.1  116    90.5 
bitvector/soft_float_1_true-unreach-call.c.cil.c 27.1  36.0  45.8  44.8  42.7  37.7  42.1  30.4  42.6  47.5  41.1  39.7 
bitvector/soft_float_2_true-unreach-call.c.cil.c 7.39 9.00 9.06 9.56 9.19 10.3  9.35 10.5  9.11 9.52 9.69 9.48
bitvector/soft_float_3_true-unreach-call.c.cil.c 7.75 9.19 8.63 9.02 9.01 9.07 9.46 10.7  8.85 11.1  9.69 9.08
bitvector/soft_float_4_true-unreach-call.c.cil.c 901    902    901    901    901    902    902    902    901    901    901    901   
bitvector/soft_float_5_true-unreach-call.c.cil.c 10.5  14.8  14.0  15.7  12.6  13.6  13.3  15.6  13.9  16.5  14.5  14.5 
bitvector-regression/implicitfloatconversion_false-unreach-call.i 3.55 3.75 4.06 3.72 3.72 3.49 3.74 3.71 4.17 3.87 3.67 3.92
bitvector-regression/implicitunsignedconversion_false-unreach-call.i 3.82 3.84 3.70 3.93 3.78 3.63 4.14 3.84 3.63 3.45 3.62 3.76
bitvector-regression/integerpromotion_false-unreach-call.i 4.10 4.19 4.08 4.04 4.31 4.15 4.13 4.29 4.09 3.97 4.27 4.41
bitvector-regression/signextension2_false-unreach-call.i 4.18 4.05 4.04 4.24 4.27 4.24 4.20 4.19 4.37 4.38 4.14 4.35
bitvector-regression/signextension_false-unreach-call.i 4.09 4.30 4.39 4.31 4.21 4.10 4.42 4.57 4.40 4.36 4.23 4.10
bitvector-regression/implicitunsignedconversion_true-unreach-call.i 3.75 3.60 3.76 3.80 3.78 3.60 3.66 3.58 3.86 3.77 3.93 3.84
bitvector-regression/integerpromotion_true-unreach-call.i 4.21 4.31 4.14 4.37 4.25 3.96 4.48 4.00 4.35 4.46 4.06 4.94
bitvector-regression/signextension2_true-unreach-call.i 4.56 4.37 4.32 4.60 4.59 4.17 4.33 4.30 4.62 4.28 4.57 4.40
bitvector-regression/signextension_true-unreach-call.i 4.34 4.10 4.08 4.34 4.01 4.12 4.34 4.04 4.24 4.37 4.55 4.55
bitvector-loops/diamond_false-unreach-call2.i 55.2  55.5  366    66.7  372    61.0  73.6  70.8  77.6  69.9  54.3  61.6 
bitvector-loops/overflow_false-unreach-call1.i 3.79 3.93 3.90 3.78 3.73 3.50 3.61 4.08 3.98 3.99 3.96 3.59
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 18.3  22.2  4.26 4.54 4.30 6.01 4.61 23.9  4.36 4.54 5.73 5.21
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c 116    124    120    126    150    106    105    130    146    118    118    116   
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c 53.5  56.3  64.3  76.1  59.0  50.2  56.0  54.8  63.5  60.3  60.6  58.0 
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c 55.3  58.3  70.3  73.6  56.9  52.2  57.1  61.1  73.3  63.8  60.7  52.6 
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c 35.3  41.7  52.4  41.7  76.2  36.4  65.9  64.8  41.9  38.7  32.8  35.3 
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c 564    592    553    718    626    561    540    719    449    704    625    427   
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c 903    902    902    901    902    901    902    902    902    902    901    901   
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c 194    196    257    334    172    166    168    175    307    217    243    193   
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c 498    325    454    711    320    369    325    329    579    444    617    365   
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c 34.2  35.5  42.1  36.2  34.5  33.4  50.1  36.4  37.1  36.2  40.7  34.3 
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c 42.1  39.5  42.4  51.0  43.2  38.0  59.4  47.2  40.1  46.3  43.7  39.9 
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 76.0  79.2  109    116    116    75.9  87.3  88.7  89.6  71.9  91.1  79.0 
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 102    91.3  901    116    901    88.1  902    901    86.1  125    101    95.7 
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 99.4  95.1  901    119    901    94.8  901    902    87.9  114    101    90.0 
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 96.5  90.2  902    122    901    99.9  901    901    91.2  104    92.7  82.0 
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 396    196    901    901    901    901    365    218    901    324    901    901   
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 202    123    902    901    901    901    93.3  146    902    101    901    902   
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 212    161    102    124    107    902    111    197    128    94.4  901    901   
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 178    122    447    206    901    902    99.4  146    219    153    125    901   
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 901    213    400    278    902    902    650    251    431    305    351    901   
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 34.0  33.7  121    50.6  901    47.3  52.6  42.3  87.8  52.2  43.3  47.1 
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 37.3  36.0  126    54.3  901    52.0  53.2  42.4  95.4  62.9  48.6  48.4 
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 156    321    630    529    902    394    902    901    756    430    441    406   
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 92.5  103    106    133    152    130    204    123    88.8  158    115    141   
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 82.7  122    268    149    901    151    901    902    88.5  155    136    149   
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 85.4  112    131    155    901    140    901    901    96.3  102    117    143   
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 86.4  115    902    120    901    139    189    901    92.9  175    112    144   
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 78.0  127    901    107    902    901    161    108    901    151    136    902   
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c 21.6  21.4  23.2  20.1  24.4  24.5  19.7  23.3  24.2  23.6  20.5  25.3 
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 8.64 8.94 12.4  8.80 13.9  11.9  9.35 11.2  12.7  12.0  9.00 10.7 
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 91.6  115    902    902    902    71.1  111    116    902    75.5  902    62.3 
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 80.2  123    901    95.5  901    89.2  204    156    901    141    108    125   
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 67.2  106    901    78.3  901    101    264    109    901    101    89.5  97.4 
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 108    289    526    522    901    474    902    901    719    319    346    387   
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 110    178    901    124    902    160    150    901    901    222    141    169   
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 83.6  120    901    141    902    148    301    141    117    112    176    144   
locks/test_locks_14_false-unreach-call.c 4.08 4.21 4.53 4.49 4.26 4.13 4.31 4.27 4.62 3.95 4.06 4.31
locks/test_locks_15_false-unreach-call.c 4.14 4.40 4.39 4.25 4.38 4.39 4.15 4.52 4.59 4.47 4.51 4.40
locks/test_locks_10_true-unreach-call.c 174    190    188    205    218    230    159    189    210    178    201    216   
locks/test_locks_11_true-unreach-call_false-termination.c 625    611    669    504    567    620    757    736    730    902    687    661   
locks/test_locks_12_true-unreach-call_false-termination.c 902    902    901    902    902    902    902    902    902    902    902    902   
locks/test_locks_13_true-unreach-call.c 902    902    903    902    902    902    902    903    902    902    902    902   
locks/test_locks_14_true-unreach-call.c 902    902    902    902    902    902    902    902    902    904    904    902   
locks/test_locks_15_true-unreach-call_false-termination.c 902    903    903    902    902    902    902    902    902    902    902    903   
locks/test_locks_5_true-unreach-call_false-termination.c 15.1  15.6  15.9  16.3  15.9  15.7  15.6  16.4  15.4  17.2  15.5  16.6 
locks/test_locks_6_true-unreach-call_false-termination.c 21.7  23.3  24.1  25.3  22.8  23.0  22.6  22.0  22.8  24.3  24.3  22.1 
locks/test_locks_7_true-unreach-call_false-termination.c 35.7  33.6  34.6  36.2  34.4  35.2  36.3  35.3  32.8  33.8  34.3  33.6 
locks/test_locks_8_true-unreach-call_false-termination.c 47.7  48.1  45.6  46.8  39.4  48.0  48.2  51.8  44.8  48.9  48.7  46.4 
locks/test_locks_9_true-unreach-call.c 93.0  79.7  79.3  85.4  73.0  77.1  84.2  77.0  83.4  89.6  77.5  124   
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i 38.2  38.8  43.5  41.3  43.2  39.4  42.6  44.6  42.7  43.1  40.9  41.2 
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i 77.1  74.4  106    88.3  98.7  78.7  89.4  86.2  85.9  103    84.8  86.1 
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i 38.6  65.8  69.9  69.7  72.5  66.0  63.1  64.3  74.0  70.9  74.9  65.9 
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i 43.1  51.7  51.4  45.9  51.1  47.6  57.4  49.6  44.3  47.4  48.0  46.2 
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i 902    901    901    901    902    901    901    901    901    901    902    901   
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i 71.8  73.1  905    91.0  902    902    903    901    901    80.8  98.9  901   
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i 247    208    455    508    250    321    713    321    553    902    204    353   
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i 902    904    902    943    902    903    903    903    903    905    903    902   
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i 51.6  52.7  57.6  56.3  55.2  51.8  56.8  49.6  46.5  61.5  53.9  47.2 
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i 66.7  75.0  68.4  74.3  69.2  71.6  68.7  72.0  69.1  68.7  68.9  73.1 
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i 349    378    327    855    439    370    901    366    385    832    459    368   
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i 56.8  76.2  234    175    85.1  53.5  96.8  94.3  83.4  138    155    56.0 
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i 79.4  78.0  131    117    91.4  85.5  105    76.1  83.1  95.0  117    87.2 
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i 215    221    171    189    350    156    254    232    160    276    178    156   
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i 43.6  53.5  54.8  55.6  53.2  46.4  56.0  54.8  43.7  52.9  50.7  45.9 
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i 42.2  43.6  43.1  40.6  48.1  44.6  42.6  41.8  48.0  46.8  41.2  44.6 
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i 43.4  45.3  39.7  44.7  47.8  40.2  41.4  44.0  42.8  41.8  42.8  43.7 
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i 60.3  73.7  40.5  52.5  902    75.6  41.3  39.3  97.5  539    73.6  81.0 
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i 53.1  62.8  29.6  32.9  87.2  62.8  29.4  32.9  86.2  30.6  47.2  63.9 
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i 19.2  17.4  16.8  18.5  18.8  19.4  17.9  18.9  17.6  18.4  18.6  16.6 
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i 200    216    20.9  35.6  21.0  200    21.2  20.2  239    43.3  247    217   
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i 55.1  55.2  54.4  54.0  64.6  55.6  56.1  57.2  59.6  55.5  58.1  54.4 
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i 9.40 9.42 9.45 9.36 9.39 9.90 9.66 9.41 9.13 9.48 9.04 9.22
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i 19.2  38.2  17.8  17.9  38.0  37.4  16.1  16.5  34.7  38.9  21.0  35.0 
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i 33.5  32.4  32.0  29.6  33.9  32.0  32.7  29.6  29.5  31.0  32.4  34.4 
ldv-linux-3.0/module_get_put-drivers-net-pppox.ko_true-unreach-call.cil.out.i.pp.i 11.7  13.5  12.1  12.4  13.5  13.0  13.3  12.8  13.0  12.5  13.4  12.2 
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i 30.1  33.5  33.7  32.9  32.2  33.3  32.0  32.7  35.4  31.9  32.3  34.4 
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i 47.2  45.8  43.0  44.9  46.4  45.3  44.1  44.7  44.1  41.7  43.6  48.2 
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i 37.2  38.4  38.2  40.0  39.5  38.2  35.8  39.8  38.6  36.9  39.3  34.4 
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i 47.0  45.5  46.0  42.6  44.0  44.1  44.4  48.1  46.3  45.6  48.5  44.1 
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i 36.7  37.9  36.3  40.4  35.0  38.3  41.2  40.9  39.4  38.1  36.7  40.9 
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i 43.3  39.7  41.5  35.5  36.1  38.6  43.7  42.2  38.6  37.3  36.0  40.7 
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i 38.5  39.1  38.7  42.9  43.6  44.5  40.0  42.1  41.3  44.9  44.3  38.0 
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i 40.4  38.6  25.7  26.8  23.2  41.0  24.1  24.9  39.1  36.8  39.6  40.7 
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i 52.7  50.0  50.9  53.6  53.2  53.6  51.8  52.1  50.8  50.1  52.1  50.7 
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i 48.5  46.5  45.8  45.4  47.0  47.7  49.6  43.7  50.0  50.4  46.1  47.2 
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i 97.4  89.3  57.0  127    53.4  135    129    117    60.0  122    286    147   
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i 69.5  64.5  89.5  87.2  487    77.1  387    65.9  62.0  64.1  78.6  76.0 
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i 674    494    903    99.6  903    496    903    596    902    902    108    475   
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i 43.2  40.9  42.2  39.7  44.2  39.5  43.3  39.9  42.1  41.2  42.5  39.7 
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i 31.1  27.8  27.9  29.7  30.9  28.8  28.7  29.9  29.9  27.8  29.5  30.6 
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 72.5  77.0  69.0  73.6  86.7  76.0  68.7  73.4  78.2  78.6  71.4  74.5 
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 52.1  69.1  48.8  98.0  69.8  66.5  50.2  63.6  99.3  65.8  82.4  68.1 
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 85.4  235    902    162    283    182    193    299    185    208    157    174   
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 23.8  24.5  23.3  24.3  26.4  26.1  24.2  25.0  24.8  24.5  25.4  26.8 
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 50.0  87.2  344    46.5  83.8  107    467    43.1  46.3  62.9  46.7  101   
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 62.2  63.2  58.7  61.1  65.3  59.6  61.0  65.3  58.5  63.6  63.1  61.2 
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 17.1  16.0  16.3  15.8  15.6  17.7  16.7  17.8  15.8  17.3  17.5  17.5 
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 35.6  35.3  28.4  25.6  37.6  37.6  24.6  27.1  34.9  37.2  27.4  37.5 
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 44.7  51.7  53.3  61.8  48.6  51.9  58.5  55.8  51.0  53.9  59.1  49.7 
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 55.5  61.1  55.2  50.9  55.5  57.5  50.9  63.9  52.2  64.0  51.6  58.7 
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 60.7  97.2  44.3  44.2  93.2  98.2  39.3  44.4  96.1  66.5  46.9  93.0 
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 41.9  43.7  52.8  43.2  50.8  53.7  42.4  40.5  42.9  40.1  40.0  43.8 
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 29.9  24.9  29.8  27.6  27.9  28.8  28.9  27.3  28.9  28.2  30.9  28.6 
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 10.6  10.5  10.4  10.5  10.3  10.5  11.2  10.1  10.7  10.4  10.7  10.6 
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 22.6  21.1  22.5  22.6  22.6  22.6  22.1  20.8  21.7  23.6  22.6  22.8 
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 40.9  46.0  44.8  45.9  45.2  47.5  45.6  44.8  41.2  45.3  42.2  42.5 
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 760    867    902    902    902    903    902    803    902    902    902    902   
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 902    902    72.7  79.0  901    902    77.7  80.3  77.6  89.5  903    902   
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 902    902    907    902    901    902    902    902    905    902    901    902   
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 902    902    902    902    902    903    902    902    943    902    902    902   
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 70.2  87.1  66.8  87.6  67.7  71.2  86.7  87.4  65.2  68.3  86.9  69.8 
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 128    902    151    143    902    126    902    901    148    904    148    123   
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 258    734    120    108    876    791    117    257    473    134    116    764   
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 8.99 8.81 8.98 9.25 9.47 8.94 9.12 9.45 8.79 8.60 8.97 9.05
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 6.77 7.06 6.60 7.01 6.94 6.68 6.83 6.71 7.11 6.93 6.69 6.80
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 8.46 8.93 7.23 7.14 8.66 8.55 7.23 7.21 8.50 7.09 6.81 8.50
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 11.8  13.1  7.56 8.50 13.1  14.6  7.43 7.74 13.4  12.8  8.51 13.0 
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 7.71 11.4  7.79 7.93 11.6  11.8  7.84 7.60 10.7  11.3  8.26 11.7 
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 7.88 7.84 8.44 7.41 8.35 8.49 8.13 7.74 8.23 8.15 8.17 7.90
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 8.00 7.87 7.03 7.52 8.02 8.01 7.53 7.96 8.04 6.78 7.71 7.70
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 9.79 17.2  9.17 9.02 9.44 14.7  8.95 10.0  15.4  15.2  11.3  15.3 
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 45.4  901    12.5  13.2  902    902    13.7  902    902    25.1  12.2  902   
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 7.80 7.21 7.15 7.58 7.05 7.43 7.22 7.02 7.09 7.04 7.10 7.21
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 6.74 7.00 6.19 6.58 7.01 6.15 6.83 6.34 7.00 6.66 6.91 7.03
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 9.67 10.3  10.4  10.5  10.3  10.4  10.5  10.0  10.8  9.74 10.1  10.5 
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 49.8  51.5  51.8  49.5  49.5  49.8  49.6  47.4  49.2  51.2  48.6  48.1 
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 15.1  13.7  14.6  14.2  13.7  14.2  13.4  14.8  14.6  14.4  15.3  14.4 
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 17.9  18.7  19.1  18.1  18.5  17.5  18.2  17.2  18.5  19.2  17.9  18.2 
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 46.0  45.4  43.5  45.1  41.9  44.0  45.6  44.7  43.1  43.0  45.8  42.9 
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 24.8  23.0  24.7  21.7  22.0  23.4  22.7  23.2  23.3  25.0  22.6  22.0 
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 9.60 9.87 9.57 9.27 9.53 9.37 9.07 9.37 9.54 9.72 9.25 9.45
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 12.9  13.4  12.3  13.4  14.1  13.6  12.5  12.9  13.2  12.8  12.7  13.2 
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 31.0  30.7  31.5  29.9  31.3  30.1  29.8  30.7  30.1  31.9  30.5  30.9 
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 26.7  27.6  25.8  25.2  27.6  25.5  25.9  27.2  25.2  27.1  26.7  28.8 
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 23.8  25.2  23.8  24.9  24.3  24.8  23.5  24.3  22.8  24.6  23.2  23.1 
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 9.76 9.78 9.89 9.63 9.57 9.95 9.92 10.0  9.18 9.90 9.72 9.66
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 21.1  21.8  21.9  18.9  20.1  21.9  20.6  19.6  23.7  20.8  21.4  22.1 
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 54.7  50.9  51.2  49.0  51.1  50.2  50.8  52.9  52.6  50.0  54.6  53.3 
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 6.89 7.13 6.98 6.96 6.53 6.94 6.93 6.66 7.08 6.84 6.90 7.05
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 8.79 8.81 9.56 9.40 8.75 8.52 9.78 8.73 8.52 8.73 8.83 9.07
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 6.99 6.73 6.52 6.53 6.22 7.05 6.29 6.61 6.61 6.42 6.81 7.14
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 10.9  11.4  10.6  10.9  11.2  11.0  11.2  11.1  10.5  10.9  10.8  11.3 
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 7.69 7.83 8.45 7.86 8.52 8.35 8.30 8.55 8.28 8.43 7.94 7.91
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 6.17 6.29 6.24 6.08 6.18 6.19 6.25 5.98 5.81 6.42 5.99 6.36
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 4.60 4.57 4.80 4.52 5.22 4.75 4.50 4.70 4.88 5.01 4.71 4.80
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 11.7  11.9  10.8  11.5  12.0  13.3  11.5  10.7  11.2  10.7  10.3  12.1 
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 8.78 9.12 6.16 6.48 8.94 9.85 6.63 6.12 17.5  6.50 6.48 9.60
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 29.3  28.7  15.6  15.6  20.3  31.3  16.8  17.8  21.6  16.7  16.7  30.7 
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 7.31 7.46 6.25 6.52 7.40 7.58 7.03 6.57 7.10 7.84 7.16 7.74
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 6.98 7.09 6.69 6.89 7.45 7.13 7.07 7.23 6.92 7.19 7.40 7.13
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 6.37 6.19 6.56 6.91 6.15 6.83 6.75 6.60 6.91 6.60 6.77 6.77
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 7.30 7.22 7.32 7.85 7.48 7.44 7.06 7.25 7.16 7.60 7.59 7.36
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 6.85 6.58 6.56 6.85 6.82 6.65 6.87 6.55 6.99 6.23 6.20 6.47
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 9.32 8.18 8.23 7.58 8.14 8.45 8.28 8.61 7.94 8.27 7.87 8.28
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 7.89 7.53 7.93 7.56 7.63 7.15 7.71 7.52 7.81 7.15 7.71 7.75
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 11.8  12.2  11.9  11.8  11.7  11.6  11.2  12.2  12.6  11.7  12.2  11.3 
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 6.32 5.57 5.87 6.17 6.20 5.88 5.81 6.54 5.81 5.74 6.04 5.74
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 6.30 6.70 5.60 6.54 6.54 6.94 6.62 5.68 6.31 6.67 6.56 6.34
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 6.76 6.80 7.05 6.70 6.90 7.04 6.37 7.08 6.95 6.92 6.63 6.82
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 8.50 8.57 8.02 8.01 8.77 8.76 8.63 8.65 8.51 8.59 8.41 8.76
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 5.55 5.31 5.60 5.31 5.34 5.13 6.00 5.32 5.57 5.79 5.41 5.12
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 6.49 6.69 6.73 6.79 6.74 6.87 6.98 9.90 6.53 6.62 6.78 6.91
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 8.46 8.52 8.71 8.61 8.64 8.37 8.38 8.79 8.47 8.47 8.06 8.34
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 6.72 6.09 7.23 6.58 6.01 6.27 6.58 6.82 7.14 6.83 6.16 6.36
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 5.34 5.63 5.09 5.79 5.26 5.38 5.51 5.53 5.18 5.46 5.45 5.42
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 7.78 7.57 7.80 7.40 7.42 7.87 7.61 7.16 7.64 7.66 7.65 7.22
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 6.69 7.12 7.18 6.66 7.11 6.80 7.00 7.13 7.10 7.23 7.11 7.08
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 5.62 5.65 6.65 6.39 6.07 5.35 6.45 6.02 5.49 5.46 6.84 6.20
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 8.05 8.41 8.12 8.02 8.45 8.01 8.09 8.19 8.29 8.03 8.54 7.92
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 6.88 6.50 6.89 7.20 6.84 6.82 6.73 6.56 6.71 6.92 6.95 6.75
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 5.60 6.12 6.52 5.89 6.38 6.45 6.38 6.89 6.52 6.12 6.31 6.12
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 9.40 9.53 9.17 10.2  9.49 9.45 9.67 9.65 9.34 9.48 9.61 10.2 
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 5.78 6.66 5.98 5.84 5.87 6.43 7.09 5.61 5.64 6.60 6.63 6.52
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 6.96 6.83 6.90 6.89 6.87 6.68 6.81 7.16 6.57 6.48 6.02 7.36
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 7.30 7.29 7.09 7.49 6.99 7.12 7.33 7.22 7.61 7.60 6.92 6.91
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 8.30 8.38 8.68 8.77 8.62 8.61 8.98 8.65 8.97 8.55 7.85 8.88
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 9.83 9.08 9.68 10.1  9.76 9.50 9.57 9.52 9.61 9.44 9.72 9.69
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 6.93 6.19 6.96 6.66 6.23 6.41 6.67 6.57 6.57 6.68 6.59 6.67
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 13.1  13.2  13.0  13.1  12.9  14.2  12.9  14.8  13.1  13.5  13.6  14.2 
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 7.80 8.08 7.70 7.07 7.76 8.37 7.37 7.80 7.79 7.73 7.85 7.64
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 9.65 9.48 9.96 9.28 9.39 9.52 11.9  9.55 9.41 9.16 9.65 9.53
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 9.06 10.1  9.52 9.85 9.98 9.20 10.0  9.68 9.58 9.53 9.05 9.81
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 24.2  22.2  23.9  24.7  24.1  23.9  24.4  24.5  22.9  25.1  26.6  24.3 
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 8.91 8.96 8.11 7.54 9.17 9.03 7.80 7.84 8.92 9.45 8.15 8.86
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 9.30 9.84 8.89 9.42 9.49 9.65 9.53 9.98 9.55 9.39 9.80 8.99
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 8.61 9.19 8.04 7.95 8.62 9.43 7.97 8.24 9.35 9.28 8.21 8.88
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 7.41 7.87 8.00 7.55 7.60 7.54 7.27 7.58 7.50 7.51 7.89 7.62
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 6.93 6.32 6.65 6.40 6.08 6.54 6.76 6.33 7.06 6.61 6.43 6.62
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 6.56 6.56 7.31 7.18 6.83 7.20 6.91 6.93 7.67 6.71 7.05 7.04
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 9.93 9.95 9.36 8.41 9.95 10.1  8.66 8.73 10.6  8.43 8.71 9.76
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 18.3  18.2  17.7  16.2  19.2  17.8  18.3  18.3  19.3  18.4  19.9  20.2 
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 33.5  59.9  19.7  18.9  59.8  60.5  20.1  20.1  58.7  19.5  22.1  62.3 
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 10.9  38.2  7.80 8.99 36.9  38.0  8.72 9.12 40.3  21.6  9.15 36.1 
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 10.1  11.8  9.54 9.33 11.4  12.0  9.78 9.86 10.8  10.4  9.55 10.8 
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 7.22 7.65 7.74 8.52 7.22 7.47 7.12 7.51 7.24 7.70 7.45 7.55
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 51.1  76.0  27.3  30.9  74.3  78.1  29.6  28.4  78.1  59.3  30.2  66.9 
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 7.45 7.54 7.61 7.42 8.01 8.10 8.55 7.91 7.63 7.72 7.75 7.81
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 15.4  17.5  8.16 8.63 19.2  32.1  8.37 7.94 44.4  17.7  8.41 32.6 
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 7.95 7.65 7.83 7.67 7.79 7.87 7.73 8.22 7.63 7.87 8.20 7.81
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 8.83 8.59 9.10 8.74 8.98 8.80 9.33 7.92 8.74 8.62 9.26 8.95
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 8.31 8.89 8.80 8.39 8.65 8.64 8.72 8.14 8.47 8.96 8.78 8.59
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 7.69 7.37 7.58 8.12 7.46 7.81 7.59 7.77 7.52 7.49 7.32 7.65
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 13.3  12.2  9.22 8.60 13.1  13.5  9.62 9.02 54.8  12.4  9.15 12.7 
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 7.68 7.61 7.74 7.44 7.67 7.62 7.89 7.86 7.65 7.86 7.42 7.74
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 8.03 8.60 8.19 8.65 8.77 8.61 8.70 9.30 8.81 8.42 9.10 8.94
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 7.41 7.41 6.99 6.97 6.96 7.02 7.21 7.22 7.68 7.30 7.29 7.08
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 8.41