Tool 2LS 0.3.4 BLAST 2.7.3 CBMC CPAchecker 1.4-svcomp16c CPAchecker 1.4-svn 18373 CPAchecker 1.4-svcomp16c ESBMC ESBMC version 2.0.0 64-bit x86_64 linux DepthK ESBMC+DepthK version 2.1 CPAchecker 1.4-svn 18356M SeaHorn-F16 0.1.0 SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8
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-22-generic Linux 4.2.0-23-generic Linux 4.2.0-22-generic Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]] 2016-01-03 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]] 2016-01-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]] 2016-01-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]]
Run set 2ls.sv-comp16.DeviceDriversLinux64 blast.sv-comp16.DeviceDriversLinux64 cbmc.sv-comp16.DeviceDriversLinux64 cpa-bam.sv-comp16.DeviceDriversLinux64 cpa-kind.sv-comp16.DeviceDriversLinux64 cpa-refsel.sv-comp16.DeviceDriversLinux64 cpa-seq.sv-comp16.DeviceDriversLinux64 esbmc.sv-comp16.DeviceDriversLinux64 esbmcdepthk.sv-comp16.DeviceDriversLinux64 lpi.sv-comp16.DeviceDriversLinux64 seahorn.sv-comp16.DeviceDriversLinux64 smack.sv-comp16.DeviceDriversLinux64 symbiotic3.sv-comp16.DeviceDriversLinux64 uautomizer.sv-comp16.DeviceDriversLinux64 ukojak.sv-comp16.DeviceDriversLinux64
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -lpi-svcomp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i error(signal 6) 2.6   290 false(reach) 2.5   110 false(reach) 5.1  540 timeout 900   4400 false(reach) 67   1700 false(reach) 160   1100 false(reach) 220   3700 unknown 18     4900 unknown 62    4900 witness unconfirmed 53   1200 false(reach) 3.0  380 witness unconfirmed 110   370 unknown 5.2   94   unknown 31   490 unknown 33   460
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i killed by signal 9 430     15000 witness timeout 6.3   86 error 210    430 timeout 900   4200 timeout 900   8200 false(reach) 150   1200 unknown 520   5900 unknown .76  170 unknown 16    350 timeout 900   9000 witness timeout 74    440 timeout 890   590 unknown .78  35   timeout 900   2000 error 170   7300
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i error (6) 3.6   380 exception (gremlins) 63     300 true 850    2900 timeout 900   2200 timeout 900   5400 timeout 900   1200 timeout 900   2000 unknown 1.2   260 unknown 890    1600 error (recursion) 36   770 witness timeout 3.3  330 timeout 890   400 unknown 1.5   46   error 210   3200 error 150   7000
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i error (6) 1.2   100 witness timeout 13     220 witness unconfirmed 39    1900 timeout 900   5100 timeout 900   7800 timeout 900   980 timeout 900   6500 unknown 2.3   650 unknown 11    720 error (recursion) 33   840 witness timeout 5.6  190 witness timeout 19   220 unknown 1.9   41   unknown 16   380 unknown 18   370
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i killed by signal 9 120     15000 witness unconfirmed 7.9   140 error 850    1900 timeout 900   4900 timeout 900   5800 timeout 900   1500 timeout 900   5600 unknown 2.3   690 unknown 9.8  730 error (recursion) 38   880 witness timeout 2.7  140 error (1) 30   110 timeout 900     120   unknown 15   360 unknown 13   330
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i error (6) 1.9   170 witness timeout 35     230 error 850    1100 witness timeout 29   910 error 160   4700 false(reach) 62   1300 unknown 310   5500 unknown 1.3   300 unknown 460    1200 error (recursion) 30   640 witness timeout 5.2  170 witness timeout 20   290 unknown 1.4   61   timeout 900   2100 error 71   6500
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i killed by signal 9 63     15000 witness timeout 42     160 error 49    12000 witness timeout 30   920 timeout 900   8200 timeout 900   2100 unknown 860   6500 unknown .93  230 unknown 6.8  370 timeout 910   8700 witness timeout 14    510 witness timeout 14   220 unknown .76  41   timeout 900   3300 error 66   6600
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i timeout 900     3500 witness timeout 100     660 error 850    1000 timeout 900   5900 error 110   3400 timeout 900   4300 timeout 900   4700 unknown 4.4   900 unknown 900    9400 error 81   1700 true 110    2400 witness timeout 32   450 unknown 3.8   110   error 230   3100 error 76   5700
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i killed by signal 9 140     15000 witness timeout 29     210 error 850    1200 error 45   990 timeout 900   10000 timeout 900   1000 timeout 900   7700 unknown 4.7   1500 unknown 19    1600 error (recursion) 45   920 timeout 900    260 witness timeout 120   620 unknown 2.9   51   timeout 900   2700 error 300   8000
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i witness unconfirmed 1.6   250 witness timeout 12     72 witness unconfirmed 3.4  220 timeout 900   4000 witness unconfirmed 77   1800 false(reach) 88   920 false(reach) 74   1600 unknown 900     14000 unknown .98 92 witness unconfirmed 32   680 witness timeout 64    140 timeout 880   810 timeout 900     110   unknown 9.8 330 unknown 10   330
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i witness timeout 2.0   310 false(reach) 64     180 true 850    1100 timeout 900   4100 timeout 900   7300 timeout 900   980 timeout 900   5600 out of memory 140     15000 unknown .99 110 timeout 900   8300 witness timeout 98    190 timeout 880   930 timeout 900     110   unknown 11   340 unknown 10   340
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i error (6) .82  65 timeout 5.7   180 error 850    1200 timeout 900   4600 error 35   1100 false(reach) 45   850 unknown 55   1200 unknown 1.7   420 unknown 7.3  540 error 22   800 false(reach) 4.7  220 witness timeout 21   220 unknown 690     220   unknown 21   840 unknown 20   960
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i witness timeout 6.3   1200 exception (gremlins) 23     150 error 160    13000 timeout 900   4400 false(reach) 420   3700 timeout 900   3300 false(reach) 430   3800 unknown 900     8800 unknown 1.6  170 witness unconfirmed 410   3400 witness timeout 2.6  140 witness timeout 8.6 150 witness timeout 390     130   unknown 12   360 unknown 11   370
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i witness timeout 13     2600 false(reach) 120     290 error 240    13000 false(reach) 30   840 unknown 43   1700 false(reach) 39   880 out of memory 190   15000 unknown 1.3   470 unknown 1.6  190 exception 25   580 false(reach) 62    190 witness unconfirmed 21   180 timeout 900     92   unknown 51   4600 unknown 46   4500
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i witness timeout 59     580 timeout 7.4   190 witness timeout 47    610 timeout 900   4500 witness unconfirmed 68   1400 timeout 900   1900 witness unconfirmed 230   4200 unknown 900     13000 unknown 1.2  130 witness unconfirmed 40   760 witness timeout 5.7  95 witness timeout 22   210 timeout 900     120   unknown 10   370 unknown 11   380
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i timeout 900     2100 exception (gremlins) 27     260 witness timeout 3.4  330 timeout 900   7700 timeout 900   7100 timeout 900   950 false(reach) 510   6100 out of memory 19     15000 unknown 1.5  160 witness unconfirmed 17   550 witness timeout 21    210 witness timeout 18   190 unknown 1.0   32   unknown 12   370 unknown 11   360
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i error (6) 5.4   570 true 3.8   280 error 850    1700 true 28   920 timeout 900   2900 true 39   940 true 110   3700 unknown 1.4   330 unknown 900    10000 error (recursion) 35   770 true 5.1  400 true 54   1200 timeout 900     150   true 40   630 error 74   7600
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i true 22     3200 true 3.8   300 true 850    1600 true 46   1000 timeout 900   5800 true 56   1300 true 120   3700 unknown 18     4900 out of memory 500    15000 timeout 900   8200 true 3.7  380 true 110   360 unknown 3.8   89   true 130   1800 error 86   6800
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i killed by signal 9 52     15000 true 10     710 true 850    580 true 13   620 timeout 900   6300 true 68   1100 true 100   750 unknown .91  340 unknown 1.5  99 timeout 910   8800 true 2.0  110 true 7.1 190 unknown .70  30   true 32   640 error 46   5800
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i error (6) 60     7700 true 4.2   300 error 850    1500 true 16   600 timeout 900   6100 true 21   680 true 100   3800 out of memory 300     15000 unknown 900    13000 timeout 910   11000 true 1.5  120 true 6.9 180 unknown 1.3   41   true 23   410 timeout 93   1200
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i error (6) .70  57 true 11     1100 true 850    1000 error 11   410 timeout 900   5400 error (recursion) 18   580 error 340   4400 unknown 5.9   160 unknown 2.5  180 timeout 900   11000 true 1.5  85 true 8.3 180 unknown .95  26   true 46   1300 error 39   800
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i true 22     3700 true 5.5   490 true 850    2600 true 83   1800 true 260   4200 true 210   1400 true 130   3800 unknown 1.9   760 true 150    7900 error (recursion) 740   7600 true 4.9  570 true 380   950 unknown 7.7   130   true 270   5100 error 100   3400
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i error (6) .28  36 true 12     770 true 850    660 true 9.6 470 timeout 910   8100 true 22   660 true 96   3800 unknown .35  81 unknown 1.4  96 error (recursion) 10   400 true .72 80 true 4.7 99 timeout 900     150   true 17   480 error 85   9900
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i true 14     3400 true 4.6   580 true 850    590 true 19   730 true 63   1600 true 77   830 true 76   4000 unknown .80  220 unknown 900    6800 true 180   4300 true 1.2  130 true 8.1 150 unknown 17     26   true 41   750 error 160   7900
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i true 100     15000 true 4.0   270 true 850    2200 timeout 900   10000 timeout 900   7500 true 39   970 true 110   4300 unknown 1.7   480 unknown 890    4600 timeout 910   8600 true 6.0  250 true 15   270 timeout 900     380   true 50   760 error 52   6100
ldv-linux-3.0/module_get_put-drivers-net-pppox.ko_true-unreach-call.cil.out.i.pp.i true .91  50 true 1.5   31 true 710    780 timeout 900   3900 timeout 900   6000 true 39   560 true 460   5200 true 1.5   210 true 2.0  77 true 12   450 true .60 41 true 880   250 timeout 900     280   unknown 17   450 unknown 18   370
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i killed by signal 9 310     15000 true 7.1   560 true 850    1200 true 20   760 timeout 900   8500 true 42   1000 true 110   4400 unknown 1.2   260 unknown 900    9200 timeout 910   8900 true 3.5  160 true 18   350 timeout 900     180   true 35   600 error 74   8200
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i error (6) 12     1300 true 7.6   600 error 850    1800 true 37   960 timeout 910   8400 true 68   1200 true 120   3800 unknown 1.7   370 unknown 890    3400 timeout 900   9100 timeout 900    84 true 40   690 unknown 1.6   77   true 44   860 error 96   8500
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i killed by signal 9 200     15000 true 7.0   500 true 850    1000 true 25   870 timeout 900   7500 true 65   1100 true 110   3700 unknown 4.0   1900 unknown 900    9500 timeout 900   9400 true 3.4  130 true 43   960 unknown 170     62   error 57   6700 error 60   7600
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i error (6) 1.7   160 true 4.4   390 error 850    1400 true 15   640 timeout 910   8900 true 59   1100 true 110   3500 out of memory 360     15000 unknown 900    13000 timeout 900   8500 true 3.6  130 true 7.8 150 timeout 900     170   true 32   770 error 46   6000
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i false(reach) 1.1   180 true 100     250 true 850    1100 true 15   600 true 160   3500 true 37   810 true 160   3600 unknown 900     13000 unknown .84 85 timeout 900   4500 true 6.8  87 timeout 880   750 unknown 220     24   unknown 10   330 unknown 10   330
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i killed by signal 9 48     15000 true 9.8   750 true 850    570 true 14   550 timeout 900   9300 true 56   1500 true 100   3800 out of memory 120     15000 unknown 190    1600 timeout 900   9800 true 2.2  130 true 29   220 timeout 900     41   true 38   620 error 54   6200
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i killed by signal 9 40     15000 true 8.3   690 true 850    1200 true 69   850 timeout 900   7500 true 74   1100 true 110   2400 out of memory 21     15000 unknown 2.0  460 timeout 910   8500 true 1.9  86 true 8.9 170 timeout 900     160   error 54   6800 error 60   6500
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i true 11     1900 true 6.5   520 true 850    1000 true 10   460 true 150   4500 true 29   950 true 100   4700 unknown .38  89 out of memory 200    15000 timeout 900   10000 true 1.4  80 true 6.2 110 timeout 900     17   unknown 12   340 unknown 12   350
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i error (6) .68  49 true 7.5   490 error 850    1400 error 9.8 380 timeout 900   2200 error (recursion) 11   360 error 310   1900 unknown 22     1300 unknown 900    5000 error (recursion) 60   1700 true 2.1  90 true 8.3 220 timeout 900     130   true 30   490 error 42   6000
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i error (6) 1.2   100 true 7.7   530 true 850    950 true 39   990 timeout 900   6200 true 98   2800 true 110   3600 unknown 1.6   420 unknown 900    1300 timeout 900   9200 true 6.5  290 true 36   440 timeout 900     410   unknown 19   410 unknown 18   390
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i false(reach) 1.7   330 timeout 3.2   180 true 850    1000 timeout 900   5000 timeout 910   12000 true 19   620 true 500   8400 true 150     5000 unknown 1.1  100 timeout 900   7700 true 1.1  78 timeout 880   820 timeout 900     18   unknown 11   330 unknown 11   360
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i error(signal 6) 44     8300 true 530     1400 error 140    14000 exception 11   410 exception 86   2300 exception 14   450 false(reach) 120   3600 out of memory 35     15000 unknown 2.5  280 timeout 900   8800 timeout 900    1500 false(reach) 360   880 timeout 900     160   unknown 13   370 unknown 13   360
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i killed by signal 9 290     15000 true 11     140 true 850    770 timeout 900   6900 timeout 900   8300 timeout 900   1400 timeout 900   7700 out of memory 62     15000 unknown 1.3  120 error (recursion) 14   450 false(reach) 4.4  250 true 890   450 timeout 900     110   unknown 8.9 310 unknown 11   360
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i true 42     7700 true 12     1100 true 850    580 true 24   720 timeout 900   8000 true 42   1000 true 110   3700 out of memory 40     15000 unknown 890    6800 timeout 910   8800 true 2.0  120 true 19   210 timeout 900     50   unknown 15   380 unknown 15   380
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i error (6) .70  67 true 9.7   900 error 850    4200 unknown 9.9 380 error 20   650 true 34   930 true 100   3700 unknown 890     7400 true 650    15000 error (recursion) 15   510 true 2.3  99 true 7.9 160 timeout 900     110   unknown 14   360 unknown 14   380
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 killed by signal 9 120     15000 witness timeout 2.3   180 error 850    3200 witness timeout 65   1800 timeout 910   11000 witness timeout 85   1400 unknown 520   6500 out of memory 52     15000 unknown 14    1100 error (recursion) 60   1200 timeout 900    490 witness timeout 170   1000 unknown 21     1000   error 40   680 error 41   750
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 timeout 900     2100 false(reach) 40     130 error 69    14000 witness timeout 26   820 timeout 900   7500 false(reach) 300   970 out of memory 540   15000 out of memory 110     15000 unknown 1.2  100 out of memory 340   15000 witness timeout 2.9  100 timeout 880   360 timeout 900     200   timeout 900   930 timeout 440   1400
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 error (6) .71  66 witness timeout 30     170 error 45    470 witness timeout 46   1300 out of memory 160   15000 false(reach) 79   1000 witness timeout 41   1000 unknown 3.7   140 unknown 2.1  170 out of memory 150   15000 witness timeout 30    1400 witness timeout 77   330 unknown 110     290   error 200   3100 error 280   6300
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 witness unconfirmed 2.8   430 false(reach) 2.5   79 false(reach) 1.4  150 false(reach) 26   810 false(reach) 83   1300 false(reach) 92   920 false(reach) 56   740 out of memory 28     15000 unknown 2.8  290 false(reach) 56   950 false(reach) 1.5  120 witness timeout 25   210 unknown 1.8   35   unknown 14   360 unknown 16   370
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 witness timeout 15     2300 witness timeout 14     800 error 380    14000 witness timeout 39   970 witness unconfirmed 100   3200 timeout 900   3500 witness unconfirmed 180   5400 out of memory 22     15000 unknown 6.3  710 witness unconfirmed 77   2500 witness timeout 2.4  210 witness timeout 250   1300 timeout 900     250   timeout 900   5200 timeout 900   5500
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 error (6) 15     1400 witness timeout 2.2   200 error 850    2400 witness timeout 40   1000 timeout 900   8900 false(reach) 340   5200 timeout 900   14000 unknown 780     1800 unknown 130    1700 timeout 900   8300 witness timeout 130    1900 witness timeout 89   1000 timeout 900     1600   unknown 22   480 unknown 22   490
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 witness timeout 27     5500 witness timeout 4.9   150 error 85    13000 witness unconfirmed 13   580 witness unconfirmed 40   960 false(reach) 16   650 false(reach) 17   580 unknown .67  160 unknown 1.9  180 witness unconfirmed 29   810 false(reach) 4.1  210 witness timeout 13   250 witness timeout 38     100   error 120   2700 error 140   6900
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 timeout 900     10000 witness timeout 19     170 error 76    13000 timeout 900   1300 timeout 900   14000 witness timeout 140   1500 out of memory 550   15000 out of memory 17     15000 unknown 2.2  210 out of memory 160   15000 witness timeout 4.7  300 witness timeout 58   390 true 59     230   unknown 17   380 unknown 15   370
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 error (6) 1.1   100 false(reach) .76  51 error 850    1100 false(reach) 19   710 witness unconfirmed 28   950 false(reach) 20   740 false(reach) 19   650 out of memory 27     15000 unknown 2.6  240 witness unconfirmed 35   960 false(reach) 2.9  290 error (1) 9.8 68 timeout 900     130   timeout 900   950 unknown 300   950
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 witness unconfirmed 39     6800 false(reach) 8.1   93 error 58    13000 false(reach) 28   740 witness unconfirmed 300   13000 false(reach) 34   860 witness unconfirmed 310   13000 out of memory 29     15000 unknown 1.8  160 witness unconfirmed 280   13000 false(reach) 4.9  280 witness unconfirmed 28   330 unknown 4.1   220   timeout 900   1000 unknown 360   4300
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 error (6) .76  73 witness timeout .77  67 error 850    2600 false(reach) 19   770 false(reach) 54   1600 false(reach) 22   750 false(reach) 20   650 unknown .24  82 unknown 1.3  110 error (recursion) 24   670 timeout 900    79 witness timeout 11   290 timeout 900     110   timeout 900   1000 error 78   6900
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 killed by signal 9 150     15000 witness timeout 380     570 error 850    4200 witness timeout 75   1600 timeout 900   8400 witness timeout 460   1300 witness timeout 80   1200 out of memory 42     15000 unknown 10    1000 error (recursion) 91   2200 witness timeout 41    3900 witness timeout 270   1500 timeout 900     370   error 42   1400 error 44   1400
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 killed by signal 9 130     15000 exception (gremlins) 3.3   150 error 850    2600 witness timeout 49   930 error 200   5600 witness timeout 230   1400 witness timeout 650   5700 unknown .17  41 unknown 2.2  210 error 75   1600 witness timeout 2.2  180 timeout 900   10000 timeout 900     220   unknown 25   730 unknown 27   580
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 false(reach) 3.0   510 false(reach) .42  42 error 85    15000 false(reach) 12   530 false(reach) 22   800 false(reach) 13   550 false(reach) 11   470 out of memory 120     15000 unknown 1.2  110 witness unconfirmed 16   570 false(reach) .91 57 witness timeout 9.7 120 witness timeout 71     71   timeout 900   540 error 35   7600
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 error (6) 31     2900 exception (gremlins) 2.6   120 error 850    3000 false(reach) 23   830 error 140   5400 false(reach) 53   1200 witness timeout 51   1000 unknown .099 37 unknown 1.9  190 error (recursion) 51   1500 witness timeout 2.6  160 witness timeout 100   450 unknown 4.9   150   error 130   4300 error 89   1800
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 error (6) 8.6   840 witness timeout 1.3   94 error 210    14000 false(reach) 28   890 witness unconfirmed 150   3000 false(reach) 29   890 false(reach) 26   800 out of memory 18     15000 out of memory 75    15000 witness unconfirmed 130   2400 false(reach) 11    1500 timeout 900   550 unknown 7.5   480   error 220   3100 error 390   6400
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 error (6) 7.8   770 witness timeout 6.5   550 error 850    2900 timeout 910   11000 timeout 900   8700 timeout 900   2400 timeout 900   6600 out of memory 20     15000 unknown 5.0  490 error (recursion) 130   4100 witness timeout 110    1600 timeout 890   1400 timeout 900     1700   timeout 900   5500 error 190   7000
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 killed by signal 9 120     15000 witness timeout 230     7900 true 850    2100 error 39   980 timeout 910   11000 timeout 900   2000 timeout 900   8100 unknown 32     430 out of memory 350    15000 error (recursion) 46   1000 witness timeout 12    3200 timeout 900   790 unknown 12     350   error 90   3200 error 380   8100
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 error (6) 1.9   220 exception (gremlins) .58  53 error 850    1900 witness timeout 30   950 timeout 900   9200 false(reach) 91   1800 out of memory 640   15000 unknown 9.6   170 unknown 3.1  210 error (recursion) 32   750 witness timeout 4.7  430 witness timeout 51   450 timeout 900     300   timeout 900   1000 error 110   7000
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 error (6) 9.4   1000 timeout 810     6500 error 850    2200 timeout 900   6100 timeout 910   10000 timeout 900   4600 timeout 900   6900 unknown 1.9   330 unknown 890    2400 timeout 900   8200 witness timeout 41    1000 timeout 900   2700 unknown 20     1300   timeout 900   4800 error 460   9200
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 timeout 900     12000 witness timeout 110     450 witness timeout 160    5800 witness timeout 41   940 timeout 900   9900 unknown 250   1000 witness unconfirmed 440   5900 unknown .52  120 unknown 900    6000 timeout 900   8400 witness timeout 1.9  210 witness unconfirmed 14   180 unknown 2.1   150   timeout 900   1800 error 430   11000
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 error (6) 25     2500 witness timeout 45     420 error 850    3400 timeout 900   4800 error 460   6500 false(reach) 85   1000 false(reach) 130   3800 unknown 1.4   260 unknown 900    13000 error 460   5900 witness timeout 11    350 timeout 890   830 timeout 900     1000   timeout 900   1200 error 350   6100
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 error (6) 95     10000 witness timeout 1.9   140 error 850    2100 witness timeout 87   3200 timeout 910   11000 false(reach) 76   1900 witness timeout 130   4100 unknown 1.2   250 out of memory 380    15000 timeout 910   11000 witness timeout 19    580 witness timeout 30   740 timeout 900     600   timeout 900   2100 error 110   1400
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 true 1.2   190 true .18  45 true 85    260 true 12   480 true 20   640 true 12   420 true 97   3700 true 2.3   290 true 2.3  96 true 56   1100 true .80 62 true 5.1 120 unknown 53     32   true 24   490 error 38   5900
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 true .39  48 true .090 26 true 12    280 true 8.1 380 true 9.8 390 true 6.7 270 true 5.7 240 true .80  120 true 1.4  55 true 17   530 true .49 42 true 4.0 77 timeout 900     370   true 14   350 true 85   620
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 true .69  70 true .071 25 true 88    980 true 8.2 390 true 10   470 true 6.8 290 true 6.6 260 true 350     2700 true 2.9  95 true 29   630 true .51 40 true 3.7 78 timeout 900     280   true 16   360 error 41   6300
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 true .50  67 true .068 23 true 850    570 true 6.6 390 true 13   500 true 7.9 300 true 6.4 250 unknown 900     12000 true 5.7  260 timeout 900   7400 true .60 56 true 4.1 97 true 18     14   true 15   360 error 28   6100
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 true 1.3   220 true .068 26 true 850    2100 true 8.5 390 true 15   610 true 6.6 280 true 6.6 260 true 420     3000 true 3.5  110 true 50   1100 true .61 46 true 4.2 75 timeout 900     380   true 18   500 error 47   7800
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 true .93  150 true .079 28 true 850    1600 true 8.7 440 true 11   490 true 8.8 340 true 7.6 300 true 8.7   580 true 2.4  110 true 36   820 true .69 45 true 4.4 76 unknown .66  15   true 19   500 error 37   6400
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 true .50  59 true .070 25 true 100    580 true 8.8 420 true 11   470 true 6.1 310 true 6.6 280 true 1.7   190 true 2.0  80 true 18   490 true .58 44 true 4.0 80 unknown .71  15   true 17   420 error 30   5900
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 error (6) .58  47 true .092 26 true 850    1600 true 9.0 460 true 15   590 true 8.8 340 true 8.3 320 true 1.7   270 true 2.2  90 true 37   780 true .69 47 true 4.5 89 unknown 23     20   true 17   420 timeout 900   12000
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 true .60  64 true .12  27 true 22    640 true 8.8 430 true 14   480 true 23   820 true 17   730 true 3.1   570 unknown .41 37 true 37   900 true .42 42 true 160   680 unknown .29  9.2 true 15   440 true 130   2300
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 true .51  66 true .071 25 true 190    960 true 8.1 390 true 9.7 450 true 6.9 280 true 6.0 250 true 5.8   340 true 1.7  73 true 23   590 true .56 41 true 3.7 80 timeout 850     200   true 16   370 error 27   6800
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 true .16  31 true .042 22 true 1.8  30 true 6.1 350 true 7.6 340 true 5.5 240 true 4.2 220 true .20  29 true .67 40 true 8.3 340 true .34 38 true 3.6 72 timeout 900     380   true 10   330 true 12   340
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 true 4.1   750 true .27  39 true 850    4000 true 9.8 430 true 68   2200 true 17   540 true 97   3700 out of memory 190     15000 true 58    5000 true 160   4100 true .72 65 true 5.4 160 timeout 900     300   true 16   370 true 170   1100
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 killed by signal 9 100     15000 true 3.4   220 true 850    2100 true 22   860 timeout 900   11000 true 62   1700 true 110   4400 unknown .87  180 out of memory 290    15000 timeout 900   8300 true 2.7  140 true 24   870 timeout 900     1500   true 39   560 timeout 890   1800
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 true 10     1800 true .41  38 true 850    2500 true 13   530 true 200   5200 true 21   660 true 99   3600 unknown .45  110 true 110    4600 true 850   7900 true 1.1  120 true 8.4 290 timeout 900     580   true 22   440 timeout 470   1600
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 true 13     2300 true .50  41 true 850    2200 true 20   710 true 82   2700 true 22   740 true 100   3600 out of memory 260     15000 true 81    4100 timeout 900   7900 true 1.5  160 true 11   330 timeout 900     1000   true 26   550 timeout 310   2000
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 true 100     12000 true 2.1   150 true 850    1500 true 18   830 timeout 900   9800 true 46   1400 true 100   4400 out of memory 130     15000 out of memory 260    15000 timeout 900   8200 true 1.5  89 true 22   670 timeout 900     1600   true 30   560 true 250   3100
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 true 31     5000 true 1.2   74 true 850    1600 true 12   600 timeout 900   10000 true 31   800 true 100   4600 out of memory 130     15000 true 260    14000 timeout 910   8200 true 1.5  75 true 20   700 timeout 900     620   true 24   530 true 360   1500
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 true 2.8   520 true .21  41 true 850    5000 true 9.3 400 true 34   1000 true 14   450 true 96   3700 out of memory 170     15000 true 70    7800 true 120   3400 true .64 51 true 5.2 140 timeout 900     300   true 15   440 true 57   880
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 true 7.0   1300 true .37  36 true 850    2800 true 12   480 true 37   1300 true 19   560 true 98   3600 out of memory 200     15000 true 61    4000 true 410   5800 true .96 79 true 6.6 200 timeout 900     430   true 20   390 true 180   1400
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 true 43     6700 true 1.2   72 true 850    1900 true 22   900 true 210   11000 true 33   1000 true 110   4400 out of memory 75     15000 out of memory 92    15000 timeout 900   7500 true 1.3  100 true 21   690 timeout 900     1900   true 35   510 true 310   1900
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 true 35     5600 true .97  63 true 850    2000 true 19   860 true 200   5200 true 29   930 true 100   4400 out of memory 75     15000 out of memory 99    15000 timeout 910   7800 true 1.5  98 true 21   670 timeout 900     1900   true 33   580 true 550   1700
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 true 36     6300 true 1.7   110 true 850    2400 true 19   700 true 780   11000 true 29   900 true 100   3700 out of memory 210     15000 out of memory 360    15000 timeout 900   9200 true 1.4  100 true 13   500 timeout 900     1500   true 32   570 true 270   2100
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 true 3.1   630 true .24  41 true 850    7000 true 8.3 410 true 43   1800 true 17   480 true 95   3700 out of memory 170     15000 true 53    6400 true 110   2800 true .49 48 true 4.7 130 timeout 900     300   true 16   350 true 130   1400
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 true 17     3100 true .52  43 true 850    2800 true 17   770 true 48   1700 true 25   730 true 100   3700 out of memory 220     15000 true 37    2600 timeout 900   7800 true 1.2  89 true 8.3 210 timeout 900     1600   true 30   550 timeout 190   1600
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 killed by signal 9 78     15000 true 2.2   120 true 850    2300 true 39   1000 true 530   10000 true 60   1500 true 110   3800 out of memory 180     15000 true 230    9600 timeout 900   6500 true 2.6  260 true 25   810 timeout 900     7600   true 49   850 timeout 420   4800
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 error (6) .15  29 exception (gremlins) .056 24 true 850    900 true 7.6 360 timeout 900   9700 true 6.7 290 true 6.1 270 true 4.1   280 true 1.2  53 error (recursion) 7.9 340 true .52 51 true 3.4 79 unknown 55     17   true 12   340 true 150   510
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 true 1.4   190 true .23  39 true 850    1300 true 8.6 430 true 78   1900 true 11   420 true 15   670 true 7.0   650 true 2.6  130 error (recursion) 14   450 true 1.0  79 true 5.1 100 timeout 900     410   true 25   540 error 77   10000
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 true .31  37 true .053 24 true 3.0  35 true 6.5 350 true 7.8 380 true 5.1 250 true 4.7 230 true .27  42 true 1.2  49 true 13   420 true .41 39 true 3.9 76 timeout 900     460   true 11   340 true 24   370
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 true 4.5   1000 true .83  82 true 850    590 true 30   910 true 64   1600 true 15   590 true 98   3900 out of memory 130     15000 true 420    15000 true 260   4900 true 1.3  120 true 5.1 100 unknown 1.6   82   true 18   500 error 31   5900
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 error (8) 1.6   250 true .18  45 true 850    3900 true 8.0 420 true 17   650 true 8.1 300 true 7.6 340 true 26     2500 true 4.6  340 true 60   1400 true .63 49 true 4.4 100 true 20     340   true 17   490 error 29   6200
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 true .37  48 true .092 24 true 90    1100 true 6.6 330 true 11   420 true 5.8 240 true 5.2 210 true 1.7   290 true .95 43 true 15   400 true .41 44 true 6.2 160 timeout 900     360   true 13   340 unknown 92   380
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 true .18  30 true .056 21 true 23    190 true 4.8 340 true 7.2 350 true 4.7 220 true 4.5 200 true .87  57 true .69 28 true 8.4 330 true .33 38 true 3.1 72 timeout 900     380   true 10   340 true 160   4100
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 error (8) 1.7   270 true .19  36 true 850    3500 true 12   470 true 26   750 true 16   480 true 35   1300 true 300     9800 true 7.1  290 timeout 900   7300 true .84 54 true 4.8 100 timeout 900     380   error 560   6500 error 460   5500
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 true .22  36 true .046 22 true 2.7  31 true 6.0 340 true 8.6 380 true 6.0 250 true 5.3 220 true .31  39 true .85 37 true 12   380 true .36 37 true 3.6 83 timeout 900     8.7 true 12   340 true 350   6000
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 true 9.7   1800 true .43  45 true 850    2300 true 13   570 true 550   8300 true 24   780 true 100   790 unknown 900     3000 true 110    710 true 270   5100 true 1.6  350 true 5.8 120 true 37     170   true 34   760 error 35   750
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 true .35  49 true .060 24 true 850    840 true 5.6 340 true 11   480 true 18   680 true 95   2400 true 8.9   1500 true 1.2  64 true 37   860 true .32 43 true 3.7 78 unknown 18     13   true 18   500 error 68   8000
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 true 1.1   130 true .10  25 true 850    2800 true 7.1 380 true 12   550 true 7.4 280 true 6.6 260 true 150     4100 true 5.6  140 true 48   1000 true .67 43 true 3.9 82 timeout 900     110   true 14   370 true 68   540
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 true .32  41 true .055 22 true 68    470 true 6.6 360 true 7.4 390 true 6.2 260 true 4.7 230 true 1.4   150 true 1.2  50 true 13   460 true .46 40 true 3.1 80 unknown 83     18   true 14   360 error 37   7900
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 true 1.1   150 true .098 24 true 850    3400 true 8.1 380 true 13   540 true 7.5 290 true 5.9 260 true 280     7600 true 5.4  130 true 48   990 true .62 46 true 3.7 78 timeout 900     100   true 13   340 true 100   480
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 true .67  100 true .081 23 true 850    2500 true 7.3 350 true 9.2 370 true 6.5 260 true 4.8 220 true 6.0   490 true 1.2  61 true 31   710 true .34 27 true 3.5 79 timeout 900     99   true 11   350 true 230   1900
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 true 1.3   220 true .12  26 true 850    1500 true 7.2 360 true 18   570 true 12   400 true 97   3600 unknown .16  35 true 7.3  430 true 61   1500 true .51 41 true 3.6 100 timeout 900     98   true 13   340 true 320   1700
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 true .29  42 true .053 25 true 4.8  75 true 7.4 420 true 11   480 true 7.2 300 true 6.4 280 true .50  74 true 1.6  68 true 10   440 true .44 41 true 3.8 79 timeout 900     380   true 12   360 true 14   380
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 true 8.5   1800 true .49  47 true 850    950 true 9.4 480 true 32   1100 true 20   680 true 18   700 true 230     5400 true 11    440 true 300   4900 true 1.2  150 true 5.4 100 timeout 900     210   true 19   510 error 42   8300
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 true .22  40 true .090 23 true 2.3  40 true 6.7 400 true 8.3 430 true 6.9 300 true 4.9 250 true .35  61 true 1.8  68 true 9.4 430 true .48 35 true 3.5 78 timeout 900     370   true 18   370 error 29   5900
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 true .30  36 true .042 24 true 37    120 true 6.2 380 true 8.7 390 true 6.4 270 true 5.5 240 true .56  71 true 1.4  53 true 9.6 400 true .38 35 true 3.8 76 timeout 900     270   true 14   350 true 800   11000
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 true .46  88 true .076 22 true 280    1200 true 6.4 370 true 9.7 390 true 6.3 260 true 5.7 230 true 6.8   500 true 1.8  84 true 22   590 true .38 43 true 3.8 80 timeout 900     380   true 14   370 true 260   6500
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 true 1.4   240 true .11  24 true 850    1800 true 7.7 380 true 16   520 true 7.2 290 true 5.4 240 true 79     3600 true 7.7  530 true 38   860 true .61 50 true 3.8 74 timeout 900     360   true 14   380 true 260   6500
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 true .22  34 true .032 23 true 7.4  180 true 7.1 370 true 7.9 370 true 4.7 250 true 5.1 220 true .70  83 true 1.0  43 true 8.3 370 true .39 39 true 3.6 75 timeout 900     380   true 11   340 true 240   6600
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 true .47  84 true .049 22 true 470    1300 true 7.4 360 true 8.3 380 true 6.1 260 true 5.5 230 true 5.4   400 true 1.7  76 true 30   680 true .44 41 true 3.5 76 timeout 900     370   true 13   340 true 240   6100
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 true 1.4   310 true .072 24 true 850    1600 true 8.0 370 true 13   490 true 7.2 280 true 5.0 240 true 51     2600 true 5.6  360 true 46   880 true .58 51 true 3.8 78 timeout 900     380   true 13   340 true 270   6300
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 true .27  44 true .044 22 true 92    650 true 7.2 360 true 8.8 380 true 5.9 250 true 5.2 230 true 2.7   220 true 1.3  56 true 17   490 true .40 40 true 3.6 78 timeout 900     370   true 12   320 true 240   5900
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 true .22  33 true .058 22 true 4.4  110 true 6.9 360 true 8.4 370 true 5.6 250 true 4.7 230 true .47  66 true 1.1  44 true 9.1 350 true .40 28 true 3.3 73 timeout 900     370   true 15   360 error 34   6200
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 true .75  120 true .047 23 true 850    1900 true 6.6 370 true 12   470 true 6.6 270 true 5.9 230 true 21     1300 true 3.1  180 true 34   790 true .55 44 true 3.1 76 timeout 900     370   true 12   330 true 250   6100
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 true .69  99 true .079 23 true 370    1300 true 7.3 360 true 8.3 400 true 6.1 260 true 4.7 230 true 8.7   610 true 1.8  98 true 24   610 true .53 44 true 3.7 82 timeout 900     380   true 13   350 true 240   6100
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 true .27  39 true .071 22 true 44    360 true 7.4 360 true 8.2 360 true 5.7 250 true 4.5 220 true 1.3   130 true 1.1  49 true 9.8 360 true .46 39 true 3.5 77 timeout 900     370   true 13   340 true 270   6200
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 true 1.5   280 true .090 25 true 850    1500 true 8.5 380 true 13   520 true 6.9 270 true 6.0 240 true 24     1300 true 3.1  170 true 49   980 true .62 54 true 3.3 78 unknown 26     17   true 13   350 true 330   6700
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 error (6) .23  32 true .093 24 true 850    180 true 7.7 380 timeout 900   8200 true 5.3 260 true 4.8 230 out of memory 94     15000 unknown 900    15000 error (recursion) 6.9 360 true .59 53 true 3.8 76 timeout 900     110   true 12   330 true 320   6400
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 true .24  39 true .041 23 true 17    380 true 7.5 360 true 8.4 370 true 5.8 250 true 5.2 230 true 1.7   150 true 1.1  50 true 12   410 true .44 40 true 3.0 77 timeout 900     370   true 13   330 true 260   6200
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 true 3.2   620 true .19  29 true 850    1700 true 8.0 420 true 18   600 true 7.7 320 true 6.4 300 true 77     2900 true 7.4  400 true 56   1200 true .96 72 true 4.4 85 timeout 900     110   true 15   420 true 340   6700
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 true .28  38 true .071 23 true 8.5  140 true 6.3 380 true 7.5 390 true 6.1 270 true 5.6 240 true .56  77 true 1.4  52 true 8.6 400 true .45 35 true 3.2 74 timeout 900     390   true 12   340 true 270   6400
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 true .55  75 true .074 23 true 210    1100 true 6.4 360 true 9.4 390 true 6.1 260 true 5.5 230 true 4.8   380 true 1.6  71 true 25   600 true .50 44 true 3.7 80 timeout 900     370   true 13   370 true 250   6300
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 true .65  98 true .058 23 true 660    1700 true 6.1 360 true 8.8 410 true 6.5 260 true 5.7 230 true 14     870 true 2.3  130 true 28   610 true .48 42 true 3.8 81 timeout 900     370   true 12   340 true 260   6600
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 true 1.5   270 true .089 25 true 850    2000 true 7.9 370 true 17   550 true 7.3 280 true 5.9 240 true 110     4500 true 10    680 true 41   930 true .67 53 true 3.5 76 timeout 900     370   true 13   350 error 27   5400
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 true 2.2   420 true .099 27 true 850    2000 true 8.1 380 true 29   860 true 7.0 310 true 7.3 280 true 270     9600 true 23    1500 true 49   1100 true .79 64 true 3.8 75 timeout 900     380   true 14   360 true 270   6700
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 true .28  38 true .049 22 true 65    350 true 7.4 360 true 7.6 380 true 6.2 260 true 5.8 230 true 2.4   150 true 1.5  58 true 9.1 390 true .38 32 true 3.6 76 timeout 900     380   true 25   480 error 58   6500
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 error (6) .65  48 true .69  64 true 850    1500 true 12   570 timeout 900   9100 true 21   680 true 19   810 out of memory 410     15000 true 14    710 error (recursion) 16   520 true .83 93 true 5.7 110 timeout 900     150   true 21   410 true 450   6300
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 error (6) .26  35 true .071 25 true 850    2300 true 8.2 380 timeout 900   5500 true 6.3 280 true 7.0 280 true 8.6   590 true 2.2  100 error (recursion) 9.0 370 true .68 59 true 4.5 88 timeout 900     110   true 28   570 error 80   7300
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 error (6) .27  35 true .16  29 true 850    2000 true 8.6 390 timeout 910   11000 true 17   590 true 12   440 true 78     3000 true 7.0  380 error (recursion) 7.9 370 true .98 80 true 4.2 82 timeout 900     120   true 14   390 true 270   6100
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 true 1.4   230 true .091 27 true 850    2200 true 8.4 380 true 13   480 true 9.7 390 true 7.3 300 true 400     11000 true 5.4  120 true 61   1400 true .60 49 true 4.2 77 unknown 170     32   true 15   340 true 140   2400
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 true 45     6100 true 6.3   500 true 850    1900 true 23   850 timeout 900   9900 true 39   1000 true 100   2500 out of memory 460     15000 unknown 890    6400 timeout 900   10000 true 3.8  570 true 7.8 200 timeout 900     200   true 37   650 error 190   6000
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 true .90  160 true .15  32 true 850    1600 true 7.3 390 true 13   560 true 9.1 320 true 7.0 260 true 3.4   420 true 2.1  91 true 46   890 true .55 46 true 4.2 90 timeout 900     16   true 17   370 error 30   7200
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 true 2.5   430 true .23  41 true 850    340 true 8.2 410 true 57   1500 true 14   440 true 97   3500 out of memory 160     15000 true 21    1200 true 240   5000 true 1.0  80 true 4.8 100 timeout 900     99   true 17   490 true 160   1000
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 true .85  110 true .10  24 true 850    2500 true 7.0 380 true 10   470 true 7.3 280 true 6.0 240 true 24     1100 true 1.6  63 true 44   890 true .47 40 true 4.0 74 unknown 21     18   true 15   360 true 27   540
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 true .90  140 true .15  28 true 850    2200 true 8.9 390 true 15   600 true 7.6 310 true 6.2 260 true 3.1   430 true 1.8  84 true 46   890 true .55 48 true 4.3 91 timeout 900     300   true 15   350 error 38   8500
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 true .27  34 true .057 22 true 260    470 true 7.2 360 true 8.6 380 true 6.3 260 true 5.3 230 true 1.3   130 true 1.1  45 true 11   400 true .43 38 true 3.8 75 timeout 900     240   true 12   350 error 30   6300
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 true .45  54 true .092 23 true 850    1200 true 6.4 370 true 9.4 390 true 7.3 280 true 6.2 240 true 2.7   310 true 1.2  67 true 30   630 true .45 39 true 3.8 84 timeout 900     290   true 14   360 error 29   6000
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 true .75  120 true .15  31 true 850    1700 true 8.2 420 true 15   610 true 7.4 320 true 7.5 280 true 3.5   430 true 2.0  88 true 51   900 true .62 45 true 3.7 88 unknown .52  18   true 15   450 error 29   6300
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 error (6) .20  40 true .16  27 error 850    1800 true 8.8 440 true 270   5700 true 14   440 true 99   4700 out of memory 470     15000 true 200    7900 timeout 900   9400 true .90 76 true 6.5 150 timeout 900     380   true 19   500 timeout 98   1100
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 true 33     5600 true .72  68 true 850    1300 true 8.9 450 true 370   6100 true 21   600 true 97   770 out of memory 260     15000 out of memory 730    15000 timeout 900   9700 true 1.5  120 true 5.2 150 timeout 900     130   true 17   500 unknown 78   530
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 true 1.9   340 true .28  51 true 1.6  38 true 7.8 410 true 36   940 true 17   600 true 96   2300 true 20     2100 true 2.0  84 true 12   420 true .81 80 true 4.8 140 true 19     110   true 17   350 error 33   6200
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 true 3.2   580 true .22  35 true 850    1100 true 7.7 420 true 36   1100 true 13   480 true 96   3800 out of memory 17     15000 true 39    4400 timeout 900   7300 true .63 41 true 4.4 120 timeout 900     63   true 15   430 true 120   590
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 true .82  120 true .12  25 true 850    2000 true 7.2 380 true 12   500 true 6.8 300 true 6.7 260 true 26     750 true 1.7  75 true 40   850 true .56 49 true 3.6 86 timeout 900     51   true 14   350 error 31   6300
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 true 14     3200 true .62  53 true 850    820 true 20   720 true 400   6700 true 24   780 true 100   4500 true 140     3200 true 6.6  290 timeout 900   9200 true 1.1  44 true 5.5 100 unknown 1.1   54   true 28   570 error 88   5500
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 true .92  160 true .12  29 true 720    2600 true 7.6 430 true 16   620 true 12   400 true 8.1 340 true 80     2900 true 3.5  120 true 33   800 true .68 47 true 4.2 80 timeout 900     120   true 15   360 true 210   4700
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 true 1.1   150 true .14  25 true 33    240 true 8.2 370 true 90   3200 true 12   410 true 58   2600 unknown 900     7600 true 23    560 true 240   4800 true .81 110 true 4.1 110 unknown .46  16   true 14   430 true 62   620
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 true 1.6   290 true .13  25 true 850    2400 true 8.6 390 true 42   940 true 13   430 true 16   700 unknown .25  44 true 5.1  300 true 70   1400 true .72 52 true 4.9 100 timeout 890     97   true 15   350 error 30   6300
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 true 2.7   510 true .23  48 true 850    2400 true 9.3 410 true 35   1100 true 13   440 true 14   650 true 31     2300 true 4.2  280 true 90   2300 true .79 64 true 4.4 100 timeout 900     76   true 15   420 true 260   770
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 true 2.4   400 true .093 26 true 850    710 true 9.0 400 true 70   1900 true 14   470 true 97   3500 true 300     14000 true 7.4  430 true 99   2800 true .94 67 true 5.7 150 timeout 880     78   true 16   450 error 34   11000
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 true 1.5   270 true .13  26 true 850    1400 true 8.7 380 true 14   520 true 13   420 true 7.9 290 true 7.4   840 true 1.9  100 true 58   1300 true .57 46 true 3.6 82 timeout 870     160   true 15   370 true 330   680
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 true 2.2   380 true .32  43 true 850    540 true 9.7 460 true 57   1500 true 14   470 true 96   750 unknown 900     11000 true 46    1200 true 450   6200 true 1.1  76 true 5.9 170 true 19     83   true 41   780 error 34   4700
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 true 1.6   270 true .13  26 true 850    4800 true 7.2 390 true 46   1000 true 12   410 true 96   2400 unknown 900     11000 true 230    12000 true 66   1500 true .72 53 true 4.2 88 timeout 900     31   true 16   350 error 29   6300
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 true 2.4   450 true .15  27 true 850    2500 true 7.4 390 true 19   620 true 14   420 true 14   540 true 18     1600 true 3.0  180 true 87   1700 true .65 58 true 4.2 86 timeout 880     110   true 14   340 true 370   2200
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 true 1.1   180 true .12  25 true 850    1000 true 8.3 380 true 11   520 true 10   360 true 5.9 260 true 5.9   570 true 1.8  80 true 44   980 true .67 55 true 3.9 80 timeout 900     99   true 15   340 true 240   610
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 true 1.3   190 true .071 25 true 850    760 true 9.1 380 true 25   760 true 12   400 true 96   4000 out of memory 130     15000 true 41    2300 true 40   1300 true .65 55 true 4.3 110 out of memory 530     15000   true 14   340 true 69   510
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 true 1.3   220 true .11  25 true 850    2000 true 8.5 380 true 18   590 true 10   450 true 23   710 true 40     5500 true 2.1  150 true 37   860 true .62 52 true 8.6 130 timeout 880     88   true 18   490 error 45   6500
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 true 1.0   220 true .083 25 true 850    1900 true 8.6 380 true 24   620 true 11   420 true 26   740 true 41     5700 true 2.2  150 true 37   880 true .56 52 true 8.0 120 timeout 890     110   true 20   370 error 38   5900
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 true 1.3   220 true .11  25 true 850    2200 true 8.4 380 true 17   580 true 15   470 true 39   1300 true 40     5500 true 2.3  150 true 37   860 true .64 58 true 17   170 timeout 880     130   true 24   550 error 46   6400
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 true .66  100 true .095 24 true 850    840 true 7.8 370 true 8.1 400 true 6.6 270 true 5.8 240 true 3.9   430 true 1.6  78 true 30   790 true .53 41 true 3.4 85 unknown 4.6   18   true 12   350 true 120   410
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 true .39  47 true .067 24 true 55    580 true 8.1 390 true 9.9 420 true 6.8 280 true 4.9 240 true .95  150 true 1.6  64 true 16   540 timeout 900    31 true 3.8 78 timeout 900     270   true 11   330 true 13   340
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 true .48  47 true .054 24 true 72    640 true 8.0 390 true 12   510 true 6.0 280 true 6.2 240 true 1.2   160 true 1.6  64 true 14   500 timeout 900    32 true 3.6 77 false(reach) 6.6   16   true 14   340 true 13   330
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 true 1.2   180 true .092 24 true 750    3300 true 7.3 390 true 13   560 true 7.6 290 true 7.5 280 true 96     3500 true 5.8  160 true 44   860 timeout 900    31 true 4.2 84 timeout 900     68   true 15   370 true 67   390
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 true .56  72 true .11  26 true 130    1000 true 9.3 410 true 13   550 true 17   720 true 96   760 true 35     6700 true 2.4  90 true 29   700 true .72 52 true 5.0 91 timeout 900     21   unknown 11   350 unknown 10   330
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 true .46  58 true .086 25 true 85    990 true 7.9 390 true 20   590 true 7.7 310 true 7.4 280 true 9.5   690 true 2.0  87 true 22   560 true .58 43 true 4.2 84 timeout 900     380   true 16   370 error 41   8000
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 true .63  110 true .085 24 true 380    1700 true 8.1 390 true 8.6 410 true 7.0 280 true 6.0 240 true 1.8   320 true 1.6  67 true 28   640 true .58 39 true 4.2 84 timeout 900     250   true 13   340 true 14   450
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 true .48  56 true .066 24 true 850    1700 true 8.2 390 true 8.3 420 true 7.4 290 true 5.3 250 true 3.5   320 true 1.8  78 true 23   560 true .55 41 true 4.0 75 timeout 900     88   true 16   410 true 170   400
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 true 1.6   330 true .077 27 true 850    1600 true 9.2 410 true 16   580 true 9.2 340 true 7.8 300 true 57     1200 true 2.2  130 true 51   1100 timeout 900    36 true 4.7 88 timeout 880     160   true 17   350 true 110   570
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 true .72  110 true .099 24 true 850    820 true 7.6 370 true 11   480 true 5.8 270 true 6.2 240 true 4.0   480 true 1.6  79 true 27   630 true .47 41 true 3.5 79 timeout 890     140   true 13   370 true 40   410
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 true .44  53 true .060 23 true 850    1300 true 8.1 380 true 7.9 390 true 5.9 280 true 5.9 240 true 2.1   240 true 1.6  64 true 16   510 true .56 40 true 3.7 76 timeout 870     140   true 12   350 true 37   490
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 true .80  120 true .070 23 true 850    1800 true 7.9 380 true 11   470 true 8.3 300 true 5.8 270 true 4.1   310 true 1.6  62 true 33   690 true .61 61 true 4.0 89 timeout 900     50   true 20   330 true 59   510
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 true 2.1   380 true .14  27 true 850    2600 true 8.0 410 true 21   640 true 13   400 true 9.9 340 true 21     1500 true 3.4  180 true 76   1500 true .70 73