Tool CPAchecker 1.5-svn 20406
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
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-34-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-03-24 21:58:48 CET
Run set valueAnalysis-Cegar valueAnalysis-Cegar-ItpDeepestInfeasibleSuffix valueAnalysis-Cegar-ItpEquality valueAnalysis-Cegar-ItpEquivalence valueAnalysis-Cegar-ItpAllOptimizations valueAnalysis-Cegar valueAnalysis-Cegar-ItpDeepestInfeasibleSuffix valueAnalysis-Cegar-ItpEquality valueAnalysis-Cegar-ItpEquivalence valueAnalysis-Cegar-ItpAllOptimizations
Options -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=false -setprop cpa.value.interpolation.applyRenamingOptimization=false -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=false -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=false -setprop cpa.value.interpolation.applyRenamingOptimization=false -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=true -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=true -setprop cpa.value.interpolation.applyRenamingOptimization=false -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=false -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=false -setprop cpa.value.interpolation.applyRenamingOptimization=true -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=false -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=true -setprop cpa.value.interpolation.applyRenamingOptimization=true -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=true -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=false -setprop cpa.value.interpolation.applyRenamingOptimization=false -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=false -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=false -setprop cpa.value.interpolation.applyRenamingOptimization=false -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=true -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=true -setprop cpa.value.interpolation.applyRenamingOptimization=false -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=false -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=false -setprop cpa.value.interpolation.applyRenamingOptimization=true -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=false -heap 12500M -disable-java-assertions -noout -setprop log.consoleLevel=WARNING -valueAnalysis-Cegar -setprop cpa.value.interpolation.manageCallstack=false -setprop cpa.value.interpolation.applyItpEqualityOptimization=true -setprop cpa.value.interpolation.applyRenamingOptimization=true -setprop cpa.value.interpolation.applyUnsatSuffixOptimization=true
test/programs/benchmarks/ status cputime (s) status cputime (s) status cputime (s) status cputime (s) status cputime (s) itpTime (s) #itps #queries size itpTime (s) #itps #queries size itpTime (s) #itps #queries size itpTime (s) #itps #queries size itpTime (s) #itps #queries size
bitvector/byte_add_false-unreach-call.i 6.97 8.77 7.51 8.46 7.27 .152 25 516 367 .173 25 515 367 .121 25 298 367 .190 25 516 367 .121 25 297 367
bitvector/byte_add_1_true-unreach-call.i 13.8  13.4  10.6  13.7  10.9  .423 47 1559 1108 .406 47 1548 1108 .238 47 786 1108 .434 47 1559 1108 .224 47 775 1108
bitvector/byte_add_2_true-unreach-call.i 14.2  14.7  11.9  14.5  12.0  .439 49 1645 1155 .430 49 1634 1155 .257 49 851 1155 .473 49 1645 1155 .247 49 840 1155
bitvector/gcd_1_true-unreach-call.i 3.73 3.51 3.66 3.61 3.65 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/gcd_2_true-unreach-call.i 3.45 3.47 3.66 3.18 2.97 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/gcd_3_true-unreach-call.i 3.51 3.78 3.53 3.51 3.56 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/gcd_4_true-unreach-call.i 4.38 5.30 4.69 5.02 3.75 .145 9 378 348 .177 9 387 348 .072 9 116 348 .161 9 367 348 .061 9 118 348
bitvector/interleave_bits_true-unreach-call.i 3.82 3.89 3.85 3.83 3.85 .008 2 6 4 .009 2 8 4 .008 2 5 4 .006 2 6 4 .009 2 7 4
bitvector/jain_1_true-unreach-call.i 2.99 3.42 3.43 3.51 3.51 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/jain_2_true-unreach-call.i 3.55 3.46 3.43 3.46 3.42 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/jain_4_true-unreach-call.i 3.78 3.69 3.67 3.46 3.64 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/jain_5_true-unreach-call.i 902    903    902    903    903    .022 2 29 24 .021 2 31 24 .015 2 17 24 .018 2 27 24 .017 2 19 24
bitvector/jain_6_true-unreach-call.i 3.47 3.56 3.61 3.05 3.53 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/jain_7_true-unreach-call.i 3.64 3.59 3.03 3.32 3.50 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/modulus_true-unreach-call.i 3.51 3.64 3.62 3.64 2.83 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/num_conversion_1_true-unreach-call.i 5.05 4.94 4.96 5.02 4.78 .163 6 276 210 .170 6 282 210 .131 6 198 210 .161 6 276 210 .127 6 204 210
bitvector/num_conversion_2_true-unreach-call.i 3.89 3.81 3.88 3.87 3.89 .014 3 18 12 .018 3 21 12 .017 3 14 12 .013 3 18 12 .013 3 17 12
bitvector/parity_true-unreach-call.i 3.07 3.52 3.58 3.11 3.56 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector/sum02_true-unreach-call.i 3.22 3.65 3.20 3.68 3.69 .017 3 24 19 .017 3 24 19 .013 3 13 19 .022 3 24 19 .014 3 13 19
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c 18.1  20.4  17.5  19.1  18.9  1.26  72 5835 2565 1.12  72 5228 2565 .969 72 3798 2565 1.28  72 5835 2565 .861 72 3191 2565
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c 19.3  19.9  19.8  19.5  19.0  1.56  84 7654 3757 1.37  84 7113 3757 1.18  84 4658 3757 1.45  84 7654 3757 1.03  84 4117 3757
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c 18.5  18.2  17.4  18.8  17.7  1.12  64 5589 3410 1.06  64 5252 3410 .790 64 3098 3410 1.15  64 5589 3410 .670 64 2761 3410
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c 28.8  25.7  25.7  28.4  25.2  4.22  168 20647 11842 4.00  168 19300 11842 2.36  168 11746 11842 4.18  168 20647 11842 2.23  168 10399 11842
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c 24.4  22.9  20.8  20.9  21.8  2.63  154 15244 6490 2.32  154 13954 6490 1.72  154 10230 6490 2.54  154 15244 6490 1.64  154 8940 6490
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c 21.0  22.4  21.2  19.9  19.6  1.91  142 12771 7345 1.82  142 11900 7345 1.32  142 7277 7345 1.84  142 12771 7345 1.16  142 6406 7345
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c 33.3  32.4  28.2  34.1  28.6  7.85  174 25947 20523 7.46  174 25511 20523 2.30  174 8510 20523 7.67  174 25947 20523 2.42  174 8074 20523
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c 24.5  23.4  23.6  22.6  23.8  4.93  142 18962 15087 4.55  142 18708 15087 1.60  142 6245 15087 4.47  142 18962 15087 1.58  142 5991 15087
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c 20.3  19.4  20.2  21.3  20.9  2.48  120 12721 10004 2.41  120 12559 10004 1.07  120 4354 10004 2.46  120 12721 10004 1.02  120 4192 10004
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c 22.3  20.3  22.8  21.9  21.7  2.69  134 14031 10815 2.57  134 13812 10815 1.12  134 5068 10815 2.66  134 14031 10815 1.09  134 4849 10815
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c 25.3  25.6  24.0  25.3  24.6  4.73  143 18950 15068 4.60  143 18717 15068 1.64  143 6315 15068 4.81  143 18950 15068 1.57  143 6082 15068
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c 25.7  25.5  24.2  25.2  23.8  4.68  142 18891 15020 4.61  142 18662 15020 1.61  142 6291 15020 4.53  142 18891 15020 1.55  142 6062 15020
bitvector/soft_float_1_true-unreach-call.c.cil.c 7.66 7.32 6.42 7.17 6.31 .244 12 679 588 .231 12 669 588 .147 12 244 588 .233 12 634 588 .110 12 203 588
bitvector/soft_float_2_true-unreach-call.c.cil.c 12.5  11.7  9.60 11.5  9.67 .658 14 1255 1147 .664 14 1241 1147 .187 14 237 1147 .671 14 1213 1147 .183 14 196 1147
bitvector/soft_float_3_true-unreach-call.c.cil.c 7.04 7.10 6.05 7.04 4.90 .175 9 274 200 .171 9 265 200 .105 9 139 200 .161 9 261 200 .083 9 118 200
bitvector/soft_float_4_true-unreach-call.c.cil.c 5.00 4.86 4.64 5.06 4.66 .110 4 165 133 .107 4 163 133 .064 4 75 133 .115 4 152 133 .056 4 66 133
bitvector/soft_float_5_true-unreach-call.c.cil.c 9.97 9.86 7.41 9.97 7.90 .401 10 638 554 .385 10 629 554 .146 10 170 554 .379 10 617 554 .132 10 146 554
bitvector-regression/implicitfloatconversion_false-unreach-call.i 3.33 3.60 3.49 3.66 3.45 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector-regression/implicitunsignedconversion_false-unreach-call.i 3.47 3.43 3.42 3.36 3.53 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector-regression/integerpromotion_false-unreach-call.i 3.48 4.01 4.03 4.11 4.24 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector-regression/signextension2_false-unreach-call.i 4.19 4.03 4.05 4.14 4.16 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector-regression/signextension_false-unreach-call.i 4.14 4.06 4.17 4.14 4.15 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
bitvector-regression/implicitunsignedconversion_true-unreach-call.i 2.99 3.38 3.50 3.49 3.44 .001 1 2 2 .002 1 3 2 .001 1 2 2 .002 1 2 2 .002 1 3 2
bitvector-regression/integerpromotion_true-unreach-call.i 4.02 3.93 3.86 4.03 3.93 .001 1 2 1 .002 1 3 1 .002 1 2 1 .002 1 2 1 .002 1 3 1
bitvector-regression/signextension2_true-unreach-call.i 4.30 3.56 4.23 4.18 4.19 .013 4 32 10 .015 4 36 10 .013 4 32 10 .014 4 32 10 .021 4 36 10
bitvector-regression/signextension_true-unreach-call.i 4.14 4.32 4.29 4.34 3.62 .023 4 52 26 .021 4 56 26 .019 4 36 26 .022 4 52 26 .013 4 40 26
bitvector-loops/diamond_false-unreach-call2.i 3.78 3.68 3.72 3.78 3.79 .002 1 3 3 .003 1 3 3 .001 1 1 3 .002 1 3 3 .001 1 1 3
bitvector-loops/overflow_false-unreach-call1.i 902    902    902    902    902    .006 2 4 4 .003 2 4 4 .003 2 3 4 .004 2 4 4 .003 2 3 4
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 4.02 3.81 3.37 3.90 3.99 .022 4 22 14 .018 4 24 14 .014 4 15 14 .018 4 22 14 .018 4 17 14
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c 68.2  55.8  61.2  67.4  50.8  22.2   457 96966 49762 11.2   457 70288 49762 15.6   457 55454 49762 21.4   457 94903 49762 5.63  457 28649 49762
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c 48.9  39.3  39.3  47.3  34.8  18.9   314 66798 35392 9.72  314 47189 35392 13.5   314 38158 35392 18.8   314 64696 35392 4.71  314 18232 35392
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c 72.6  49.6  48.8  67.4  50.9  25.9   435 100448 58516 12.8   435 74080 58516 17.4   435 50886 58516 24.8   435 97777 58516 5.96  435 24173 58516
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c 22.5  14.9  21.8  23.7  20.2  3.06  97 14608 7191 1.46  97 10169 7191 2.49  97 8718 7191 3.02  97 14295 7191 1.11  97 4224 7191
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c 107    89.1  89.6  104    82.9  32.5   618 139081 75023 17.8   618 104678 75023 22.0   618 76845 75023 31.5   618 135207 75023 8.56  618 42103 75023
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c 60.9  47.7  53.1  58.2  43.7  28.1   277 68653 39781 17.7   277 54424 39781 18.6   277 36841 39781 26.8   277 65606 39781 8.89  277 22404 39781
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c 50.4  40.0  37.9  46.4  33.5  19.7   308 66095 35135 10.1   308 47060 35135 13.3   308 37768 35135 18.6   308 63956 35135 4.70  308 18420 35135
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c 71.2  55.0  62.1  68.3  47.9  26.2   450 103430 60118 13.3   450 76335 60118 17.7   450 52557 60118 25.2   450 100655 60118 5.76  450 25121 60118
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c 19.0  17.7  19.5  18.6  18.8  2.59  74 10117 4317 1.38  74 6528 4317 2.25  74 6792 4317 2.29  74 9856 4317 1.02  74 3177 4317
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c 25.3  18.0  23.8  23.7  21.9  4.08  136 19901 9461 1.76  136 13139 9461 3.14  136 12007 9461 3.85  136 19498 9461 1.35  136 5201 9461
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 18.6  18.9  19.0  17.3  18.6  .896 78 4739 3401 .864 78 4607 3401 .492 78 1975 3401 .857 78 4739 3401 .488 78 1843 3401
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 19.3  17.9  17.9  18.7  18.3  .821 78 4674 3411 .770 78 4542 3411 .458 78 1903 3411 .814 78 4674 3411 .430 78 1771 3411
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 18.8  19.0  19.3  17.7  17.7  .891 78 4684 3419 .857 78 4552 3419 .478 78 1903 3419 .855 78 4684 3419 .456 78 1771 3419
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 18.6  18.2  18.1  18.9  18.5  .847 78 4676 3413 .781 78 4544 3413 .448 78 1903 3413 .857 78 4676 3413 .507 78 1771 3413
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 59.5  62.3  58.9  62.5  58.4  7.69  301 32325 22055 7.60  301 30695 22055 2.95  301 14586 22055 7.81  301 32325 22055 2.75  301 12956 22055
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 31.4  32.1  31.2  32.1  31.1  4.93  179 21559 16701 4.92  179 21183 16701 1.79  179 7652 16701 4.68  179 21559 16701 1.82  179 7276 16701
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 27.4  29.5  25.5  28.8  27.3  3.51  141 17439 14053 3.67  141 17253 14053 1.39  141 5489 14053 3.74  141 17439 14053 1.38  141 5303 14053
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 24.8  26.4  23.0  23.4  24.6  2.13  122 11620 9196 2.28  122 11478 9196 .971 122 3960 9196 2.18  122 11620 9196 1.03  122 3818 9196
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 53.4  53.1  52.4  53.6  52.1  5.15  271 26990 19950 5.15  271 26569 19950 2.18  271 11145 19950 5.16  271 26990 19950 2.20  271 10724 19950
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 16.3  16.3  17.1  16.7  17.1  1.03  67 4979 3866 1.09  67 4890 3866 .605 67 1707 3866 1.06  67 4979 3866 .487 67 1618 3866
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 16.6  16.8  18.5  15.9  17.8  .979 67 4982 3869 .981 67 4902 3869 .524 67 1732 3869 .976 67 4982 3869 .480 67 1652 3869
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 4.88 4.82 4.93 4.99 4.84 .007 1 10 3 .007 1 11 3 .011 1 10 3 .010 1 10 3 .011 1 11 3
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 18.1  17.0  18.8  18.0  17.8  .847 80 4749 3337 .833 80 4619 3337 .537 80 2103 3337 .872 80 4749 3337 .498 80 1973 3337
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 18.1  18.6  18.9  18.4  18.6  .858 80 4675 3343 .835 80 4545 3343 .495 80 2023 3343 .843 80 4675 3343 .453 80 1893 3343
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 16.7  18.5  18.2  19.4  19.2  .854 80 4692 3352 .856 80 4562 3352 .537 80 2024 3352 .839 80 4692 3352 .477 80 1894 3352
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 18.7  17.4  18.7  18.2  16.9  .865 80 4677 3345 .794 80 4547 3345 .490 80 2023 3345 .906 80 4677 3345 .448 80 1893 3345
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 23.7  24.6  24.6  24.7  24.3  3.76  133 16479 13008 3.85  133 16253 13008 1.44  133 5619 13008 3.93  133 16479 13008 1.45  133 5393 13008
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c 10.8  9.95 10.2  9.90 9.57 .459 26 2035 1556 .476 26 2015 1556 .256 26 762 1556 .463 26 2035 1556 .250 26 742 1556
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 5.45 5.28 5.18 5.36 4.99 .121 14 314 191 .100 14 306 191 .071 14 175 191 .122 14 314 191 .073 14 167 191
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 24.8  26.7  23.3  24.8  23.8  4.20  134 16696 13168 4.08  134 16483 13168 1.43  134 5772 13168 4.20  134 16696 13168 1.32  134 5559 13168
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 22.4  25.0  23.3  25.0  23.4  3.76  140 17059 13380 3.95  140 16828 13380 1.45  140 5970 13380 4.12  140 17059 13380 1.31  140 5739 13380
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 24.3  25.6  22.3  25.0  23.1  3.91  140 16990 13310 4.08  140 16763 13310 1.42  140 5953 13310 4.14  140 16990 13310 1.42  140 5726 13310
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 26.7  27.4  25.1  26.4  26.4  3.23  136 16115 12789 3.28  136 15892 12789 1.21  136 5275 12789 3.16  136 16115 12789 1.26  136 5052 12789
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 22.4  23.3  22.1  25.2  21.7  2.08  130 11849 9077 1.95  130 11642 9077 1.02  130 4353 9077 2.08  130 11849 9077 .973 130 4146 9077
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 24.7  23.9  24.5  24.3  24.6  3.10  143 16279 12890 2.98  143 16055 12890 1.27  143 5398 12890 3.07  143 16279 12890 1.15  143 5174 12890
locks/test_locks_14_false-unreach-call.c 4.04 4.08 4.10 4.03 3.94 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
locks/test_locks_15_false-unreach-call.c 4.23 3.47 4.19 4.06 4.22 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
locks/test_locks_10_true-unreach-call.c 56.5  56.4  61.6  56.9  58.7  .559 200 9460 4090 .479 200 7660 4090 .514 200 7740 4090 .596 200 9460 4090 .553 200 5940 4090
locks/test_locks_11_true-unreach-call_false-termination.c 145    144    144    147    144    .760 242 12540 5434 .599 242 10120 5434 .650 242 10219 5434 .748 242 12540 5434 .508 242 7799 5434
locks/test_locks_12_true-unreach-call_false-termination.c 532    497    494    495    498    .811 288 16224 7044 .666 288 13056 7044 .697 288 13176 7044 .826 288 16224 7044 .595 288 10008 7044
locks/test_locks_13_true-unreach-call.c 901    902    902    902    902    1.04  316 19378 8372 .796 315 15543 8346 .886 315 15674 8346 1.02  311 19106 8241 .659 316 11926 8372
locks/test_locks_14_true-unreach-call.c 902    902    902    901    902    1.17  328 21856 9360 .934 328 17592 9360 1.01  327 17683 9332 1.14  328 21856 9360 .841 328 13468 9360
locks/test_locks_15_true-unreach-call_false-termination.c 901    902    902    902    901    1.48  338 24322 10338 1.02  338 19590 10338 1.14  338 19735 10338 1.29  339 24386 10368 .851 341 15114 10428
locks/test_locks_5_true-unreach-call_false-termination.c 10.7  10.3  10.0  10.4  10.2  .186 50 1230 520 .150 50 1030 520 .149 50 1045 520 .173 50 1230 520 .154 50 845 520
locks/test_locks_6_true-unreach-call_false-termination.c 15.6  16.9  16.9  16.3  14.5  .260 72 2100 894 .206 72 1740 894 .200 72 1764 894 .242 72 2100 894 .185 72 1404 894
locks/test_locks_7_true-unreach-call_false-termination.c 17.2  17.9  18.8  17.6  20.0  .326 98 3304 1414 .278 98 2716 1414 .283 98 2751 1414 .293 98 3304 1414 .239 98 2163 1414
locks/test_locks_8_true-unreach-call_false-termination.c 16.3  24.6  19.6  17.6  23.7  .342 128 4896 2104 .321 128 4000 2104 .326 128 4048 2104 .364 128 4896 2104 .299 128 3152 2104
locks/test_locks_9_true-unreach-call.c 28.7  28.9  28.2  28.7  26.3  .535 162 6930 2988 .440 162 5634 2988 .421 162 5697 2988 .522 162 6930 2988 .337 162 4401 2988
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i 904    904    904    904    904    .460 13 1004 642 .485 13 975 642 .229 13 470 642 .403 13 955 642 .318 13 438 642
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i 904    903    904    904    903    .488 16 980 746 .439 16 944 746 .250 16 355 746 .434 16 920 746 .180 16 318 746
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i 29.5  25.4  27.1  27.2  25.5  2.16  62 5795 3933 1.89  62 5592 3933 .874 62 2628 3933 1.82  62 5429 3933 .721 62 2421 3933
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i 915    991    943    916    931    186     567 103053 59403 183     567 101535 59403 135     567 51323 59403 180     567 99298 59403 129     567 49581 59403
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i 36.7  35.0  39.2  36.1  34.5  .636 44 2989 2101 .496 44 2490 2101 .390 44 1171 2101 .725 44 2842 2101 .205 44 669 2101
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i 23.8  21.3  22.8  23.9  24.0  .642 23 1504 827 .618 23 1399 827 .453 23 834 827 .664 23 1468 827 .390 23 728 827
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i 912    910    902    912    902    688     180 65716 60598 706     180 66044 60938 9.13  193 9225 88382 688     180 65054 66289 5.86  193 9159 88382
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i 904    903    904    904    902    15.4   26 1170 308 17.7   26 906 308 3.93  26 934 308 15.6   26 1158 308 4.05  26 670 308
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i 1010    1010    1010    1010    1010   
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i 14.1  13.6  11.4  13.7  10.8  .676 7 810 712 .649 7 805 712 .245 7 169 712 .581 7 745 712 .238 7 163 712
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i 15.5  12.7  13.1  14.9  13.1  .750 11 1065 865 .603 11 1048 865 .305 11 324 865 .599 11 978 865 .304 11 304 865
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i 21.5  22.4  21.2  20.4  18.9  .811 21 1851 1327 .820 21 1768 1327 .405 21 737 1327 .719 21 1721 1327 .433 21 652 1327
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i 14.1  14.6  12.0  13.8  13.5  .266 9 368 247 .315 9 328 247 .144 9 154 247 .263 9 347 247 .162 9 113 247
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i 21.5  24.0  22.2  23.4  19.2  .892 11 1667 1239 1.02  11 1620 1239 .594 11 628 1239 .946 11 1536 1239 .488 11 580 1239
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i 907    908    906    907    909    9.91  137 31104 24568 9.76  137 30482 24568 3.56  137 9673 24568 9.23  137 29428 24568 3.47  137 9046 24568
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i 17.7  17.3  15.7  17.8  13.3  .741 8 1096 918 .682 8 1083 918 .352 8 288 918 .706 8 1011 918 .296 8 275 918
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i 908    909    909    908    909    .231 24 1542 704 .231 24 1230 704 .176 24 964 704 .222 24 1477 704 .127 24 650 704
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i 903    903    903    902    903    .355 5 465 303 .343 5 404 303 .189 5 198 303 .401 5 455 303 .213 5 137 303
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i 903    903    902    902    903    4.15  43 5093 2383 3.78  43 3929 2383 1.57  43 3091 2383 3.95  43 4841 2383 1.11  43 1920 2383
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i 902    902    902    902    902    8.61  618 52961 37249 8.51  616 50614 36642 3.62  617 22973 36943 8.33  615 50992 36357 3.49  617 21346 36943
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i 904    905    904    902    905    70.4   1051 221102 144105 67.5   1061 214040 145432 38.2   1103 118558 150568 73.7   1052 213655 144281 33.7   1082 107130 147890
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i 245    236    205    252    220    28.5   88 17560 13940 30.8   88 16698 13940 1.81  88 4426 13940 26.2   88 16184 13940 1.53  88 3561 13940
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i 69.6  74.1  66.8  73.4  66.8  9.01  355 49731 38974 9.20  355 48599 38974 3.29  355 16476 38974 9.03  355 45961 38974 3.04  355 15337 38974
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i 367    313    177    292    175    237     305 223850 194699 225     305 221618 194699 56.3   305 44579 194699 203     305 194367 194699 53.2   305 42272 194699
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i 903    903    729    901    697    549     201 264564 237042 589     211 291661 261981 132     331 71023 353699 512     210 264168 261176 131     331 70986 353699
ldv-linux-3.0/module_get_put-drivers-net-pppox.ko_true-unreach-call.cil.out.i.pp.i 904    904    904    904    904    .381 11 871 745 .360 11 880 745 .211 11 249 745 .335 11 820 745 .212 11 256 745
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i 905    905    903    903    903    701     51 93377 78826 706     51 92660 78494 127     52 22928 88774 651     52 87619 88774 128     52 22565 88774
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i 904    904    903    904    904    24.5   64 12224 8920 23.5   64 11620 8920 1.60  64 3758 8920 25.3   64 11969 8920 1.31  64 3148 8920
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i 906    906    905    906    906    12.9   81 27601 7934 12.7   81 25546 7934 3.81  81 20178 7934 11.6   81 26663 7934 3.62  81 18121 7934
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i 903    902    903    902    903    .356 31 2662 2151 .363 31 2541 2151 .139 31 736 2151 .353 31 2444 2151 .126 31 615 2151
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i 12.5  12.9  10.6  12.3  10.3  .455 7 625 524 .435 7 617 524 .203 7 168 524 .467 7 576 524 .225 7 159 524
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i 903    906    903    924    903    427     72 162950 160157 421     72 157662 155314 46.3   77 8981 186329 421     72 156090 154715 53.6   78 9894 192933
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i 903    905    903    903    902    163     476 202605 167129 168     475 200185 166007 47.5   508 64819 187621 157     486 196500 173054 47.8   509 63851 187999
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i 907    910    967    910    914    527     51 89897 76823 531     51 89768 76823 87.7   51 18448 76823 499     51 83908 76823 88.3   51 18315 76823
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i 903    903    911    903    902    3.04  129 14335 10385 2.97  135 14641 11074 1.39  129 5463 10385 3.03  133 14126 10796 1.19  126 4663 9909
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i 930    928    927    933    903    773     78 17896 15420 767     78 17597 15371 766     78 17643 107192 763     78 16599 16275 752     79 21049 131440
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i 910    910    910    910    910    8.11  232 33736 26563 7.96  232 32689 26563 2.70  232 10900 26563 8.24  232 32396 26563 2.58  232 9849 26563
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i 110    70.3  89.4  92.3  96.3  10.9   381 38731 29497 10.7   381 36339 29497 2.67  381 12548 29497 9.85  381 36628 29497 2.61  381 10142 29497
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i 902    902    902    902    902    .588 14 923 301 .511 14 794 301 .392 14 713 301 .606 14 902 301 .399 14 568 301
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i 902    902    907    906    902    112     699 285870 256400 106     699 280429 256400 20.5   699 45017 256400 99.7   699 252653 256400 17.9   699 39553 256400
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i 533    733    512    683    530    261     578 293566 260346 255     578 292240 260346 50.1   578 54128 260346 219     578 253410 260346 50.3   578 52787 260346
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 42.0  41.2  41.6  42.5  39.8  .689 2 395 331 .680 2 384 331 .286 2 94 331 .757 2 373 331 .282 2 82 331
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 30.6  29.5  26.8  28.7  28.5  7.85  101 16808 12416 7.37  101 16648 12416 3.55  101 6915 12416 7.14  101 15621 12416 3.53  101 6748 12416
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 24.1  22.7  26.1  25.6  24.0  1.39  29 3182 2059 1.14  29 2848 2059 .899 29 1456 2059 1.36  29 3006 2059 .760 29 1117 2059
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 19.8  18.9  20.3  18.9  17.4  .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
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 31.8  32.8  33.7  32.6  31.2  .236 13 633 279 .212 13 575 279 .204 13 434 279 .242 13 618 279 .190 13 374 279
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 32.0  29.5  30.7  31.3  33.3  .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
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 10.6  11.2  11.3  10.1  10.1  .010 1 7 3 .008 1 4 3 .011 1 7 3 .008 1 6 3 .005 1 3 3
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 905    905    905    905    911    1.83  20 3691 2698 1.65  20 3542 2698 1.02  20 1453 2698 1.81  20 3539 2698 .854 20 1298 2698
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 14.9  15.4  15.7  16.5  15.7  .025 1 27 23 .023 1 28 23 .012 1 8 23 .023 1 27 23 .014 1 9 23
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 26.9  27.0  25.8  28.3  26.2  1.16  43 4061 2826 1.06  43 3851 2826 .636 43 1664 2826 1.14  43 3880 2826 .543 43 1451 2826
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 15.5  15.6  16.1  15.0  14.8  .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 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 33.3  35.6  34.1  34.4  35.6  .078 2 89 61 .078 2 91 61 .057 2 38 61 .062 2 87 61 .050 2 40 61
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 22.2  22.2  21.9  24.1  23.9  .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
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 8.39 8.48 8.48 8.97 8.82 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
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 16.5  17.6  17.2  17.9  17.1  .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0 .00  0 0 0
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 22.8  20.7  22.9  22.7  22.5  .079 2 79 49 .086 2 70 49 .067 2 40 49 .085 2 75 49 .048 2 30 49
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 916    913    905    914    905    442     293 115339 79311 400     293 104554 79251 150     293 43377 135699 415     293 106818 79185 112     293 32641 135699
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 46.8  42.1  44.2  44.6  39.1  1.15  21 2108 1218 .693 21 1580 1218 .901 21 1036 1218 1.12  21 2027 1218 .401 21 506 1218
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    902    902    902    555     56 40309 29430 564     56 37925 29430 132     67 16917 30661 589     55 39420 29250 132     67 13877 30661
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 904    904    906    905    907    59.7   338 108181 34902 51.4   340 80074 35308 34.2   342 81535 35831 57.3   341 106624 35556 25.1   338 51626 34902
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 20.8  21.1  21.0  22.4  19.5  .792 17 1188 304 .705 17 791 304 .577 17 964 304 .735 17 1162 304 .509 17 563 304
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 31.8  30.3  29.9  31.8  31.3  .458 15 826 212 .415 15 698 212 .403 15 708 212 .476 15 812 212 .378 15 577 212
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 497    471    427    509    397    120     194 68894 43558 106     194 63334 43558 56.0   194 32144 43558 110     194 64368 43558 45.6   194 26538 43558
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 22.4  23.2  22.5  22.0  23.8  2.88  97 12135 7751 2.61  97 11332 7751 1.96  97 6209 7751 2.89  97 11690 7751 1.68  97 5375 7751
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 12.1  12.0  10.2  11.7  10.6  .343 13 846 716 .421 13 856 716 .190 13 240 716 .342 13 795 716 .177 13 249 716
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 10.6  10.8  9.38 11.1  10.6  .265 8 539 298 .344 8 533 298 .183 8 307 298 .269 8 516 298 .191 8 300 298
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 17.0  16.2  17.4  17.9  14.0  .682 40 2962 2030 .695 40 2885 2030 .495 40 1422 2030 .743 40 2867 2030 .433 40 1342 2030
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 15.9  16.2  14.1  15.1  14.8  .357 31 1962 1572 .418 31 1989 1572 .191 31 698 1572 .359 31 1857 1572 .221 31 724 1572
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 17.4  17.1  18.2  18.4  16.0  .675 34 2375 1918 .708 34 2339 1918 .357 34 725 1918 .791 34 2307 1918 .329 34 686 1918
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 10.3  10.9  10.5  10.1  10.9  .206 16 607 440 .216 16 593 440 .137 16 267 440 .192 16 581 440 .179 16 252 440
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 17.1  18.4  17.1  15.4  15.8  .681 34 2592 1774 .664 34 2508 1774 .483 34 1186 1774 .664 34 2441 1774 .381 34 1098 1774
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 910    909    908    909    907    836     12 37601 31740 836     12 38729 31740 827     21 33036 36578 835     13 36226 31762 828     21 33428 38713
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 11.0  11.8  10.5  10.9  10.3  .221 19 753 540 .244 19 741 540 .158 19 336 540 .216 19 726 540 .146 19 322 540
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.82 6.86 5.84 7.09 6.40 .127 6 258 140 .124 6 249 140 .105 6 152 140 .134 6 250 140 .084 6 142 140
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 33.8  31.9  30.1  32.6  29.1  3.44  171 22189 19928 3.19  171 22190 19928 .923 171 4338 19928 3.19  171 20496 19928 .943 171 4339 19928
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 932    979    941    961    948    637     149 107886 84447 645     149 106265 84522 646     149 33267 89042 649     149 101176 84673 639     149 31551 89028
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 68.4  64.8  59.4  70.2  58.8  7.50  327 48691 43718 7.35  327 48696 43718 1.78  327 9572 43718 6.82  327 44920 43718 1.82  327 9577 43718
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 115    124    102    121    98.4  26.2   407 117965 106482 27.1   407 117978 106482 6.14  407 22526 106482 25.7   407 108161 106482 5.82  407 22539 106482
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 906    908    907    906    906    625     229 213663 181279 636     229 212226 181483 639     239 69139 296114 639     229 197797 182489 538     237 63518 272459
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 907    907    906    907    906    808     64 28391 23159 807     64 28373 23413 722     70 27698 150520 807     64 27943 24453 718     70 27316 150102
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 33.3  29.0  24.4  30.4  25.1  4.57  133 20426 18504 4.37  133 20427 18504 1.05  133 3700 18504 4.25  133 18795 18504 1.19  133 3701 18504
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 50.2  48.6  30.4  49.9  48.5  4.81  265 34032 30364 4.69  265 34037 30364 1.24  265 7046 30364 4.34  265 31516 30364 1.31  265 7051 30364
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 909    908    906    910    911    780     165 71427 63256 778     165 71272 63247 776     165 17063 81127 772     165 65344 63463 781     165 16915 81078
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 907    906    906    907    907    825     59 21622 18587 824     59 21568 18657 822     59 8618 39631 824     59 20180 19026 825     59 8629 40420
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 443    447    436    485    434    24.2   750 125489 112860 24.7   750 125657 112860 5.02  750 23401 112860 23.5   750 116507 112860 5.12  750 23569 112860
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 28.5  28.9  25.7  27.9  26.3  3.68  142 22027 19856 3.65  142 22033 19856 1.06  142 4186 19856 3.45  142 20250 19856 1.12  142 4192 19856
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 182    186    139    174    146    54.5   454 182977 165337 55.1   454 182983 165337 11.7   454 34690 165337 49.1   454 167033 165337 11.6   454 34696 165337
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 903    903    904    903    904    178     218 180843 158006 165     218 180326 158006 47.2   218 31346 158006 165     218 172549 158006 47.0   218 30827 158006
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 15.0  17.5  15.1  14.7  15.7  .606 33 2158 1695 .649 33 2128 1695 .400 33 710 1695 .543 33 2014 1695 .361 33 679 1695
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 25.8  25.5  21.5  24.6  25.2  1.40  70 6270 4260 1.27  70 5978 4260 .762 70 2691 4260 1.35  70 6055 4260 .821 70 2395 4260
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 8.28 8.13 7.00 8.29 7.53 .163 7 297 214 .162 7 294 214 .086 7 113 214 .159 7 276 214 .110 7 109 214
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 46.8  43.7  39.6  45.7  41.4  10.5   150 26818 21052 10.3   150 26530 21052 4.52  150 9058 21052 9.72  150 24085 21052 4.30  150 8761 21052
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 13.5  14.4  13.0  14.3  14.3  .558 25 2118 1227 .544 25 2138 1227 .409 25 1191 1227 .576 25 2049 1227 .391 25 1210 1227
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 11.6  12.7  11.0  11.6  10.1  .481 14 1110 761 .530 14 1115 761 .287 14 516 761 .499 14 1057 761 .288 14 520 761
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 6.21 5.24 5.39 5.92 5.35 .143 7 318 277 .113 7 325 277 .061 7 82 277 .131 7 298 277 .067 7 89 277
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 53.1  54.5  48.3  63.3  56.3  8.70  51 8593 7694 8.53  51 8619 7694 .667 51 1468 7694 8.69  51 8317 7694 .589 51 1494 7694
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 902    902    902    902    902    .069 4 119 75 .060 4 107 75 .050 4 64 75 .081 4 117 75 .040 4 51 75
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 140    135    104    143    96.2  40.7   112 30877 24984 40.3   112 29387 24984 6.21  112 7667 24984 44.2   112 29548 24984 5.39  112 6151 24984
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 11.2  11.0  9.02 11.2  8.96 .488 10 737 530 .470 10 743 530 .281 10 294 530 .430 10 673 530 .287 10 299 530
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 15.9  13.4  13.1  14.9  12.9  .567 18 1160 924 .531 18 1153 924 .287 18 379 924 .582 18 1076 924 .303 18 371 924
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 9.58 8.56 8.99 9.24 9.39 .248 14 597 477 .204 14 595 477 .149 14 202 477 .239 14 558 477 .145 14 199 477
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 14.9  17.8  13.6  15.8  13.3  .596 19 1321 1083 .701 19 1319 1083 .310 19 396 1083 .643 19 1219 1083 .306 19 393 1083
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 16.7  17.5  13.2  17.1  13.0  .600 25 1273 960 .602 25 1268 960 .269 25 505 960 .586 25 1208 960 .257 25 500 960
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 54.7  54.8  26.7  52.5  27.6  27.7   139 34506 32312 27.2   139 34399 32312 2.79  139 3943 32312 25.9   139 33328 32312 2.70  139 3835 32312
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 8.19 8.20 8.03 7.94 8.26 .066 5 125 106 .062 5 130 106 .023 5 38 106 .067 5 122 106 .036 5 43 106
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 34.4  36.2  29.5  36.3  31.3  7.71  105 16591 11125 7.77  105 15994 11125 3.76  105 7536 11125 7.75  105 15617 11125 3.63  105 6937 11125
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 7.18 7.12 6.99 6.73 7.00 .049 3 75 66 .051 3 78 66 .021 3 18 66 .038 3 70 66 .021 3 21 66
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 8.27 8.35 7.89 8.15 7.84 .132 11 337 255 .137 11 333 255 .083 11 137 255 .144 11 322 255 .080 11 133 255
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 11.2  11.3  11.0  11.4  11.1  .223 15 671 555 .199 15 683 555 .115 15 204 555 .205 15 630 555 .140 15 216 555
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 19.0  19.5  14.9  19.2  16.5  .452 39 2150 1631 .450 39 2155 1631 .179 39 816 1631 .398 39 2019 1631 .199 39 821 1631
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 7.36 6.81 5.63 7.21 6.71 .108 7 277 244 .123 7 284 244 .041 7 66 244 .107 7 260 244 .057 7 73 244
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 11.9  12.0  10.9  12.6  10.9  .214 17 732 602 .230 17 746 602 .117 17 233 602 .220 17 691 602 .122 17 247 602
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 17.9  16.2  15.5  17.9  16.0  .377 36 1929 1492 .339 36 1939 1492 .181 36 704 1492 .369 36 1809 1492 .159 36 714 1492
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 8.44 7.76 8.04 8.42 6.87 .144 9 337 270 .149 9 344 270 .079 9 116 270 .134 9 318 270 .072 9 123 270
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.02 6.08 5.79 5.90 5.89 .046 4 121 106 .074 4 125 106 .031 4 30 106 .054 4 113 106 .027 4 34 106
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 14.1  14.2  14.5  14.0  15.5  .291 21 974 767 .327 21 987 767 .149 21 342 767 .294 21 915 767 .191 21 355 767
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 12.3  12.5  11.4  11.7  11.3  .223 17 770 633 .290 17 783 633 .129 17 238 633 .217 17 723 633 .144 17 251 633
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 8.43 8.15 7.58 8.25 7.52 .155 10 445 394 .156 10 455 394 .075 10 102 394 .134 10 419 394 .080 10 112 394
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 19.7  17.6  18.5  18.6  18.8  .511 65 3063 2300 .481 65 3018 2300 .276 65 1260 2300 .532 65 2912 2300 .271 65 1207 2300
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 16.5  16.4  15.0  16.6  13.9  .441 36 1540 1177 .436 36 1516 1177 .263 36 605 1177 .434 36 1462 1177 .238 36 574 1177
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 9.39 8.54 8.18 9.07 8.73 .196 11 548 470 .181 11 559 470 .095 11 156 470 .208 11 519 470 .104 11 167 470
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 23.8  24.8  23.5  24.6  25.1  1.13  121 7686 5775 1.08  121 7553 5775 .558 121 3122 5775 1.06  121 7318 5775 .532 121 2980 5775
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 8.17 7.68 7.57 6.53 6.29 .108 8 311 269 .112 8 319 269 .058 8 84 269 .105 8 291 269 .062 8 92 269
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 11.1  11.1  10.4  10.2  8.91 .215 14 631 530 .220 14 643 530 .119 14 183 530 .179 14 593 530 .093 14 195 530
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 12.4  13.7  13.9  12.1  12.7  .221 18 826 658 .247 18 838 658 .129 18 282 658 .241 18 776 658 .137 18 294 658
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 17.4  16.8  19.5  18.0  16.9  .361 45 2300 1817 .399 45 2325 1817 .179 45 786 1817 .379 45 2169 1817 .177 45 811 1817
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 23.5  23.1  20.5  24.3  22.4  .499 69 3770 3011 .521 69 3807 3011 .210 69 1230 3011 .493 69 3567 3011 .236 69 1267 3011
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 10.6  10.3  9.52 11.0  10.4  .265 14 656 571 .240 14 670 571 .090 14 170 571 .223 14 618 571 .123 14 184 571
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 34.7  43.1  39.3  41.6  39.0  3.56  139 15889 12562 3.36  139 15743 12562 1.33  139 5442 12562 3.19  139 14783 12562 1.28  139 5289 12562
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 19.7  19.4  18.1  20.8  18.7  .793 63 3287 2595 .760 63 3245 2595 .341 63 1182 2595 .733 63 3112 2595 .401 63 1135 2595
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 25.9  24.5  23.0  26.1  22.5  1.40  109 7667 6186 1.44  109 7585 6186 .535 109 2456 6186 1.43  109 7317 6186 .503 109 2369 6186
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 18.7  19.5  19.7  19.9  18.9  1.34  15 2157 1729 1.54  15 2143 1729 .855 15 679 1729 1.51  15 1939 1729 1.01  15 664 1729
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 187    187    122    186    122    102     299 108231 82701 98.3   299 106966 82701 38.0   299 40715 82701 97.0   299 102046 82701 37.0   299 39336 82701
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 17.3  17.5  15.5  19.2  16.4  .524 31 1800 1360 .522 31 1764 1360 .291 31 733 1360 .549 31 1721 1360 .307 31 695 1360
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 903    903    903    903    903    .911 27 2645 2235 .938 27 2626 2235 .504 27 663 2235 .869 27 2479 2235 .454 27 642 2235
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 12.3  13.5  11.1  13.0  12.4  .444 14 782 594 .506 14 768 594 .257 14 296 594 .442 14 727 594 .265 14 280 594
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 18.8  17.7  19.6  19.2  19.0  .807 32 2598 2109 .849 32 2548 2109 .449 32 793 2109 .835 32 2421 2109 .399 32 740 2109
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 10.2  10.8  9.73 10.6  9.97 .198 24 808 609 .201 24 796 609 .122 24 352 609 .220 24 790 609 .133 24 340 609
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 15.6  14.8  13.4  14.7  15.0  .398 66 3022 2223 .384 66 2989 2223 .236 66 1445 2223 .382 66 2962 2223 .236 66 1412 2223
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 18.2  17.5  17.0  18.5  16.9  1.07  26 3089 2400 1.02  26 3058 2400 .493 26 1094 2400 .918 26 2719 2400 .456 26 1059 2400
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 53.8  53.1  55.1  54.8  51.4  1.69  101 11926 10276 1.73  101 11980 10276 .571 101 2639 10276 1.66  101 11655 10276 .628 101 2690 10276
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 907    917    912    907    961    20.1   171 33993 24272 17.5   171 32499 24272 8.67  171 13182 24272 18.2   171 31233 24272 7.12  171 11630 24272
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 20.4  21.2  18.0  21.5  19.0  2.29  43 7039 6447 2.27  43 7058 6447 .476 43 1002 6447 2.37  43 6860 6447 .559 43 1020 6447
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 23.5  20.0  23.9  24.5  24.4  1.94  55 5435 4082 1.93  55 5335 4082 .927 55 2081 4082 1.93  55 5136 4082 .869 55 1976 4082
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 14.5  15.5  14.1  14.5  13.9  .563 28 1963 1532 .569 28 1933 1532 .343 28 718 1532 .562 28 1848 1532 .318 28 686 1532
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 389    352    202    346    190    243     206 111989 88130 214     206 105145 88130 74.7   206 28712 88130 214     206 100091 88130 52.3   206 21838 88130
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 18.0  17.6  20.1  21.3  16.8  .866 29 2046 1556 .828 29 2030 1556 .683 29 800 1556 .939 29 1883 1556 .458 29 774 1556
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 437    398    379    409    386    56.7   125 67998 55756 56.8   125 66959 55756 18.6   125 20400 55756 52.5   125 61446 55756 17.0   125 19344 55756
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 24.6  24.6  21.2  24.2  21.5  2.32  57 5316 4124 2.31  57 5207 4124 .878 57 1779 4124 2.17  57 5004 4124 .900 57 1665 4124
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 25.4  24.6  24.0  24.3  25.3  1.81  76 6613 4982 1.71  76 6523 4982 .831 76 2439 4982 1.75  76 6257 4982 .829 76 2346 4982
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 26.8  27.8  24.0  28.2  25.9  2.70  74 6893 5434 2.59  74 6752 5434 .879 74 2173 5434 2.59  74 6531 5434 .931 74 2029 5434
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 20.6  20.4  19.3  19.6  19.6  .931 31 2331 1590 .818 31 2282 1590 .470 31 1036 1590 .787 31 2204 1590 .482 31 984 1590
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 36.1  41.4  30.6  34.8  32.0  9.66  96 17287 12477 10.2   96 16871 12477 3.67  96 6398 12477 9.22  96 16443 12477 3.54  96 5981 12477
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 22.9  21.7  20.1  20.8  19.1  1.18  45 3479 2714 1.01  45 3443 2714 .477 45 1205 2714 .953 45 3272 2714 .482 45 1166 2714
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 23.7  24.3  21.7  23.4  18.9  1.29  51 4345 3414 1.35  51 4294 3414 .635 51 1442 3414 1.36  51 4072 3414 .473 51 1388 3414
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 19.4  18.3  16.1  17.0  20.5  .701 33 2174 1678 .643 33 2146 1678 .347 33 786 1678 .628 33 2043 1678 .386 33 755 1678
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 903    903    903    903    903    .507 16 867 628 .507 16 858 628 .319 16 335 628 .494 16 838 628 .266 16 325 628
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 49.5  50.3  31.2  45.6  27.4  26.9   32 15004 11757 28.1   32 14948 11757 8.85  32 4824 11757 24.6   32 13604 11757 8.40  32 4765 11757
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 63.4  59.4  39.1  58.8  41.6  39.5   30 18768 12956 38.1   30 18712 12956 17.3   30 8667 12956 36.1   30 17374 12956 18.0   30 8608 12956
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 123    124    55.5  116    55.3  92.8   36 27882 22063 94.7   36 27824 22063 27.6   36 8692 22063 86.0   36 25214 22063 27.2   36 8631 22063
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 10.9  12.7  12.7  13.4  11.9  .315 21 917 731 .367 21 913 731 .183 21 321 731 .346 21 879 731 .177 21 316 731
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 8.88 8.87 8.43 8.86 8.23 .140 10 299 215 .176 10 294 215 .102 10 141 215 .165 10 286 215 .085 10 135 215
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 8.85 8.81 8.60 9.13 8.48 .147 11 338 248 .141 11 334 248 .106 11 152 248 .161 11 324 248 .102 11 147 248
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 14.4  14.8  12.5  14.7  12.8  .363 23 1018 777 .378 23 1008 777 .201 23 399 777 .363 23 966 777 .177 23 388 777
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 908    908    908    908    908    825     24 13888 8723 823     24 14623 9165 821     24 16473 17518 823     24 14811 9381 825     24 16346 17392
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 16.1  16.1  14.9  15.6  15.8  1.00  15 1424 1023 .949 15 1412 1023 .575 15 602 1023 .853 15 1359 1023 .496 15 589 1023
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 10.6  12.6  9.97 10.7  11.2  .239 22 825 599 .277 22 814 599 .145 22 360 599 .237 22 796 599 .158 22 348 599
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 10.2  10.5  9.99 9.89 10.0  .223 11 375 274 .228 11 369 274 .131 11 165 274 .229 11 360 274 .141 11 158 274
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 19.2  20.2  19.9  19.6  20.5  .861 24 1968 1471 .985 24 1949 1471 .521 24 788 1471 .859 24 1837 1471 .508 24 767 1471
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 14.2  15.5  12.0  14.3  12.1  .492 19 987 729 .514 19 976 729 .297 19 436 729 .464 19 937 729 .265 19 424 729
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 10.3  10.3  9.93 10.3  9.61 .276 12 493 361 .247 12 484 361 .160 12 208 361 .249 12 468 361 .158 12 198 361
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 14.2  16.6  16.3  16.1  13.8  .393 33 1565 970 .410 33 1449 970 .279 33 822 970 .401 33 1516 970 .226 33 705 970
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 20.9  21.0  21.0  21.7  20.4  1.39  67 5316 4263 1.31  67 5284 4263 .645 67 1889 4263 1.27  67 4987 4263 .635 67 1855 4263
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 15.2  15.6  12.9  15.6  12.8  .524 15 811 592 .539 15 795 592 .263 15 328 592 .500 15 782 592 .235 15 311 592
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 15.7  14.6  13.9  16.4  15.7  .387 21 1304 1065 .430 21 1314 1065 .234 21 429 1065 .441 21 1229 1065 .228 21 438 1065
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 17.1  18.7  15.8  15.9  17.1  1.19  42 4349 3521 1.32  42 4322 3521 .556 42 1368 3521 1.07  42 4297 3521 .561 42 1340 3521
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 902    902    902    902    902    1.07  27 2199 1576 .944 27 2151 1576 .601 27 989 1576 1.05  27 2043 1576 .585 27 934 1576
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 13.6  13.5  13.9  13.5  12.7  .951 19 2630 2037 .857 19 2523 2037 .539 19 815 2037 .908 19 2272 2037 .542 19 703 2037
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 11.2  11.2  10.1  10.8  10.4  .365 11 697 426 .385 11 654 426 .281 11 353 426 .369 11 656 426 .265 11 306 426
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 16.4  17.6  15.9  17.9  15.0  .811 37 2944 2433 .800 37 2903 2433 .353 37 842 2433 .805 37 2716 2433 .319 37 800 2433
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 17.0  17.8  17.0  17.7  16.2  1.36  43 5011 3885 1.42  43 4940 3885 .653 43 1755 3885 1.34  43 4714 3885 .594 43 1683 3885
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 19.7  19.3  17.4  19.1  17.3  .833 32 2492 1863 .838 32 2464 1863 .415 32 948 1863 .828 32 2342 1863 .464 32 918 1863
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 18.1  15.0  16.7  17.7  15.0  .566 16 1013 719 .498 16 985 719 .381 16 431 719 .553 16 971 719 .322 16 402 719
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 23.4  21.0  21.7  23.8  19.8  3.10  42 4729 3539 3.03  42 4694 3539 1.43  42 2092 3539 2.94  42 4583 3539 1.42  42 2055 3539
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 18.4  20.0  15.7  17.2  16.5  .748 34 2509 1883 .869 34 2480 1883 .369 34 948 1883 .740 34 2361 1883 .374 34 917 1883
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 20.5  19.9  18.1  19.6  17.8  .952 38 2951 2197 1.00  38 2920 2197 .510 38 1158 2197 .930 38 2773 2197 .437 38 1125 2197
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 18.8  17.9  17.2  18.9  17.0  .862 32 2500 1863 .830 32 2472 1863 .398 32 956 1863 .796 32 2350 1863 .428 32 926 1863
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 19.1  18.9  17.7  18.2  17.4  .857 30 2331 1729 .798 30 2304 1729 .425 30 900 1729 .734 30 2191 1729 .388 30 871 1729
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 20.2  21.3  18.7  20.2  22.2  1.14  36 2772 1913 1.12  36 2716 1913 .620 36 1359 1913 1.03  36 2650 1913 .672 36 1302 1913
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 13.7  15.2  13.4  15.4  10.4  .685 14 1311 991 .645 14 1308 991 .373 14 466 991 .626 14 1206 991 .301 14 462 991
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 22.1  18.3  20.8  17.6  16.8  .932 36 2734 2043 .830 36 2704 2043 .482 36 1052 2043 .843 36 2570 2043 .406 36 1020 2043
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 26.0  23.2  23.0  25.3  24.5  1.58  70 5863 4471 1.45  70 5805 4471 .659 70 2086 4471 1.46  70 5531 4471 .644 70 2026 4471
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 17.7  18.9  17.2  19.3  17.0  1.13  30 2929 2094 1.09  30 2890 2094 .669 30 1225 2094 1.13  30 2796 2094 .603 30 1184 2094
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 19.7  17.5  20.4  20.5  17.5  .772 34 2581 1935 .793 34 2552 1935 .482 34 982 1935 .805 34 2429 1935 .372 34 951 1935
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 19.4  20.9  21.3  19.2  16.4  .903 30 2311 1709 .870 30 2284 1709 .570 30 902 1709 .777 30 2175 1709 .428 30 873 1709
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 20.3  21.3  20.3  21.4  17.0  .832 34 2555 1919 .932 34 2526 1919 .450 34 962 1919 .791 34 2403 1919 .391 34 931 1919
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 22.7  24.2  19.1  22.5  19.1  1.09  42 3032 2364 1.07  42 2996 2364 .436 42 1066 2364 .962 42 2840 2364 .391 42 1028 2364
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 41.9  40.6  36.0  41.4  34.6  8.91  155 24508 19775 8.54  155 24336 19775 2.82  155 7393 19775 8.62  155 22626 19775 2.72  155 7210 19775
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 15.1  15.2  14.8  15.7  14.5  .498 29 1697 1144 .523 29 1666 1144 .321 29 851 1144 .550 29 1637 1144 .338 29 818 1144
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 69.4  68.3  24.4  66.8  24.3  44.7   39 21761 20344 44.0   39 21514 20344 2.18  39 1938 20344 42.7   39 21578 20344 2.19  39 1685 20344
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 7.29 7.93 6.92 7.65 6.81 .152 7 338 241 .138 7 339 241 .096 7 156 241 .140 7 325 241 .110 7 156 241
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 17.7  17.2  15.9  17.2  18.6  .825 27 1993 1371 .777 27 1921 1371 .519 27 910 1371 .823 27 1925 1371 .543 27 834 1371
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 904    905    914    908    903    379     14 54326 49258 367     14 54200 49258 90.5   17 13001 68908 342     15 49452 49258 91.3   18 12881 68960
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 16.5  15.5  12.9  15.0  13.0  .700 21 1441 1053 .637 21 1413 1053 .300 21 593 1053 .554 21 1369 1053 .339 21 563 1053
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 16.8  17.2  17.3  15.6  14.0  .752 23 1793 1477 .698 23 1782 1477 .389 23 530 1477 .640 23 1674 1477 .294 23 517 1477
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 15.6  15.7  13.4  16.3  15.1  .613 22 1609 1319 .650 22 1597 1319 .293 22 481 1319 .635 22 1500 1319 .304 22 467 1319
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 19.5  17.8  16.1  19.2  17.9  .836 23 1838 1481 .812 23 1827 1481 .415 23 582 1481 .819 23 1719 1481 .424 23 569 1481
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 14.6  14.4  13.6  13.8  13.6  .573 16 1274 896 .546 16 1282 896 .408 16 566 896 .547 16 1181 896 .307 16 572 896
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 26.1  26.9  24.7  27.5  24.0  3.84  69 8466 6012 3.75  69 8229 6012 1.89  69 3654 6012 3.55  69 8228 6012 1.84  69 3411 6012
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 903    903    903    902    903    .276 4 280 198 .259 4 275 198 .169 4 115 198 .279 4 269 198 .155 4 109 198
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 902    903    903    903    902    2.36  34 5193 3902 2.50  34 5047 3902 1.21  34 1865 3902 2.52  34 4894 3902 1.19  34 1715 3902
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 902    902    902    902    902    .075 4 128 65 .078 4 121 65 .072 4 84 65 .081 4 126 65 .070 4 76 65
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 17.5  17.9  14.3  18.7  16.3  .807 27 1927 1450 .765 27 1904 1450 .397 27 740 1450 .851 27 1862 1450 .491 27 714 1450
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 14.5  13.9  12.9  13.1  12.6  .812 28 2119 1410 .736 28 1991 1410 .573 28 959 1410 .768 28 2010 1410 .496 28 830 1410
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 9.00 9.43 8.14 9.01 8.39 .174 9 438 384 .160 9 447 384 .082 9 104 384 .170 9 407 384 .088 9 113 384
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 5.83 5.94 5.40 5.58 5.41 .095 6 239 213 .127 6 245 213 .043 6 52 213 .092 6 222 213 .047 6 58 213
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 9.62 9.33 9.18 10.0  9.35 .213 12 666 584 .214 12 678 584 .098 12 158 584 .221 12 622 584 .120 12 170 584
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 18.7  17.1  14.6  17.8  14.3  .599 32 2102 1546 .505 32 2013 1546 .322 32 834 1546 .617 32 1980 1546 .297 32 743 1546
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 8.05 7.93 7.70 8.04 7.70 .117 9 369 317 .116 9 378 317 .060 9 98 317 .147 9 348 317 .062 9 107 317
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 87.2  87.0  65.4  86.4  62.8  42.8   134 56315 40725 42.8   134 55076 40725 18.6   134 21352 40725 43.0   134 55018 40725 17.4   134 20089 40725
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 23.5  22.6  21.2  20.3  21.9  2.66  71 7924 3792 2.58  71 7358 3792 2.03  71 5587 3792 2.60  71 7652 3792 1.90  71 5006 3792
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 36.4  36.3  30.8  37.8  30.2  13.0   69 20447 10889 12.8   69 20360 10889 7.43  69 12508 10889 12.5   69 19908 10889 7.36  69 12421 10889
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 903    903    902    902    903    57.9   156 47674 36295 58.8   156 46532 36295 18.8   156 17784 36295 56.2   156 45588 36295 18.2   156 16630 36295
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 40.6  41.6  35.7  40.4  34.5  14.2   93 26605 14345 14.1   93 26499 14345 8.13  93 15769 14345 13.7   93 25808 14345 8.06  93 15660 14345
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 30.1  26.2  29.7  31.7  29.6  4.68  127 18342 12429 4.47  127 18181 12429 2.22  127 8695 12429 4.64  127 17876 12429 2.22  127 8532 12429
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 39.1  39.5  39.6  39.7  35.4  5.43  178 20376 14521 5.59  178 19756 14521 2.50  178 8209 14521 5.33  178 19482 14521 2.29  178 7551 14521
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 907    853    757    905    665    700     170 142263 44199 644     172 126422 46849 566     172 113740 46849 706     170 141160 44788 477     172 91787 46849
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 39.3  38.8  39.7  41.8  36.5  12.9   91 16527 6601 11.2   91 13940 6601 10.4   91 11678 6601 13.0   91 16276 6601 7.78  91 9077 6601
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 196    193    149    202    146    93.5   268 121426 73892 92.9   268 120287 73892 50.4   268 63098 73892 92.0   268 115524 73892 47.0   268 61958 73892
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 111    107    85.2  110    83.8  52.1   214 84228 62486 51.3   214 83647 62486 24.4   214 34885 62486 51.9   214 81035 62486 23.6   214 34304 62486
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 129    126    93.1  135    98.3  48.8   270 71119 51571 47.3   270 69805 51571 17.6   270 27973 51571 47.6   270 68784 51571 19.2   270 26655 51571
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 18.1  16.7  12.8  17.1  13.7  .376 22 1020 715 .342 22 998 715 .160 22 481 715 .351 22 986 715 .177 22 459 715
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 16.7  14.5  15.9  16.5  15.9  .296 36 1640 1151 .284 36 1608 1151 .210 36 789 1151 .358 36 1612 1151 .188 36 757 1151
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 21.4  20.3  19.2  20.9  20.6  .689 36 2159 1089 .507 36 1857 1089 .610 36 1243 1089 .689 36 2087 1089 .445 36 937 1089
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 23.1  23.5  23.6  21.9  21.4  1.85  68 6033 2942 1.41  68 5078 2942 1.64  68 3611 2942 1.86  68 5907 2942 1.10  68 2649 2942
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 16.9  16.5  17.4  16.9  16.7  .387 47 2336 1693 .424 47 2284 1693 .225 47 1035 1693 .397 47 2297 1693 .215 47 980 1693
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 20.5  20.3  17.7  20.5  17.7  .613 45 2709 1767 .540 45 2616 1767 .377 45 1384 1767 .575 45 2649 1767 .362 45 1291 1767
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 23.4  21.0  20.8  21.5  22.2  .850 93 6401 5042 .840 93 6259 5042 .378 93 2197 5042 .838 93 6271 5042 .339 93 2055 5042
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 9.89 9.43 9.82 9.99 10.1  .049 3 67 53 .032 3 70 53 .022 3 25 53 .054 3 66 53 .039 3 28 53
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 24.4  25.0  24.4  22.7  22.4  1.19  60 5174 3064 1.22  60 5139 3064 .705 60 2894 3064 1.10  60 5086 3064 .673 60 2858 3064
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 9.13 10.1  9.71 9.77 9.30 .087 8 190 127 .086 8 186 127 .057 8 104 127 .088 8 188 127 .054 8 100 127
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 26.4  25.0  24.8  24.9  25.0  1.37  102 7314 4188 1.22  102 6943 4188 .900 102 4437 4188 1.32  102 7156 4188 .808 102 4060 4188
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 24.6  24.5  20.9  26.7  21.8  .744 68 3955 2924 .714 68 3877 2924 .296 68 1653 2924 .798 68 3858 2924 .318 68 1574 2924
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 30.5  29.9  25.8  27.6  24.3  5.36  46 7730 5875 5.11  46 7628 5875 2.12  46 2919 5875 4.99  46 7451 5875 2.12  46 2817 5875
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 18.6  16.6  15.5  18.5  16.7  .396 37 1666 1129 .432 37 1614 1129 .220 37 841 1129 .438 37 1630 1129 .238 37 786 1129
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 16.8  14.5  15.2  15.4  15.9  .361 36 1640 1151 .295 36 1608 1151 .190 36 789 1151 .347 36 1612 1151 .259 36 757 1151
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 906    904    903    905    903    220     290 170879 133796 213     289 166486 133663 95.2   333 63267 170930 210     282 159288 128511 90.7   338 60113 175174
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 18.9  17.0  17.2  18.4  16.4  .022 2 41 28 .017 2 43 28 .014 2 18 28 .022 2 41 28 .013 2 20 28
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 22.9  21.1  21.2  22.1  19.7  3.77  27 5391 4331 3.64  27 5334 4331 1.47  27 1589 4331 3.67  27 5070 4331 1.29  27 1532 4331
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 33.7  28.0  34.7  33.5  30.3  2.80  131 10888 7482 2.55  131 10492 7482 1.26  131 4954 7482 2.66  131 10704 7482 1.20  131 4553 7482
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 28.5  27.2  25.4  29.5  25.7  1.79  64 6311 4545 1.67  64 6111 4545 .891 64 2517 4545 1.76  64 6106 4545 .798 64 2306 4545
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 39.8  40.8  38.0  39.9  39.5  2.60  158 14448 10692 2.49  158 14150 10692 1.13  158 5785 10692 2.43  158 14028 10692 1.10  158 5485 10692
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 16.2  16.0  12.8  14.6  12.7  .270 25 1013 734 .263 25 997 734 .146 25 473 734 .257 25 994 734 .153 25 456 734
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 24.3  24.3  21.9  25.3  22.5  4.28  54 8262 5686 3.67  54 7581 5686 1.93  54 3183 5686 4.06  54 7966 5686 1.60  54 2501 5686
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 23.3  21.2