Tool 2LS 0.5.0 BLAST 2.7.3 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a SymDIVINE ULTIMATE Automizer f7c3ed31 ULTIMATE Kojak f7c3ed31 ULTIMATE Taipan f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic [Linux 4.4.0-57-generic; Linux 4.4.0-59-generic] Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:51:44 CET ]] [[ 2017-01-14 18:06:48 CET ]] [[ 2017-01-14 19:59:41 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]] 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]] 2017-01-10 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]] 2017-01-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]] 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]] 2017-01-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]] 2017-01-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]] 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]] 2017-01-11 16:16:17 CET [[ 2017-01-14 22:37:08 CET ]] [[ 2017-01-15 00:13:18 CET ]] [[ 2017-01-14 22:52:42 CET ]] [[ 2017-01-15 00:24:59 CET ]] 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]] 2017-01-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]] 2017-01-13 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]] 2017-01-13 11:13:29 CET [[ 2017-01-15 02:06:46 CET ]] [[ 2017-01-15 03:46:01 CET ]] [[ 2017-01-15 02:24:39 CET ]] [[ 2017-01-15 04:02:29 CET ]] 2017-01-13 12:41:58 CET [[ 2017-01-15 02:09:41 CET ]] [[ 2017-01-15 04:03:21 CET ]] [[ 2017-01-15 02:31:54 CET ]] [[ 2017-01-15 04:27:36 CET ]] 2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]] 2017-01-14 09:46:18 CET [[ 2017-01-15 02:18:39 CET ]] [[ 2017-01-15 04:12:25 CET ]] [[ 2017-01-15 02:37:40 CET ]] [[ 2017-01-15 04:38:18 CET ]]
Run set 2ls.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety blast.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety cbmc.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety ceagle.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety cpa-bam-bnb.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety cpa-kind.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety cpa-seq.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety depthk.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety esbmc.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety esbmc-falsi.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety esbmc-incr.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety esbmc-kind.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety smack.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety symbiotic4.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety symdivine.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety uautomizer.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety ukojak.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety utaipan.sv-comp17.Systems_DeviceDriversLinux64_ReachSafety
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/blast.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-11_1616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --fix_volatile --fix_inline --silent -Os [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-13_1241.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i 1.7   270 16    0 1.6   110 21    1 4.5  250 50   0 1.1   35   13    0 40   1500 310 1 24   870 160 0 170   2100 2300 0 190   15000 2500 0 14    3900 160   0 7.1   3900 90    0 7.1   3900 99    0 7.1   3900 94    0 640   880 7800 1 710    180   9100   1 47     83   560    -32 8.0 410 68 0 8.3 410 63 0 8.3 420 62 0
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i 79     15000 730    0 3.8   82 40    0 240    1000 1400   0 .93  12   12    0 30   820 250 0 96   3600 630 0 940   8300 7800 0 570   450 7700 0 .58 100 6.4 0 .28  100 3.7  0 .28  100 3.7  0 .28  100 3.1  0 880   480 8700 0 900    390   8700   0 .18  14   2.4  -32 900   3700 8900 0 900   13000 12000 0 490   3600 4600 0
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i 91     1500 570    0 40     280 470    0 25    340 300   0 1.3   13   16    0 16   540 130 0 510   7200 4300 0 910   8600 7800 0 600   1100 7800 0 .78 160 8.3 0 .43  160 4.9  0 .40  160 5.1  0 .40  160 4.4  0 16   220 190 0 900    360   11000   0 .86  15   11    -32 110   2900 1000 0 900   11000 12000 0 110   3000 1100 0
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i 1.3   110 11    0 7.6   210 75    0 54    2300 380   0 2.4   18   27    0 900   6100 9900 0 930   6200 8200 0 940   6600 9800 0 280   450 3500 0 1.7  440 16   0 .85  440 11    0 .87  440 9.3  0 .90  440 9.2  0 880   990 11000 0 900    260   11000   0 6.4   47   74    -32 7.5 330 57 0 8.0 350 66 0 8.1 350 60 0
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i 100     15000 850    0 4.6   160 44    0 850    6900 9200   0 2.6   18   31    0 73   2000 590 0 960   4600 8200 0 960   4900 12000 0 10   350 120 0 1.7  450 20   0 .88  450 11    0 .90  450 9.1  0 .89  450 11    0 56   310 680 0 130    100   1400   0 3.2   66   36    -32 7.3 340 55 0 7.0 330 54 0 7.4 350 54 0
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i 28     440 180    0 24     260 310    0 850    2700 5400   0 1.4   14   16    0 17   670 130 1 80   2300 460 0 100   1000 1200 1 620   2600 7900 0 .85 190 11   0 .48  190 4.7  0 .43  190 5.0  0 .43  190 5.6  0 8.8 210 100 0 900    850   10000   0 .33  16   3.7  -32 550   2500 6100 0 900   12000 10000 0 80   1400 650 0
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i 49     15000 520    0 24     160 280    0 5.8  180 65   0 1.1   12   13    0 55   1600 460 0 920   8800 6400 0 960   7900 9400 0 120   700 1600 0 .62 140 6.8 0 .36  140 3.7  0 .31  140 3.6  0 .32  140 4.0  0 11   240 140 0 900    270   9200   0 .35  15   4.5  -32 900   2400 9000 0 900   13000 12000 0 900   4100 5700 0
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i 120     15000 1000    0 61     660 600    0 850    4400 4200   0 2.0   16   22    0 900   4800 14000 0 960   9700 7400 0 920   6800 10000 0 820   9800 11000 0 1.9  630 25   0 .97  630 12    0 .98  630 12    0 .96  630 12    0 47   1700 600 0 900    510   12000   0 1.0   18   13    -32 230   2700 2500 0 900   12000 11000 0 120   3100 1100 0
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i 160     15000 1200    0 16     190 190    0 850    2700 10000   0 5.2   27   58    0 340   5600 2800 0 120   2700 830 0 350   5200 3300 0 230   15000 2500 0 3.9  1100 46   0 1.9   1100 25    0 2.0   1100 22    0 1.9   1100 22    0 900   1700 10000 0 900    470   10000   0 19     55   210    -32 15   420 110 0 17   440 130 0 17   420 140 0
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i .93  220 9.8  0 6.8   55 85    0 5.0  270 56   0 4.1   9.6 52    0 460   5700 4900 0 960   4400 11000 0 960   4800 11000 0 21   210 260 0 .16 21 1.5 0 .088 21 .84 0 .11  21 .73 0 .074 21 .88 0 120   300 910 0 900    98   10000   0 .090 12   .78 -32 60   1200 480 0 900   12000 13000 0 64   1400 470 0
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i 1.2   270 14    0 34     160 380    1 850    1300 7200   0 4.9   10   60    0 900   7600 10000 0 940   4800 7800 0 960   5200 10000 0 7.3 410 89 0 92    15000 1100   0 .34  76 4.7  0 .33  76 4.4  0 .37  76 4.2  0 880   770 6100 0 900    110   9200   0 .19  12   2.2  -32 900   2600 6600 0 220   13000 2400 0 900   2800 5100 0
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i 1.1   81 10    0 3.0   130 1100    0 850    2800 4200   0 17     15   200    0 22   640 170 0 920   6500 8300 0 910   4600 10000 0 92   1000 1200 0 .29 48 3.1 0 .15  45 1.9  0 .15  45 1.8  0 .18  45 1.7  0 16   220 200 1 15    110   200   0 .73  15   9.3  -32 96   1800 740 0 180   11000 2100 0 97   1900 910 0
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i 4.3   1100 46    0 14     140 140    0 42    3300 450   0 12     13   140    0 900   11000 7600 0 960   10000 8600 0 960   8300 9800 0 16   470 220 0 900    7900 7000   0 .67  130 8.2  0 .76  140 9.0  0 .75  140 9.3  0 4.5 130 53 0 900    240   12000   0 .20  14   2.1  -32 60   1600 480 0 52   9100 560 0 62   1600 500 0
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i 8.9   2400 130    0 82     270 940    1 65    14000 850   0 12     15   150    0 900   6100 13000 0 960   6400 9400 0 960   12000 12000 0 900   720 11000 0 900    4000 5600   0 .66  130 7.8  0 .69  130 8.8  0 .67  140 7.1  0 13   160 140 1 900    260   9900   0 .16  14   1.9  -32 870   2700 11000 0 51   10000 440 0 900   2800 11000 0
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i 3.1   360 34    0 3.6   190 1100    0 36    700 470   0 8.0   11   91    0 190   4600 2100 0 960   4200 11000 0 910   4900 9200 0 31   250 370 0 .17 29 2.3 0 .12  29 1.1  0 .095 29 1.3  0 .10  29 1.1  0 24   220 230 0 900    230   11000   0 .55  13   7.0  -32 900   4200 13000 0 460   12000 5800 0 900   4300 11000 0
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i 4.8   1200 66    0 16     200 180    0 2.7  290 29   0 .98  11   11    0 57   1900 450 0 960   6500 7700 0 960   6600 9100 0 460   400 6000 0 .19 29 2.1 0 .12  29 1.0  0 .097 29 1.0  0 .12  29 1.1  0 12   170 140 1 70    15000   780   0 .62  13   7.9  -32 180   4700 1800 0 340   12000 3700 0 200   4700 2000 0
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i 46     2300 260    0 3.2   270 36    2 850    4200 6200   0 1.4   14   16    0 13   500 93 1 960   10000 6500 0 98   2900 1200 2 620   2100 6900 0 .86 210 11   0 .46  210 5.3  0 .49  210 5.2  0 .48  210 4.7  0 35   420 420 2 900    260   13000   0 .93  16   11    2 26   720 210 2 760   11000 9100 0 26   700 210 2
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i 16     2800 180    2 3.2   290 42    2 680    7100 6100   1 1.0   35   14    0 19   670 130 1 330   5300 2500 0 100   2000 1400 2 190   15000 2400 0 14    3900 190   0 7.1   3900 81    0 7.1   3900 110    0 7.0   3900 82    0 80   400 630 2 81    190   1200   0 47     83   540    2 130   2500 1400 2 900   9900 11000 0 130   2600 1400 2
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i 40     15000 460    0 7.6   710 89    2 850    810 3400   0 .58  10   6.7  0 9.5 440 74 1 570   5400 5600 0 98   710 1100 2 530   9200 6800 0 .38 51 3.7 0 .19  51 1.9  0 .21  51 1.8  0 .21  51 2.0  0 4.0 130 53 2 .68 38   7.1 2 .25  13   2.9  2 34   2000 240 2 900   13000 13000 0 36   2000 240 2
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i 85     15000 770    0 2.5   300 30    2 850    3500 4100   0 1.0   12   13    0 9.1 360 78 1 900   4600 9300 0 96   2900 1000 2 570   250 6700 0 .57 110 7.0 0 .34  110 3.2  0 .31  110 3.1  0 .30  110 3.2  0 3.4 130 37 2 900    130   9800   0 .19  14   2.3  2 16   540 120 2 900   2400 11000 0 15   540 110 2
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i .98  120 6.5  0 8.5   1100 110    2 850    2400 4100   0 1.0   11   12    0 12   500 94 1 960   6300 10000 0 960   6300 10000 0 85   260 1100 0 .55 96 6.8 0 .29  96 3.6  0 .32  96 3.6  0 1.1   96 2.5  0 4.7 180 58 2 900    210   12000   0 .76  13   8.8  2 86   5200 600 2 900   12000 12000 0 83   5200 570 2
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i 16     3400 180    1 4.1   500 53    1 850    3200 8100   0 12     54   140    0 25   1100 190 1 870   5700 7800 1 110   3200 1400 1 180   12000 2000 0 12    4700 150   0 5.8   4700 65    0 1.2   450 14    0 1.2   450 15    0 730   11000 6500 1 900    330   10000   0 110     120   1300    1 510   11000 5500 1 900   12000 11000 0 500   11000 5400 1
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i .25  35 2.4  0 8.2   770 100    2 850    2800 3000   0 .49  9.8 5.5  0 6.3 290 52 1 120   4000 910 2 100   3700 1200 2 890   1400 9500 0 900    11000 6300   0 900     1800 9800    0 900     2100 12000    0 2.0   110 29    0 2.3 100 32 2 900    180   12000   0 .087 12   1.1  2 13   530 100 2 810   11000 11000 0 13   530 110 2
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i 5.3   1600 60    2 3.1   580 41    2 850    1200 4900   0 1.6   12   17    0 11   480 100 1 76   2700 490 1 55   3100 490 2 890   3600 10000 0 900    12000 6500   0 900     2300 8300    0 900     2300 8100    0 2.4   170 4.7  0 4.3 130 61 2 .93 22   14   2 1.7   19   23    2 40   3000 340 2 260   11000 3200 0 37   2700 290 2
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i 82     14000 930    2 2.3   210 29    2 850    3000 7000   0 1.9   14   23    0 14   520 100 1 960   9200 6500 0 100   4100 970 2 500   3100 4900 0 1.2  320 12   0 .63  320 8.0  0 .59  320 6.5  0 .64  320 5.9  0 7.3 190 93 2 900    4100   11000   0 .22  17   2.5  2 31   960 230 2 900   12000 11000 0 32   910 290 2
ldv-linux-3.0/module_get_put-drivers-net-pppox.ko_true-unreach-call.cil.out.i.pp.i .53  44 5.2  2 1.2   29 13    2 850    3300 6300   0 .49  10   5.1  0 9.5 440 70 1 17   810 100 2 160   3600 1900 2 250   140 3600 0 56    15000 500   0 900     14000 13000    0 630     15000 7500    0 .15  36 1.9  0 880   250 8100 2 900    3600   9600   0 .099 12   .62 2 14   520 95 2 13   500 96 2 14   530 110 2
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i 21     15000 280    0 5.6   560 62    2 850    2600 4100   0 1.1   12   13    0 11   470 83 1 960   11000 5400 0 100   3800 1100 2 590   11000 6500 0 .67 160 9.3 0 .34  160 3.9  0 .35  160 4.0  0 .33  160 3.8  0 32   500 420 2 900    460   9300   0 .54  49   6.2  2 25   720 180 2 900   12000 11000 0 23   830 160 2
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i 52     4300 420    0 5.7   600 72    2 850    5900 4800   0 1.6   50   22    0 16   570 140 1 920   9800 5700 0 100   2700 1200 2 630   5400 6700 0 .92 230 10   0 .50  230 4.9  0 .50  230 5.7  0 .49  230 5.3  0 31   300 340 2 900    380   9700   0 1.9   24   21    2 31   1100 290 2 900   11000 13000 0 31   920 240 2
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i 38     15000 390    0 4.6   500 56    1 850    14000 7000   0 1.6   14   22    0 12   510 93 1 150   4400 1100 0 100   2800 1100 1 730   6900 8700 0 1.4  420 18   0 .73  420 8.0  0 .72  420 8.6  0 .75  420 11    0 38   1200 510 1 900    320   9100   0 .84  17   11    1 100   13000 1000 0 100   13000 1100 0 100   12000 980 0
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i 3.4   500 26    0 3.2   390 47    2 850    3400 8300   0 .92  48   11    0 9.9 410 79 1 910   10000 6400 0 98   1500 1200 2 900   4700 7100 0 900    12000 11000   0 900     2500 10000    0 900     2100 9000    0 51     610 520    0 5.3 140 66 2 900    220   11000   0 .31  14   3.7  2 24   820 190 2 900   12000 11000 0 25   800 190 2
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i .58  150 7.3  0 75     200 970    2 850    2100 5000   0 .089 9.6 .55 0 8.0 310 66 2 42   1600 330 2 15   530 140 2 4.1 200 57 -16 110    15000 1200   0 .99  55 2.1  -16 .27  55 3.3  -16 .27  55 3.1  -16 880   720 7100 0 900    170   9400   0 .087 12   .96 2 79   1400 660 2 900   13000 10000 0 110   1500 660 2
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i 31     15000 390    0 7.3   750 86    2 850    3200 5800   0 1.6   11   18    0 8.9 390 67 1 970   11000 6300 0 100   2700 1200 2 4.8 15000 48 0 900    3900 14000   0 900     5400 11000    0 260     3400 3400    0 260     3400 3300    0 3.9 130 59 2 900    390   11000   0 .22  14   2.4  2 19   730 170 2 110   12000 1200 0 21   570 140 2
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i 31     15000 350    0 6.6   690 93    1 850    4700 5900   0 2.2   13   30    0 13   480 100 1 300   6100 2100 0 100   1300 1200 1 900   5500 7800 0 21    15000 260   0 580     15000 7900    0 460     15000 5300    0 38     2400 450    1 5.0 150 63 1 900    460   8400   0 1.8   19   20    1 12   340 92 0 7.6 330 57 0 13   340 91 0
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i 6.6   1400 77    2 4.3   520 57    2 850    1000 3900   0 1.2   11   13    0 6.9 330 57 1 960   5300 13000 0 110   4900 960 2 690   15000 7500 0 300    15000 3400   0 69     15000 790    0 73     15000 950    0 16     800 180    2 2.9 120 39 2 1.7  20   20   2 .10  13   1.1  0 18   660 140 2 900   13000 10000 0 19   640 140 2
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i 1.2   87 9.9  0 5.8   490 66    2 850    1600 5500   0 1.4   11   16    0 10   470 84 2 940   8400 7800 0 900   8200 8900 0 510   4000 4400 0 .22 35 3.2 0 .14  35 1.1  0 .13  35 1.1  0 .12  35 1.1  0 4.2 140 59 2 770    250   9000   0 .38  13   4.2  2 21   560 160 2 49   11000 520 0 21   560 170 2
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i 7.2   150 53    0 5.8   530 80    1 850    2800 3800   0 3.1   15   37    0 14   510 110 1 270   5500 2000 0 100   1700 1400 1 540   3300 5400 0 .38 73 4.6 0 .23  70 2.9  0 .22  68 2.3  0 .23  71 2.1  0 28   300 400 1 900    230   12000   0 2.1   21   23    1 11   330 87 0 11   330 92 0 11   330 93 0
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i .90  260 11    0 1.6   170 900    0 850    1800 4800   0 .10  10   .66 0 24   1000 170 1 40   1600 300 2 170   4800 1500 2 900   300 14000 0 900    10000 9000   2 900     4200 13000    0 900     2300 2000    0 2.3   78 6.3  0 880   920 6200 0 900    140   9700   0 .24  12   2.6  2 48   1400 320 2 110   10000 1200 0 53   1400 350 2
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i 38     7600 450    -16 16     660 200    2 850    910 9300   0 1.7   12   21    0 11   460 80 2 160   4800 1200 2 97   2300 1100 2 890   1600 7200 0 94    15000 1000   0 900     5200 12000    0 900     2400 8700    0 30     600 380    0 880   1900 8400 0 900    140   13000   0 .74  14   8.7  2 48   2100 370 1 380   12000 4300 0 50   2000 370 1
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i 900     1500 9100    0 5.4   140 74    1 850    950 9400   0 1.2   11   15    0 14   520 110 1 75   2900 460 0 900   7300 8100 0 58   1100 720 -16 900    650 11000   0 .79  93 9.3  -16 .82  93 9.6  -16 .77  93 9.9  -16 890   420 7700 1 900    290   10000   0 .11  13   1.2  0 900   1400 12000 0 110   11000 1200 0 900   1400 10000 0
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i 32     6800 410    2 9.2   1100 110    2 850    14000 6500   0 2.7   15   30    0 13   490 97 2 970   11000 6100 0 99   1500 1300 2 520   2400 4900 0 .32 63 3.7 0 .19  62 1.8  0 .16  62 2.1  0 .17  62 2.1  0 6.4 150 92 2 900    290   11000   0 .63  17   8.0  2 30   1000 230 2 290   10000 3600 0 30   1000 230 2
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i 1.9   210 17    0 7.5   900 80    2 850    5700 6700   0 1.7   11   18    0 10   470 88 2 940   11000 6600 0 98   2600 1100 2 900   1900 12000 0 900    9900 6900   0 900     3200 11000    0 900     7100 11000    0 11     500 130    0 4.0 130 49 2 900    170   7700   0 .44  14   5.4  2 29   1500 240 2 300   11000 3600 0 31   1200 250 2
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 120     15000 870    0 1.5   170 22    0 850    4800 5500   0 900     89   12000    0 29   1600 230 0 960   8900 6800 0 38   920 340 1 890   14000 8900 0 140    15000 1800   0 900     2900 5700    0 900     2900 6500    0 900     2900 5100    0 240   800 2300 0 170    1500   2100   0 10     43   140    -32 770   15000 7600 0 900   12000 10000 0 660   7500 7700 0
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 170     1800 1300    0 18     140 230    1 4.5  1200 58   0 8.9   11   110    0 17   680 140 0 960   11000 9400 0 210   15000 2900 0 890   1000 6400 0 93    15000 1100   0 4.9   170 60    0 7.2   290 110    0 11     400 140    0 880   400 6500 0 900    1300   11000   0 .12  13   1.5  -32 900   1500 6700 0 900   2100 11000 0 53   1500 380 0
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 .94  75 8.4  0 19     160 240    0 15    420 210   0 .25  26   2.6  0 33   1100 220 0 370   15000 3200 0 18   740 140 1 890   2100 8200 0 900    5000 11000   0 3.2   170 43    0 3.2   170 36    0 900     4600 11000    0 35   240 380 1 61    72   680   0 .20  15   1.9  -32 900   4800 8900 0 900   12000 11000 0 210   4800 1900 0
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 1.6   310 15    1 1.5   75 18    1 1.3  130 14   1 .31  15   4.0  0 15   600 110 0 42   1700 260 1 17   600 170 1 900   670 12000 0 290    15000 3400   0 .88  190 7.6  1 .89  190 8.0  1 .93  190 9.2  1 890   1400 11000 0 1.5  28   18   0 .22  18   2.2  0 7.6 330 60 0 8.4 340 57 0 7.1 330 51 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 12     2500 120    0 10     800 120    0 75    14000 960   0 .63  24   7.8  0 18   880 150 0 160   4400 1200 0 61   2000 580 0 900   1100 13000 0 11    15000 130   0 2.1   440 26    0 2.1   440 25    0 2.2   440 20    0 900   5800 11000 0 740    160   7500   0 25     59   360    -32 900   14000 6100 0 900   11000 11000 0 900   14000 5200 0
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 46     5400 420    0 1.6   190 20    0 850    2800 2900   0 46     72   480    0 21   730 150 0 970   8600 6300 0 960   7900 8200 0 890   3200 12000 0 900    10000 11000   0 330     15000 3000    0 320     15000 3000    0 900     370 11000    0 81   740 810 0 900    320   10000   0 1.6   24   18    -32 900   5200 11000 0 900   2500 13000 0 900   5300 11000 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 19     5500 250    1 2.6   150 24    0 40    13000 450   0 10     14   110    0 10   490 75 0 25   1200 150 1 8.1 360 64 1 890   1100 6600 0 11    15000 130   0 .95  140 11    1 .92  140 13    1 .94  140 13    1 8.4 170 110 0 8.5  49   100   0 .32  15   3.9  -32 900   2800 11000 0 900   9600 11000 0 72   1200 650 0
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 900     8900 9100    0 9.8   150 110    0 45    13000 620   0 23     20   230    0 24   760 170 0 960   10000 7700 0 230   15000 2500 0 900   2400 2900 0 11    15000 130   0 2.9   190 33    0 3.4   200 48    0 3.4   210 44    0 880   260 12000 0 1.2  42   15   -32 .63  16   7.7  -32 47   1400 380 0 900   13000 11000 0 45   1500 410 0
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 1.2   100 10    0 .42  50 5.2  1 850    1100 6200   0 .63  130   6.2  0 11   530 79 0 29   990 170 1 9.0 390 72 1 880   6000 9900 0 11    15000 130   0 .90  330 9.5  0 .90  330 9.5  0 4.3   340 10    0 9.9 150 140 1 900    180   9300   0 .24  18   2.6  0 43   950 380 1 900   900 11000 0 44   940 410 1
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 27     5800 320    1 4.8   99 51    1 38    14000 500   0 2.5   13   32    0 15   540 110 0 960   12000 6600 0 30   1400 270 0 900   1500 13000 0 36    15000 410   0 .82  110 9.1  1 .83  110 9.8  1 .82  110 9.0  1 16   220 210 1 900    190   9800   0 .25  15   3.0  -32 900   4900 7400 0 900   5800 9300 0 900   4900 9000 0
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 1.6   200 14    0 .50  62 5.4  1 850    4900 4300   0 10     17   110    0 12   540 88 0 39   2100 260 1 9.4 400 68 1 86   420 700 0 9.6  15000 120   0 .62  120 7.2  0 .63  120 6.1  0 .65  120 6.8  0 19   240 260 1 900    460   9900   0 .30  16   3.6  -32 40   960 330 1 900   13000 10000 0 37   1100 300 1
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 130     15000 1100    0 260     560 2400    0 850    4400 7300   0 .99  37   10    0 31   990 260 0 950   11000 4800 0 17   730 130 1 900   2800 10000 0 900    5000 13000   0 24     1500 270    0 24     1500 240    0 900     1700 9800    0 710   1400 5600 0 32    130   420   0 .63  41   8.3  0 370   3500 4500 0 900   11000 9400 0 370   3900 4500 0
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 140     15000 1100    0 2.0   150 22    0 850    3700 5200   0 32     34   360    0 14   670 98 0 290   5700 2000 1 20   950 170 1 60   3000 590 0 10    15000 130   0 1.2   220 13    0 1.2   220 10    0 2.0   240 21    0 900   11000 11000 0 560    130   6000   0 30     61   350    -32 900   4600 9300 0 900   4700 9100 0 900   4600 9400 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 2.2   500 22    1 .25  37 3.1  1 44    13000 550   0 5.1   12   55    0 7.8 410 65 0 16   640 110 1 6.7 330 51 1 4.0 120 50 0 180    15000 2100   0 .32  60 3.7  1 1.2   60 3.1  1 .38  61 3.4  1 6.0 110 95 1 900    150   9500   0 .16  14   1.7  -32 14   500 110 1 390   9700 4500 0 15   510 100 1
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 290     8000 1700    0 1.5   120 20    0 850    3900 7500   0 27     32   340    0 15   560 120 0 120   4500 880 0 15   610 120 1 890   9200 4900 0 67    15000 840   0 1.2   230 11    0 3.9   230 7.9  0 1.2   240 13    0 890   1800 9600 0 900    320   12000   0 .24  21   2.8  0 900   5200 6800 0 900   2600 12000 0 900   4900 6400 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 100     2600 600    0 .76  92 8.6  0 130    13000 1300   0 .43  19   5.6  0 85   15000 920 0 260   5500 2000 0 12   430 86 1 890   14000 9000 0 900    2200 8300   0 52     640 750    0 51     640 560    0 53     660 550    0 890   570 7600 0 43    130   520   0 .72  22   7.7  -32 900   4000 11000 0 900   12000 12000 0 900   4300 11000 0
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 28     3400 280    0 5.1   550 57    0 850    3700 5000   0 50     35   560    0 900   6000 6200 0 960   14000 6400 0 930   11000 8000 0 890   6200 9300 0 11    15000 120   0 900     2100 9800    0 900     2400 8500    0 900     3600 9000    0 890   280 12000 0 900    210   10000   0 1.3   23   20    -32 900   4600 9100 0 900   1600 11000 0 870   6300 8900 0
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c 900     2200 12000    0 15     290 1100    0 4.2  440 52   0 46     19   540    0 3.7 280 27 0 17   1400 130 0 330   4500 3200 0 500   640 6800 0 .32 32 4.0 0 .16  32 1.9  0 .19  32 1.8  0 .16  32 2.3  0 31   280 390 0 .91 25   11   -32 .63  21   7.5  -32 12   350 96 0 13   350 100 0 12   350 100 0
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.c 1.2   170 10    0 .51  57 5.2  0 440    2400 2800   0 .62  91   6.8  0 4.2 270 31 0 16   1200 120 0 250   2900 2300 0 500   6300 6000 0 .29 30 3.1 0 .19  30 2.1  0 .19  30 1.8  0 .16  30 2.0  0 5.2 130 64 0 900    160   12000   0 .55  20   6.7  -32 12   350 99 0 12   340 85 0 12   350 110 0
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c 900     1800 12000    0 4.4   110 49    0 6.1  630 64   0 320     63   3500    0 5.3 310 38 0 18   1300 120 0 270   3500 2800 0 43   550 500 0 .40 36 4.8 0 .21  36 2.4  0 .24  36 2.5  0 .21  36 2.7  0 8.6 160 110 0 900    190   9100   0 .35  25   4.4  -32 13   350 93 0 12   350 97 0 12   340 100 0
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c 120     15000 880    0 1.1   140 14    0 850    2500 6300   0 .43  26   5.6  0 5.0 290 42 0 30   1900 220 0 390   4200 5200 0 12   15000 120 0 .50 39 6.1 0 .28  39 2.6  0 .24  39 2.7  0 .25  39 3.2  0 120   1000 1500 0 900    330   9800   0 1.4   30   18    -32 14   340 120 0 13   350 94 0 13   360 94 0
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c 2.8   270 20    0 .79  94 9.6  0 850    3800 4600   0 22     39   270    0 5.8 310 47 0 22   1600 180 0 280   4400 2800 0 28   270 330 0 .45 39 6.0 0 .22  39 2.8  0 .23  39 2.5  0 .26  39 2.4  0 34   270 480 0 900    470   9700   0 .39  26   5.1  -32 13   340 100 0 13   350 110 0 13   350 120 0
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c 14     3000 150    0 .57  69 6.8  0 7.5  1000 88   0 24     23   310    0 4.2 260 32 0 19   1100 140 0 270   2300 2900 0 27   370 340 0 .34 34 4.7 0 .21  34 2.1  0 .74  34 1.5  0 .74  34 2.0  0 9.6 210 150 0 4.8  34   61   0 .28  22   2.9  -32 12   350 97 0 13   350 110 0 12   360 96 0
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c 2.4   230 22    0 .55  63 7.9  0 1.8  180 17   0 25     32   280    0 4.5 260 37 0 19   1300 130 0 86   2600 900 0 23   310 290 0 .37 35 4.1 0 .22  35 2.3  0 .23  35 2.2  0 .19  35 2.3  0 4.1 110 55 0 900    130   10000   0 .26  22   4.0  -32 12   350 95 0 14   340 94 0 13   340 95 0
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 140     15000 990    0 160     8200 2400    0 850    13000 3800   0 100     21   1200    0 250   15000 2400 0 960   12000 6100 0 920   9800 7900 0 890   14000 10000 0 900    870 11000   0 530     2200 6600    0 530     2400 8100    0 900     840 11000    0 180   600 2000 0 27    79   350   0 1.8   22   24    -32 900   3900 11000 0 900   13000 12000 0 900   4200 10000 0
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 40     1100 310    0 .44  51 4.5  0 850    4000 4200   0 .20  14   2.5  0 21   730 160 0 970   12000 6400 0 910   8800 8300 0 260   4400 2700 0 .37 66 4.0 0 .18  66 1.9  0 .19  66 1.8  0 .18  66 1.9  0 25   300 310 0 13    100   150   0 .61  16   7.6  -32 350   1200 3100 0 860   12000 10000 0 50   920 400 0
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 430     5300 2300    0 900     6900 10000    0 850    3600 6000   0 8.0   18   90    0 900   4700 10000 0 960   11000 7000 0 930   9800 8800 0 570   13000 5100 0 .60 130 7.4 0 1.2   130 2.8  0 .34  130 3.5  0 .31  130 3.6  0 240   14000 2300 0 900    430   13000   0 1.3   21   16    -32 900   3700 5500 0 900   11000 11000 0 900   3900 4600 0
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 900     11000 10000    0 54     450 620    0 570    9100 3100   0 2.2   11   28    0 24   750 190 1 840   9800 6300 0 960   9200 9400 0 37   430 430 0 .23 44 2.4 0 .11  43 1.4  0 .15  44 1.3  0 .15  44 1.3  0 6.7 140 96 0 900    3800   11000   0 .23  14   2.4  -32 900   2900 9800 0 900   10000 11000 0 900   2900 7800 0
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 810     12000 6200    0 22     410 260    1 850    5700 5000   0 22     15   280    0 23   830 150 0 620   15000 4700 0 100   2000 1100 1 470   3600 6200 0 .47 100 6.8 0 .28  100 3.0  0 .28  100 2.8  0 .25  100 3.0  0 240   14000 2800 0 900    270   10000   0 .36  18   5.0  -32 51   1500 460 1 900   8900 11000 0 53   1300 440 1
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 900     8400 6000    0 1.1   130 15    0 850    7300 4100   0 32     15   420    0 19   680 150 1 960   12000 6100 0 110   3200 1200 1 900   6800 6000 0 230    15000 2800   0 900     1800 10000    0 900     2000 8000    0 160     710 1700    0 900   1100 7800 0 900    140   9900   0 .44  17   4.8  -32 120   1600 1000 0 900   11000 11000 0 79   1500 640 0
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 .80  210 8.9  2 .15  27 1.7  2 850    4700 4500   0 1.9   10   24    0 6.1 300 57 2 14   630 110 2 95   2300 1300 2 900   380 9500 0 210    8900 2400   2 900     1000 3300    0 670     15000 8300    0 .56  67 6.8  2 2.4 97 32 2 .47 15   5.8 2 .23  12   2.0  2 15   530 110 2 900   12000 10000 0 16   550 110 2
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 .25  37 2.6  2 .087 26 .96 2 850    14000 5600   0 1.5   9.5 16    2 4.9 290 45 1 4.9 290 36 2 3.7 270 28 2 6.5 280 66 2 53    3400 670   2 900     1300 13000    0 460     15000 6400    0 .23  32 2.6  2 1.6 78 21 2 .32 13   3.6 2 .077 11   .65 2 9.9 430 76 2 110   670 1200 2 9.2 410 65 2
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 .41  56 4.2  2 .087 22 1.0  2 850    14000 10000   0 1.7   9.7 22    2 5.1 290 49 1 5.6 290 46 2 4.0 270 34 2 900   760 10000 0 900    5800 7000   0 900     930 11000    0 900     3800 11000    0 .23  34 2.6  0 1.8 89 21 2 .40 14   4.7 2 .092 12   .95 2 13   540 92 2 900   12000 12000 0 13   550 95 2
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 .28  46 2.7  2 .079 21 .87 2 850    1600 6900   0 1.4   9.1 15    2 5.2 290 43 2 6.1 300 44 2 4.5 280 33 2 25   290 320 2 900    11000 7400   0 900     530 11000    0 900     2200 13000    0 .32  38 3.8  2 1.7 88 20 2 .33 13   4.0 2 .078 11   .90 2 9.8 400 66 2 200   11000 2400 0 9.3 400 70 2
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 .76  160 8.6  2 .10  27 1.2  2 850    14000 7000   0 1.6   9.4 19    2 5.2 290 44 1 6.3 320 52 2 4.0 270 30 2 890   1000 6900 0 900    5600 6700   0 900     950 13000    0 900     3600 13000    0 .25  34 3.4  0 1.8 84 22 2 .38 14   4.8 2 .10  12   1.1  2 13   510 96 2 900   9700 13000 0 13   520 96 2
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 .61  140 7.1  2 .13  27 1.4  2 850    14000 6600   0 2.0   10   26    2 5.3 290 44 2 6.7 340 48 2 4.3 280 39 2 10   280 110 2 240    15000 2500   0 900     960 11000    0 900     7200 9800    0 .40  49 4.4  2 2.0 77 27 2 900    110   10000   0 .092 12   1.1  2 12   520 89 1 900   12000 11000 0 12   550 86 1
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 .30  46 2.6  2 .087 24 1.2  2 850    3800 4600   0 2.0   9.8 23    2 5.0 280 44 2 5.5 330 45 2 3.9 270 35 2 8.1 280 71 2 130    4900 1500   2 900     1100 9800    0 900     15000 9600    0 .26  38 3.2  2 1.7 81 21 2 900    4100   9800   0 .078 12   .77 2 11   520 88 2 900   12000 11000 0 11   520 82 2
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 .30  45 4.6  0 .10  24 1.2  2 850    14000 5100   0 2.5   11   28    2 6.2 330 48 2 6.4 310 50 2 4.3 280 35 2 890   740 7200 0 510    8400 6200   2 900     1300 14000    0 900     2500 10000    0 .34  42 3.4  0 1.9 87 22 2 4.8  20   52   2 .10  13   .82 2 10   480 78 2 500   13000 6300 2 11   440 83 2
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 .41  54 3.1  2 .13  31 1.9  2 310    15000 1600   0 3.0   9.2 32    2 4.9 290 42 1 8.9 440 61 2 12   680 91 2 450   170 6200 0 11    15000 110   0 900     6300 11000    0 870     15000 10000    0 .28  37 3.5  2 2.2 89 31 2 .43 19   3.5 0 .086 11   1.1  2 12   510 92 2 69   740 800 2 13   510 100 2
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 .29  46 2.5  2 .092 22 .98 2 850    13000 10000   0 1.7   9.7 22    2 4.9 290 43 2 5.1 290 42 2 3.8 270 33 2 890   510 7700 0 420    15000 2800   0 900     1700 8100    0 900     8100 11000    0 .27  34 2.5  2 1.7 84 23 2 .42 14   4.3 2 .080 12   .86 2 9.8 440 79 2 680   11000 7800 0 11   440 75 2
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 .17  29 1.3  2 .069 19 .78 2 850    4700 4000   0 .86  8.3 9.5  2 4.1 290 32 1 4.2 290 37 2 3.2 260 27 2 4.8 280 45 2 1.5  170 17   2 900     550 2900    0 600     15000 4900    0 .19  28 1.6  2 1.7 88 22 2 .22 11   2.9 2 .092 11   1.1  2 6.9 370 53 2 8.0 360 60 2 7.4 350 60 2
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 1.8   480 20    2 .21  30 2.2  2 850    14000 7900   0 1.8   9.4 19    2 5.8 290 46 2 43   1700 280 1 96   2400 1100 2 320   5100 3600 2 480    15000 1500   0 900     1800 13000    0 900     4400 14000    0 2.2   220 27    2 3.3 120 44 2 900    3600   8300   0 .11  12   .84 2 13   530 92 2 120   810 1200 2 13   510 100 2
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 28     15000 310    0 3.1   270 38    2 850    14000 6900   0 5.8   14   60    2 11   460 82 2 910   11000 6800 0 100   4100 1300 2 890   10000 10000 0 11    15000 120   0 900     2700 13000    0 900     6500 10000    0 360     7400 4200    2 33   450 420 2 900    250   11000   0 .14  16   1.5  2 23   710 180 2 900   1600 9900 0 25   700 170 2
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 4.7   1200 65    2 .32  34 3.5  2 850    14000 5600   0 3.0   10   34    2 7.5 310 57 2 190   5700 1400 1 95   1800 1100 2 890   2800 7600 0 270    15000 3000   0 900     2100 11000    0 900     5100 11000    0 6.1   550 73    2 5.7 200 74 2 900    300   9100   0 .099 13   1.1  2 18   560 140 2 260   1100 3300 2 16   540 120 2
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 6.5   1700 73    2 .35  36 4.8  2 850    14000 5100   0 3.6   11   40    2 9.5 360 71 2 80   4500 520 1 96   1800 1300 2 900   8200 12000 0 240    15000 2900   0 900     1500 11000    0 900     3600 11000    0 7.4   500 92    2 7.6 240 96 2 900    3500   8500   0 .15  13   1.2  2 18   620 140 2 170   1400 1900 2 18   640 130 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 39     10000 420    2 1.6   150 18    2 850    14000 5200   0 4.3   48   50    2 8.9 360 71 2 910   11000 6300 0 100   4200 1200 2 890   14000 12000 0 150    15000 1600   0 900     3200 10000    0 900     7300 13000    0 90     3100 1100    2 880   620 12000 0 900    3500   8900   0 .13  14   1.4  2 20   630 150 2 300   2400 3800 2 21   650 170 2
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 15     4000 190    2 .74  70 8.1  2 850    14000 4900   0 3.0   11   34    2 7.7 320 63 2 210   5300 1600 1 98   4000 960 2 900   11000 12000 0 140    15000 2000   0 900     2900 10000    0 900     5400 11000    0 35     2000 390    2 880   560 11000 0 900    3300   8700   0 .11  13   1.0  2 17   650 130 2 230   880 3000 2 18   550 140 2
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 1.2   310 11    2 .17  30 2.1  2 850    14000 11000   0 1.4   9.1 16    2 5.4 300 45 2 26   960 160 1 97   3600 1000 2 390   7800 4800 2 140    15000 1800   0 900     2200 10000    0 900     5500 11000    0 1.4   140 16    2 2.9 120 41 2 .32 12   3.8 2 .076 11   .82 2 11   490 82 2 110   840 1300 2 12   490 98 2
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 3.5   950 42    2 .27  34 3.4  2 850    14000 6200   0 2.5   10   26    2 6.9 300 55 2 30   1500 210 1 96   2300 1300 2 360   4100 4700 2 180    15000 1900   0 900     1800 12000    0 900     4600 9600    0 4.0   380 55    2 4.3 150 53 2 900    3400   8200   0 .12  12   1.0  2 16   550 110 2 92   980 1000 2 15   510 110 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 22     5300 260    2 .72  67 8.3  2 850    14000 4800   0 4.9   13   66    2 11   410 71 2 280   7900 2100 1 99   3800 1100 2 900   15000 10000 0 96    15000 1000   0 900     3800 11000    0 900     8700 14000    0 28     1600 430    2 62   390 930 2 900    3500   8700   0 .15  15   1.4  2 22   700 180 2 350   1300 4100 2 22   670 160 2
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 17     4300 190    2 .63  59 7.8  2 850    14000 4900   0 4.5   12   52    2 10   400 81 2 240   7400 1700 1 98   3700 990 2 900   15000 12000 0 100    15000 1300   0 900     4100 11000    0 900     7600 11000    0 24     1600 320    2 57   420 890 2 900    3300   9500   0 .12  15   1.7  2 21   660 150 2 270   1200 3000 2 21   790 160 2
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 21     5400 230    2 1.0   100 14    2 850    14000 7600   0 4.4   13   60    2 9.5 380 73 2 240   7300 1600 1 98   2600 1100 2 900   8800 10000 0 120    15000 1300   0 900     2800 11000    0 900     5500 11000    0 31     1800 380    2 9.8 380 140 2 900    340   11000   0 .12  15   1.3  2 21   660 160 2 330   1200 4300 2 21   800 180 2
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 1.3   360 15    2 .17  30 2.2  2 850    14000 7700   0 1.6   9.1 18    2 5.4 290 41 2 37   1600 230 1 110   1300 200 2 590   6400 7200 2 150    15000 1500   0 900     1900 12000    0 900     4700 10000    0 1.4   140 21    2 2.9 120 35 2 .34 12   3.2 2 .11  11   .89 2 12   510 82 2 68   800 700 2 12   520 100 2
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 8.9   2300 110    2 .40  39 4.8  2 850    14000 7200   0 4.3   11   53    2 8.9 360 63 2 38   1700 240 1 96   2400 1000 2 740   9000 8300 2 220    15000 2800   0 900     1500 10000    0 900     3500 12000    0 8.1   490 91    2 6.0 160 93 2 900    3600   9200   0 .11  14   1.2  2 20   650 150 2 97   1700 1100 2 20   670 160 2
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 28     15000 350    0 1.4   120 17    2 850    14000 5300   0 10     24   110    2 17   650 120 2 190   14000 1500 1 100   2800 1300 2 890   10000 12000 0 10    15000 130   0 900     3000 9500    0 900     6300 9500    0 120     4300 1200    2 23   590 300 2 900    3600   7500   0 .19  19   2.3  2 35   1100 240 2 350   3300 4100 2 35   1000 270 2
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 .16  28 1.0  0 .070 20 .89 0 850    14000 3900   0 .82  8.4 9.8  2 4.5 290 37 2 6.5 320 48 2 4.2 270 33 2 8.3 280 72 2 440    8600 5500   2 900     2300 10000    0 900     9300 11000    0 .23  31 2.6  2 1.7 90 21 2 .24 11   3.0 2 .077 11   .67 2 9.4 430 63 2 90   640 1100 2 8.8 410 69 2
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 .70  120 6.7  2 .18  29 2.4  2 850    13000 4600   0 2.3   9.8 27    2 5.5 290 47 1 14   560 93 2 8.6 440 66 2 21   440 210 2 220    15000 2700   0 900     3000 11000    0 900     13000 12000    0 .47  69 5.5  2 2.5 100 28 2 900    3700   11000   0 .46  12   6.0  2 22   1000 180 2 900   10000 11000 0 21   930 160 2
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 .26  35 2.5  2 .093 25 1.1  2 850    4700 3800   0 1.3   9.2 15    2 4.4 290 34 1 4.6 310 39 2 3.4 270 32 2 480   280 6600 2 1.7  190 21   2 900     850 8000    0 460     15000 5600    0 .18  32 2.0  2 1.8 76 26 2 .28 11   3.5 2 .12  11   1.6  2 7.5 350 55 2 45   470 470 2 7.6 350 58 2
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 3.3   1100 36    2 .56  78 7.0  2 850    14000 6700   0 2.2   10   30    2 6.8 310 59 2 59   2600 460 2 100   3700 1100 2 900   1900 9400 0 93    15000 1100   0 900     640 11000    0 900     1100 12000    0 2.0   190 23    2 2.5 100 29 2 .49 16   5.8 2 .16  12   1.8  2 15   550 110 2 900   9500 11000 0 15   540 110 2
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 1.2   300 13    2 .22  34 2.4  2 850    13000 7800   0 2.1   9.9 26    2 6.0 290 56 1 7.4 430 55 2 4.9 290 41 2 500   3000 5900 2 260    15000 3200   0 900     5500 11000    0 520     15000 6800    0 1.7   250 21    2 2.5 87 28 2 .43 15   5.7 2 .10  12   .93 2 17   540 130 2 6.4 310 47 0 15   500 120 0
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 .25  42 3.3  2 .085 20 .98 2 850    4500 4400   0 .59  8.6 6.5  2 3.9 280 30 1 4.7 290 36 2 3.2 260 28 2 5.5 270 61 2 550    11000 8100   2 900     920 13000    0 900     11000 11000    0 .21  27 2.5  2 3.3 150 42 2 .22 9.9 1.8 2 1.1   15   13    2 7.9 360 54 2 130   520 1700 2 8.6 380 69 2
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 .13  26 1.3  2 .059 18 .59 2 850    14000 4400   0 .42  8.2 5.1  2 3.6 290 32 1 3.7 290 30 2 2.9 260 25 2 4.2 260 45 2 31    1700 380   2 900     1100 10000    0 530     15000 7400    0 .14  25 1.1  2 1.5 79 17 2 .20 9.9 2.1 2 .091 12   .66 2 7.5 350 58 2 130   3400 1800 2 7.4 360 62 2
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 1.4   310 14    2 .18  32 2.8  2 850    14000 8400   0 2.9   11   33    2 6.9 320 62 2 19   680 130 2 18   690 160 2 180   690 1500 2 440    15000 5900   0 900     450 2300    0 900     3800 13000    0 .98  110 11    2 2.3 96 33 2 900    80   13000   0 .40  13   5.2  2 14   540 100 2 500   5400 5700 2 15   550 120 2
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 .17  31 1.7  2 .068 19 .65 2 850    13000 5000   0 .80  8.5 11    2 4.0 280 34 1 4.9 300 36 2 3.4 270 28 2 5.5 280 59 2 6.0  590 74   2 900     1500 7600    0 380     15000 5700    0 .18  28 1.9  2 1.7 97 20 2 .25 11   2.5 2 .14  44   1.1  2 8.4 400 65 2 450   8500 5000 0 8.3 410 65 2
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 4.7   1300 58    2 .35  40 4.0  2 850    3400 6000   0 3.8   11   49    2 8.7 410 73 1 100   4400 860 2 97   920 1300 2 890   830 6300 0 900    2800 8200   0 900     680 9600    0 .83  89 11    0 .83  90 9.7  0 3.4 110 45 2 900    130   11000   0 .25  14   3.2  2 21   660 140 2 900   9700 11000 0 20   640 150 2
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 .23  30 1.6  2 .11  22 .98 2 850    13000 9300   0 .77  8.5 11    2 4.3 280 39 1 6.9 380 52 1 95   1200 1100 2 900   430 7500 0 160    15000 1800   0 900     2800 10000    0 420     15000 5300    0 .22  29 2.0  2 1.8 82 24 2 .23 10   2.1 2 .087 11   1.1  2 12   550 95 2 900   12000 10000 0 13   510 91 2
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 .52  85 4.7  2 .12  22 .89 2 850    1500 5700   0 1.2   9.7 14    0 5.1 290 40 2 6.8 360 48 2 4.2 270 31 2 18   290 210 2 790    15000 8200   0 900     1300 11000    0 900     8600 11000    0 .36  43 5.0  2 1.7 81 20 2 .33 12   3.5 2 .084 11   .83 2 9.7 430 73 2 310   540 3800 2 10   440 75 2
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 .28  34 2.1  2 .11  19 .72 2 850    14000 7600   0 1.2   9.5 14    2 4.4 290 37 2 4.8 290 43 2 3.5 270 33 2 6.0 280 65 2 130    4800 1700   2 900     1300 12000    0 900     14000 11000    0 .17  32 2.6  2 1.6 94 23 2 .31 12   3.9 2 .096 11   .77 2 10   460 80 2 480   12000 6200 0 9.4 420 71 2
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 .56  95 5.3  2 .075 20 .82 2 850    2300 6000   0 .94  9.8 11    0 4.9 280 44 2 6.5 340 46 2 4.2 270 32 2 18   280 210 2 870    15000 9400   0 900     1200 11000    0 900     8600 12000    0 .37  42 4.5  2 1.7 89 22 2 .32 12   4.2 2 .11  11   .85 2 9.9 450 77 2 230   520 2900 2 9.8 410 75 2
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 .34  60 3.1  2 .11  19 .61 2 850    13000 11000   0 .90  9.2 11    2 4.4 290 36 2 5.3 300 42 2 3.5 270 30 2 7.8 280 88 2 360    15000 2800   0 900     1400 11000    0 900     9300 12000    0 .24  33 2.5  2 1.6 79 21 2 .27 11   2.9 2 .066 11   .76 2 8.5 390 71 2 140   1100 1900 2 8.3 380 61 2
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 .63  150 7.8  2 .098 26 1.4  2 850    1900 6800   0 1.1   8.8 14    2 4.9 290 40 2 11   510 80 1 96   2300 1300 2 890   830 8100 0 220    15000 2400   0 900     1100 13000    0 900     4900 11000    0 .61  58 7.7  2 2.0 96 26 2 .31 12   3.0 2 .097 11   1.2  2 10   430 75 2 210   850 2900 2 10   450 70 2
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 .22  39 1.9  2 .091 22 1.0  2 850    5400 6300   0 2.0   11   28    2 5.0 290 42 2 5.2 290 39 2 4.1 300 34 2 5.9 280 56 2 15    670 190   2 900     910 11000    0 640     15000 8700    0 .21  36 1.9  2 1.6 74 24 2 .47 15   6.9 2 .074 12   .81 0 8.4 370 63 2 8.4 360 68 2 8.4 360 62 2
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 6.3   1600 66    2 .36  43 3.7  2 850    13000 7100   0 2.7   11   36    2 7.1 330 56 2 16   740 99 2 8.6 420 69 2 890   2100 7500 0 900    8800 7200   0 900     710 11000    0 900     2900 11000    0 2.0   160 26    2 2.5 98 33 2 900    440   10000   0 .12  13   1.1  2 13   510 90 2 900   12000 12000 0 13   520 99 2
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 .25  37 1.8  2 .083 22 1.1  2 850    4300 3800   0 1.8   9.7 27    2 4.9 280 43 1 4.6 290 36 2 3.6 270 30 2 5.6 270 60 2 1.8  200 23   2 900     780 7100    0 550     15000 6700    0 .18  35 2.0  2 1.6 74 19 2 .39 15   5.0 2 .080 12   .78 2 11   510 80 2 900   10000 11000 0 11   520 89 2
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 .19  33 1.8  2 .11  20 .70 2 850    1400 8000   0 1.3   9.1 17    2 4.7 290 37 2 4.6 290 34 2 3.7 270 27 2 5.7 270 65 2 25    1200 330   2 900     1100 10000    0 660     15000 7800    0 .16  31 1.5  2 1.5 80 22 2 .31 14   4.0 2 .065 11   .64 2 8.4 380 60 2 320   11000 4000 2 8.7 390 63 2
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 .35  59 3.1  2 .071 19 .85 2 850    13000 6700   0 1.2   9.1 13    2 4.7 290 38 1 4.8 300 39 2 3.3 270 29 2 8.5 280 96 2 330    15000 3300   0 900     3500 11000    0 800     15000 9500    0 .32  53 4.6  2 1.6 74 21 2 .42 20   3.3 2 .089 11   .63 2 9.2 410 64 2 140   5300 1700 2 10   430 76 2
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 .71  170 6.7  2 .091 30 1.1  2 850    13000 6900   0 1.2   9.7 15    2 4.9 290 40 1 5.7 300 40 2 4.1 270 31 2 59   750 660 2 450    15000 6100   0 900     10000 9300    0 370     15000 4500    0 3.0   540 41    2 1.6 75 18 2 .29 12   3.6 2 .069 11   .68 2 9.5 430 64 2 140   3800 1800 2 11   430 81 2
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 .20  30 1.4  2 .062 19 .72 2 850    6000 5300   0 1.0   8.8 12    2 4.2 290 33 1 4.5 290 32 2 3.1 270 28 2 4.9 280 54 2 43    2100 500   2 900     1600 9500    0 900     6000 2300    0 .14  29 1.7  2 1.5 78 19 2 .26 12   3.0 2 .066 11   .61 2 8.1 370 68 2 130   5600 1400 2 8.3 370 61 2
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 .34  64 3.4  2 .076 19 .76 2 850    14000 6000   0 1.1   8.9 14    2 5.1 290 40 1 4.7 290 40 2 3.5 270 28 2 8.2 270 90 2 800    15000 11000   0 900     2600 11000    0 900     12000 10000    0 .32  46 3.4  2 1.6 76 19 2 .31 12   3.3 2 .071 11   .79 2 8.5 390 65 2 170   5200 2300 2 8.8 400 61 2
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 .92  240 9.1  2 .12  28 1.0  2 850    14000 6900   0 1.3   8.9 13    2 4.9 290 42 1 5.5 290 44 2 3.9 270 30 2 40   490 450 2 320    15000 4200   0 900 &#x