Tool CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 20   860 140 false(unreach-call) 1 wit inspect 16    640 error (7) 0 wit inspect 7.2   460   timeout 0 wit inspect 6.7  300 error (2) 0 wit inspect 6.6    83    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 29   680 260 false(unreach-call) 1 wit inspect 13    420 true -32 wit inspect 22     570   unknown 0 wit inspect 7.4  290 error (2) 0 wit inspect 1.5    24    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   8300 7600 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5400 9700 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0021 .29 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 30   690 260 false(unreach-call) 1 wit inspect 15    580 unknown 0 wit inspect 6.0   290   unknown 0 wit inspect 9.4  350 error (2) 0 wit inspect 2.8    36    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 130   1400 1400 true -32 wit inspect 9.2  320 true -32 wit inspect 29     600   unknown 0 wit inspect 6.7  280 error (2) 0 wit inspect 1.9    25    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   8400 7400 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 290   5300 2400 false(unreach-call) 1 wit inspect 11    370 true -32 wit inspect 46     910   unknown 0 wit inspect 7.3  320 error (2) 0 wit inspect 2.6    29    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 110   1100 1100 timeout 0 wit inspect 92    830 timeout 0 wit inspect 96     1800   unknown 0 wit inspect 14    520 error (2) 0 wit inspect 6.3    62    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 33   670 350 false(unreach-call) 1 wit inspect 8.7  300 true -32 wit inspect 11     440   unknown 0 wit inspect 5.3  260 error (2) 0 wit inspect 1.1    20    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5300 9200 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .99 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 18   540 130 false(unreach-call) 1 wit inspect 10    440 true -32 wit inspect 26     600   unknown 0 wit inspect 7.1  290 error (2) 0 wit inspect 2.0    25    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 220   1900 2100 false(unreach-call) 1 wit inspect 8.1  300 true -32 wit inspect 16     500   unknown 0 wit inspect 5.4  270 error (2) 0 wit inspect 1.4    22    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5700 9100 error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 320   5300 3500 timeout 0 wit inspect 92    330 timeout 0 wit inspect 97     860   unknown 0 wit inspect 6.0  270 error (2) 0 wit inspect 1.6    21    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 66   1100 740 true -32 wit inspect 7.9  350 true -32 wit inspect 15     510   unknown 0 wit inspect 5.9  290 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   2900 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 true 2 wit inspect 36     720  
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 120   4200 1100 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 41    1100 true 2 wit inspect 110     2600  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   3700 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 43     1900  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 97   2300 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 true 2 wit inspect 18     500  
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   6000 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 42 error (2) 0 wit inspect .019 4.8
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i true 1 wit inspect 120   1800 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6500 out of memory 0 wit inspect 880     7000  
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 30   700 240 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 14     450  
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 98   1600 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 53     3200  
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   2600 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5900 true 2 wit inspect 43     830  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 7.2 390 52 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 true 2 wit inspect 15     510  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   3700 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 true 2 wit inspect 25     600  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   3100 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 42     870  
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   2500 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 34     1300  
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   2700 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5700 true 2 wit inspect 32     800  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 13   530 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 53     1200  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   2800 960 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 true 2 wit inspect 20     530  
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   3700 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 30     820  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   4800 830 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 21     620  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 910   7800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 42 error (2) 0 wit inspect .019 4.9
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i true 1 wit inspect 100   3700 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5300 error (7) 0 wit inspect 10     260  
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 14   510 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 true 2 wit inspect 67     2100  
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   2800 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 47     1500  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   7100 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .025 4.8
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   3800 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 35     990  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 100   3600 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6000 true 2 wit inspect 36     1100  
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 false(unreach-call) 0 wit inspect 64   1000 500 true -32 wit inspect 18    800 timeout 0 wit inspect 97     3000   unknown 0 wit inspect 17    550 error (2) 0 wit inspect 7.7    83    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb_false-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 39   900 360 true -32 wit inspect 8.4  290 timeout 0 wit inspect 97     1500   unknown 0 wit inspect 7.3  290 error (2) 0 wit inspect 2.3    24    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 35   700 330 true -32 wit inspect 11    480 timeout 0 wit inspect 97     4000   unknown 0 wit inspect 9.3  320 error (2) 0 wit inspect 2.6    27    - wit inspect - wit inspect
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 false(unreach-call) 1 wit inspect 48   570 470 false(unreach-call) 1 wit inspect 24    600 unknown 0 wit inspect 5.6   300   unknown 0 wit inspect 8.7  330 error (2) 0 wit inspect 2.9    30    - wit inspect - wit inspect
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 false(unreach-call) 0 wit inspect 65   2300 710 timeout 0 wit inspect 96    1900 timeout 0 wit inspect 97     4500   unknown 0 wit inspect 10    510 error (2) 0 wit inspect 5.7    59    - wit inspect - wit inspect
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 timeout 0 wit inspect 900   7900 7200 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0035 .31 - wit inspect - wit inspect
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 false(unreach-call) 1 wit inspect 9.9 440 83 false(unreach-call) 1 wit inspect 8.6  350 error (7) 0 wit inspect 11     270   unknown 0 wit inspect 3.9  280 error (2) 0 wit inspect 1.7    24    - wit inspect - wit inspect
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 false(unreach-call) 0 wit inspect 38   740 360 true -32 wit inspect 19    540 true -32 wit inspect 27     870   unknown 0 wit inspect 8.0  340 error (2) 0 wit inspect 2.5    28    - wit inspect - wit inspect
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 false(unreach-call) 1 wit inspect 11   400 82 false(unreach-call) 1 wit inspect 9.7  380 timeout 0 wit inspect 97     950   unknown 0 wit inspect 8.8  330 error (2) 0 wit inspect 2.5    29    - wit inspect - wit inspect
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 false(unreach-call) 0 wit inspect 24   570 180 true -32 wit inspect 9.2  350 timeout 0 wit inspect 96     1100   unknown 0 wit inspect 7.2  280 error (2) 0 wit inspect 2.1    26    - wit inspect - wit inspect
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 false(unreach-call) 1 wit inspect 9.8 400 83 false(unreach-call) 1 wit inspect 9.6  370 true -32 wit inspect 20     610   unknown 0 wit inspect 7.9  310 error (2) 0 wit inspect 2.4    26    - wit inspect - wit inspect
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 false(unreach-call) 1 wit inspect 31   960 240 false(unreach-call) 1 wit inspect 36    770 true -32 wit inspect 72     2100   unknown 0 wit inspect 14    540 error (2) 0 wit inspect 8.4    83    - wit inspect - wit inspect
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 timeout 0 wit inspect 900   5400 7300 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .98 50 error (invalid witness file) 0 wit inspect .0040 .28 - wit inspect - wit inspect
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(unreach-call) 1 wit inspect 7.7 350 64 false(unreach-call) 1 wit inspect 8.3  300 unknown 0 wit inspect 30     540   unknown 0 wit inspect 5.9  270 error (2) 0 wit inspect 1.4    22    - wit inspect - wit inspect
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 false(unreach-call) 1 wit inspect 26   640 190 false(unreach-call) 1 wit inspect 31    900 true -32 wit inspect 44     1300   unknown 0 wit inspect 8.2  350 error (2) 0 wit inspect 3.1    36    - wit inspect - wit inspect
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 false(unreach-call) 1 wit inspect 13   450 100 false(unreach-call) 1 wit inspect 14    480 timeout 0 wit inspect 97     3100   unknown 0 wit inspect 9.0  350 error (2) 0 wit inspect 3.7    35    - wit inspect - wit inspect
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 timeout 0 wit inspect 930   9800 7700 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .92 50 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c false(unreach-call) 0 wit inspect 40   1000 360 timeout 0 wit inspect 92    860 error (7) 0 wit inspect 11     480   timeout 0 wit inspect 5.8  260 error (1) 0 wit inspect .86   20    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.c false(unreach-call) 1 wit inspect 20   810 170 false(unreach-call) 1 wit inspect 22    600 error (7) 0 wit inspect 11     420   timeout 0 wit inspect 5.6  220 error (1) 0 wit inspect .87   20    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c false(unreach-call) 1 wit inspect 35   1400 320 false(unreach-call) 1 wit inspect 32    950 error (7) 0 wit inspect 11     520   timeout 0 wit inspect 7.0  270 error (1) 0 wit inspect 1.0    22    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c false(unreach-call) 1 wit inspect 68   1500 700 false(unreach-call) 1 wit inspect 48    950 error (7) 0 wit inspect 14     600   timeout 0 wit inspect 7.3  280 error (1) 0 wit inspect 1.1    24    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c false(unreach-call) 1 wit inspect 55   1200 510 false(unreach-call) 1 wit inspect 39    950 error (7) 0 wit inspect 7.8   560   timeout 0 wit inspect 7.1  280 error (1) 0 wit inspect 1.1    22    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c false(unreach-call) 1 wit inspect 79   930 820 false(unreach-call) 1 wit inspect 33    840 error (7) 0 wit inspect 12     520   timeout 0 wit inspect 5.8  270 error (1) 0 wit inspect 1.1    21    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c false(unreach-call) 1 wit inspect 56   1300 570 false(unreach-call) 1 wit inspect 30    670 error (7) 0 wit inspect 14     540   timeout 0 wit inspect 6.3  280 error (1) 0 wit inspect .98   22    - wit inspect - wit inspect
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 timeout 0 wit inspect 900   9500 8000 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
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 timeout 0 wit inspect 930   10000 8000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
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 timeout 0 wit inspect 900   6200 8800 error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 37   970 320 true -32 wit inspect 8.9  320 true -32 wit inspect 15     510   unknown 0 wit inspect 8.5  350 error (2) 0 wit inspect 2.9    26    - wit inspect - wit inspect
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 false(unreach-call) 0 wit inspect 47   1400 430 true -32 wit inspect 11    420 timeout 0 wit inspect 96     1700   unknown 0 wit inspect 11    350 error (2) 0 wit inspect 3.4    33    - wit inspect - wit inspect
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 false(unreach-call) 0 wit inspect 15   490 130 true -32 wit inspect 9.3  380 true -32 wit inspect 27     750   unknown 0 wit inspect 7.8  330 error (2) 0 wit inspect 2.5    28    - wit inspect - wit inspect
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 2 wit inspect 4.7 290 41 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 15     500  
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 1 wit inspect 4.9 290 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    7000 unknown 0 wit inspect 480     2000  
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 2 wit inspect 5.5 300 44 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 17     470  
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 2 wit inspect 5.2 300 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 27     1400  
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 2 wit inspect 4.0 290 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    7000 true 2 wit inspect 16     460  
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 2 wit inspect 10   500 93 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6900 true 2 wit inspect 32     1200  
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 2 wit inspect 3.9 260 34 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 11     390  
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 2 wit inspect 3.3 260 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 6.3   290  
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 2 wit inspect 98   4100 960 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    7000 true 2 wit inspect 19     480  
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 true 2 wit inspect 100   3900 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 true 2 wit inspect 25     650  
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 2 wit inspect 100   4400 950 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6900 true 2 wit inspect 21     510  
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 2 wit inspect 110   4300 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 21     580  
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 2 wit inspect 120   4200 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 21     600  
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 2 wit inspect 99   4200 960 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 19     510  
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 wit inspect 95   3000 940 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    7000 true 2 wit inspect 13     470  
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 2 wit inspect 97   3000 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 18     500  
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 2 wit inspect 100   4000 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 27     630  
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 2 wit inspect 100   4000 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 24     610  
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 2 wit inspect 100   4200 870 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6800 true 2 wit inspect 26     610  
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 2 wit inspect 97   4300 940 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 true 2 wit inspect 15     470  
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 2 wit inspect 99   2300 1400 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    7000 true 2 wit inspect 25     630  
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 true 2 wit inspect 110   2700 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 true 2 wit inspect 37     890  
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 true 2 wit inspect 5.5 290 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 11     340  
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 2 wit inspect 95   2300 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 30     970  
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 2 wit inspect 3.8 290 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 7.6   300  
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 true 2 wit inspect 6.4 310 53 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 12     480  
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 2 wit inspect 3.5 260 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 7.7   310  
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 2 wit inspect 3.0 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 8.4   280  
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 true 2 wit inspect 59   1900 720 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 49     2800  
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 2 wit inspect 4.9 290 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6900 true 2 wit inspect 10     370  
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 2 wit inspect 3.8 280 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 true 2 wit inspect 10     360  
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 2 wit inspect 4.8 300 42 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 10     370  
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 2 wit inspect 4.0 290 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5800 true 2 wit inspect 8.9   340  
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 2 wit inspect 97   2400 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 11     390  
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 2 wit inspect 14   860 130 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 110     950  
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 2 wit inspect 3.6 260 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 12     390  
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 2 wit inspect 3.9 290 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 8.3   320  
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 2 wit inspect 3.8 290 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 8.6   350  
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 2 wit inspect 4.2 260 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 8.8   340  
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 2 wit inspect 3.5 290 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.2   300  
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 2 wit inspect 3.6 260 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 9.7   330  
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 2 wit inspect 4.3 290 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 840    7000 true 2 wit inspect 11     360  
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 2 wit inspect 3.4 260 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 8.4   310  
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 2 wit inspect 3.6 280 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 8.9   340  
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 2 wit inspect 3.6 260 32 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 true 2 wit inspect 7.9   320  
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 2 wit inspect 3.8 290 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 9.9   330  
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 2 wit inspect 3.6 280 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 8.8   320  
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 2 wit inspect 4.2 290 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 11     360  
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 true 2 wit inspect 4.0 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    1700 true 2 wit inspect 8.9   350  
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 2 wit inspect 3.6 290 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 7.3   310  
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 2 wit inspect 5.4 290 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 true 2 wit inspect 13     440  
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 2 wit inspect 3.7 280 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    7000 true 2 wit inspect 8.4   330  
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 2 wit inspect 3.8 290 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 9.1   340  
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 2 wit inspect 3.6 260 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 9.3   340  
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 2 wit inspect 4.3 270 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 8.8   340  
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 wit inspect 4.6 280 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 9.1   350  
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 2 wit inspect 94   2600 1300 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 15     710  
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 true 2 wit inspect 22   1300 180 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 19     510  
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 true 2 wit inspect 95   3100 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 22     810  
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 true 1 wit inspect 6.6 300 52 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 unknown 0 wit inspect 30     480  
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 2 wit inspect 5.7 300 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 14     420  
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 2 wit inspect 100   3100 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 33     860  
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 1 wit inspect 4.9 290 45 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 unknown 0 wit inspect 180     1000  
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 wit inspect 97   4200 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 15     480  
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 2 wit inspect 4.1 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 9.9   370  
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 - wit inspect - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 timeout 0 wit inspect 960     2200  
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 2 wit inspect 4.0 290 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 8.9   330  
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 2 wit inspect 4.5 290 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 true 2 wit inspect 10     330  
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 true 2 wit inspect 98   3200 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 14     470  
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 2 wit inspect 100   4100 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    3900 true 2 wit inspect 14     480  
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 2 wit inspect 98   4500 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 true 2 wit inspect 15     440  
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 2 wit inspect 4.4 290 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 10     350  
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 2 wit inspect 97   4000 950 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 20     600  
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 2 wit inspect 5.3 290 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 130     990  
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 2 wit inspect 97   4500 810 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 8.7   380  
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 wit inspect 29   1600 310 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    3700 unknown 0 wit inspect 31     460  
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 1 wit inspect 8.7 420 64 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 unknown 0 wit inspect 41     520  
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 wit inspect 98   4300 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 12     440  
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 wit inspect 5.0 300 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 unknown 0 wit inspect 32     490  
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 2 wit inspect 96   3600 980 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6200 true 2 wit inspect 11     400  
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 1 wit inspect 9.1 430 70 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 unknown 0 wit inspect 34     530  
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 wit inspect 4.9 290 38 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 unknown 0 wit inspect 28     520  
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 wit inspect 9.0 340 75 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 unknown 0 wit inspect 60     670  
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 wit inspect 9.2 330 71 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 unknown 0 wit inspect 50     670  
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 wit inspect 11   440 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 unknown 0 wit inspect 180     1200  
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 1 wit inspect 4.9 300 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 false(unreach-call) -16 wit inspect 19     650  
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 2 wit inspect 4.2 290 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 7.8   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--xen-kbdfront.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 14     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--mouse--gpio_mouse.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 7.9 330 56 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    7000 unknown 0 wit inspect 24     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--mouse--vsxxxaa.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 7.8 380 63 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4100 timeout 0 wit inspect 960     4500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--ad7879-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3500 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6900 true 2 wit inspect 8.6   360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--cyttsp_spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   1400 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 true 2 wit inspect 12     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--dynapro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.1 300 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 unknown 0 wit inspect 38     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--egalax_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 33   1400 320 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 13     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--fujitsu_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.0 300 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 unknown 0 wit inspect 32     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--gunze.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.9 300 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 unknown 0 wit inspect 46     540  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--hampshire.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.3 300 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5700 unknown 0 wit inspect 53     560  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--inexio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.2 300 39 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 unknown 0 wit inspect 36     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--mtouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.9 290 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 unknown 0 wit inspect 39     530  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--penmount.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c - wit inspect - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 15     450  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchit213.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.4 300 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 unknown 0 wit inspect 50     580  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchright.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c - wit inspect - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 unknown 0 wit inspect 32     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.7 300 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 unknown 0 wit inspect 32     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--tsc40.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 6.7 300 62 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 unknown 0 wit inspect 40     570  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--wacom_w8001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2400 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 16     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--avm_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.2 290 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 12     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--b1pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 13   580 120 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 14    610 unknown 0 wit inspect 87     960  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--b1pcmcia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 true 2 wit inspect 8.9   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--t1pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.7 290 41 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 10    500 true 2 wit inspect 14     450  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--eicon--divadidd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 97   2400 880 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 unknown 0 wit inspect 5.5   230  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--avma1_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.9 300 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 13     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--elsa_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.1 300 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 12     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--sedlbauer_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.7 290 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 true 2 wit inspect 16     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--teles_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.9 290 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 16     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-bd2802.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3700 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 27     620  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-lp5521.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   1900 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    7000 true 2 wit inspect 18     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-ot200.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 8.0 330 57 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    7000 true 2 wit inspect 140     3700  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-backlight.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 8.8   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-default-on.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.2 280 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 6.1   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.0 290 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 11     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--macintosh--mac_hid.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.9 290 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5400 unknown 0 wit inspect 48     630  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--md--dm-zero.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.9 280 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 8.2   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--max2165.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3300 990 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 19     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mc44s803.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.4 300 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 true 2 wit inspect 15     560  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2060.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 14   570 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 true 2 wit inspect 19     590  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2131.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   4100 980 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 16     440  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2266.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2500 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 14     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mxl5007t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   3600 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 25     670  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--qt1010.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   1000 1400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6000 true 2 wit inspect 23     590  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda18218.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3300 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 true 2 wit inspect 19     570  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda8290.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   2900 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 27     610  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda9887.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 110   3400 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 28     820  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--bt8xx--dvb-bt8xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3700 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 31     800  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-a800.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.1 320 46 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 26     790  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-au6610.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.5 330 54 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    7000 true 2 wit inspect 28     820  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   3800 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 71     2000  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   2600 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 110     4700  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-ce6230.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 12   470 86 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 true 2 wit inspect 20     800  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-cinergyT2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2300 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6900 true 2 wit inspect 32     1200  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-mb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 16   780 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5600 true 2 wit inspect 93     3700  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-mc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 300 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 24     780  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-digitv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3700 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 37     1100  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtt200u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   1900 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 100     4600  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtv5100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2900 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 25     740  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-gl861.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 7.3 300 60 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 28     790  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-mxl111sf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   2300 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5100 true 2 wit inspect 90     3700  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-nova-t-usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2700 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 26     780  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-pctv452e.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   4300 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 840    7000 true 2 wit inspect 220     4900  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-rtl28xxu.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   4000 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6900 true 2 wit inspect 80     1900  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-ttusb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   2600 900 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 81     2600  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-umt-010.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.1 310 48 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    7000 true 2 wit inspect 26     810  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3500 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 110     3000  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--mxl111sf-demod.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   2900 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 28     660  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--cxd2820r.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   2700 1500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 true 2 wit inspect 31     850  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dib3000mb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   7500 8300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .020 4.9
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dib3000mc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   4300 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 31     790  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dvb_dummy_fe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 50     1800  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--ec100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 64   2000 660 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 21     760  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--it913x-fe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 99   2900 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 out of memory 0 wit inspect 460     7000  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--rtl2830.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3000 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 24     740  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--stb6000.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 10   550 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 20     560  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tda18271c2dd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3700 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 54     2700  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tda826x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.3 290 54 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 16     550  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tua6100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.6 310 51 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 18     530  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--ttpci--budget-patch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 34   1400 340 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 23     540  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--ttpci--budget.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   3600 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 28     800  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-adstech-dvb-t-pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 8.1   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-alink-dtu-m.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 21 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 7.1   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-anysee.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 9.1   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-apac-viewcomp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 7.4   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-asus-pc39.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.7   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-ati-tv-wonder-hd-600.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 7.4   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-ati-x10.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 280 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 8.2   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-a16d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.3   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-cardbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 9.8   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-dvbt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 8.5   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-m135a.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 260 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 9.6   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-m733a-rm-k6.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 8.0   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-rm-ks.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 7.2   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 7.8   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avertv-303.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.1   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-azurewave-ad-tu700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 8.7   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-behold-columbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 8.2   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-behold.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 9.7   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-budget-ci-old.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 true 2 wit inspect 8.9   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-cinergy-1400.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    7000 true 2 wit inspect 7.9   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-cinergy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 8.9   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dib0700-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 10     320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dib0700-rc5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 270    7000 true 2 wit inspect 12     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-digitalnow-tinytwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 510    7000 true 2 wit inspect 8.2   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-digittrade.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 8.4   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dm1105-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.6   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dntv-live-dvb-t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 8.4   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dntv-live-dvbt-pro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 8.3   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-em-terratec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 260 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 7.1   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-encore-enltv-fm53.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.5 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 7.3   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-encore-enltv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.8   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-encore-enltv2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    7000 true 2 wit inspect 7.8   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-evga-indtube.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 6.5   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-eztv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 9.1   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-flydvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 7.6   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-flyvideo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    7000 true 2 wit inspect 7.6   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-fusionhdtv-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 true 2 wit inspect 8.7   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-gadmei-rm008z.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 21 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 7.5   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-genius-tvgo-a11mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 8.5   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-gotview7135.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 7.5   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-hauppauge.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    7000 true 2 wit inspect 12     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-imon-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 8.8   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-imon-pad.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 12     350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-iodata-bctv7e.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.9   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-it913x-v1.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.0 280 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 8.1   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-it913x-v2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    7000 true 2 wit inspect 8.5   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kaiomy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 7.6   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kworld-315u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 7.5   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kworld-pc150u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 8.3   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kworld-plus-tv-analog.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 5.1   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-leadtek-y04g0051.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 8.7   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-lirc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 2.6 250 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 error (7) 0 wit inspect 7.3   210  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-lme2510.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 21 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    7000 true 2 wit inspect 9.0   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-manli.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 9.2   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-medion-x10.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 8.4   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-digivox-ii.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 7.1   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-digivox-iii.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 5.2   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-tvanywhere-plus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 7.6   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-tvanywhere.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 7.1   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-nebula.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 8.7   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-nec-terratec-cinergy-xs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 12     350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-norwood.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 9.5   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-npgtech.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 8.0   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pctv-sedna.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 8.6   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pinnacle-color.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 7.5   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pinnacle-grey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 8.0   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pinnacle-pctv-hd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 7.0   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview-002t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 7.3   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview-mk12.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 290    7000 true 2 wit inspect 9.2   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview-new.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.0 280 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 7.8   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 7.5   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-powercolor-real-angel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 7.4   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-proteus-2309.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 6.7   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-purpletv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 8.2   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pv951.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 7.1   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-rc6-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.9 260 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 8.7   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-real-audio-220-32-keys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 7.1   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-snapstream-firefly.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 8.0   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-streamzap.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    7000 true 2 wit inspect 7.8   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tbs-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 22 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 7.4   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-technisat-usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 21 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 7.2   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-terratec-cinergy-xs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 510    7000 true 2 wit inspect 9.8   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-terratec-slim-2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 6.9   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-terratec-slim.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 24 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 7.0   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tevii-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.2   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tivo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.5 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 8.0   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-total-media-in-hand.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 7.5   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-trekstor.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 290    7000 true 2 wit inspect 7.5   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tt-1500.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 7.9   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-twinhan1027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 true 2 wit inspect 8.4   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-videomate-m1f.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 10     300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-videomate-s350.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 250 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 8.8   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-videomate-tv-pvr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 7.7   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-winfast-usbii-deluxe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.7 250 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 7.0   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-winfast.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 250 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 9.2   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--cx231xx--cx231xx-dvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3600 950 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5800 true 2 wit inspect 30     820  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--em28xx--em28xx-dvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   3200 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 37     850  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_benq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 8.0 310 59 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 error (7) 0 wit inspect 9.8   220  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_finepix.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 8.1 360 64 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 17     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_jl2005bcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3400 990 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 17     540  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_pac207.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2800 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 22     630  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_sq905c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.7 290 49 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 820    7000 true 2 wit inspect 14     430  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_stv0680.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 6.5 290 54 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 error (7) 0 wit inspect 10     230  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--zoran--zr36016.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3100 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5800 true 2 wit inspect 13     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--message--i2o--i2o_bus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 260 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 9.1   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--message--i2o--i2o_scsi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   2700 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 20     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--janz-cmodio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   4500 960 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 13     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--rdc321x-southbridge.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 280 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 9.5   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--tps6105x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 39   2000 390 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 unknown 0 wit inspect 34     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--tps6507x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.1 290 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 unknown 0 wit inspect 31     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--tps65217.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.1 280 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 unknown 0 wit inspect 28     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--ucb1400_core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.2 300 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 9.8   360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--wl1273-core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 6.3 290 50 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 unknown 0 wit inspect 180     950  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--wm8400-core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   2900 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    7000 true 2 wit inspect 19     620  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--apds9802als.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.3 290 44 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 14     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--bmp085.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.7 290 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 14     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--c2port--c2port-duramar2150.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.4 250 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 8.8   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--eeprom--eeprom_93xx46.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.4 290 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 14     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--isl29020.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.9 300 43 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 unknown 0 wit inspect 29     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--sgi-xp--xp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.5 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 true 2 wit inspect 25     600  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--ti_dac7512.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 280 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 8.5   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--tifm_core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.2 300 44 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 18     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mmc--host--sdricoh_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3600 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 18     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--docprobe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3800 940 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 12     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--mtdram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.6 290 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    7000 true 2 wit inspect 7.7   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--ftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   2900 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 25     620  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--inftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   3500 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5700 true 2 wit inspect 32     830  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--intel_vr_nor.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 8.4 430 72 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    7000 true 2 wit inspect 13     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--mtdblock_ro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.5 280 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 7.0   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--nftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   3500 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    6300 true 2 wit inspect 33     620  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--onenand--onenand_sim.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 43 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 820    7000 true 2 wit inspect 14     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--tests--mtd_oobtest.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3500 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    1400 true 2 wit inspect 19     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--tests--mtd_pagetest.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   2900 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    630 true 2 wit inspect 16     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--ubi--gluebi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.6 300 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 13     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--arcnet--com20020_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 28   1100 260 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 76     1400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--act200l-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.7 320 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5100 unknown 0 wit inspect 24     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--litelink-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   3700 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 8.6   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--ma600-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 7.2 320 60 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 false(unreach-call) -16 wit inspect 21     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--tekram-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 50   1500 500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 unknown 0 wit inspect 39     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--amd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 290 30 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 9.0   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--broadcom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 11   560 88 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 true 2 wit inspect 18     640  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--cicada.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 270 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 8.7   360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--davicom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 39 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 true 2 wit inspect 10     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--et1011c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 280 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 8.4   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--icplus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 9.7   390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--lxt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 12     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.4 310 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 unknown 0 wit inspect 210     1200  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--micrel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 39 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 14     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--national.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 40 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 true 2 wit inspect 8.9   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--qsemi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.9 290 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 9.4   360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--realtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.4 260 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 7.7   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--smsc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 13     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--spi_ks8995.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 7.4 350 54 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 12     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--ste10Xp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.3 290 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 9.6   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--vitesse.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.5 260 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 9.8   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--ppp--bsd_comp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2400 750 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    4000 true 2 wit inspect 19     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--ppp--ppp_mppe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 99   3700 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 error (7) 0 wit inspect 6.7   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--sungem_phy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   2600 970 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 20     600  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--team--team_mode_activebackup.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.3 300 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 8.6   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--team--team_mode_roundrobin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.1 300 50 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 9.3   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--airo_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.0 300 51 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 true 2 wit inspect 14     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--ath--ath6kl--ath6kl_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 7.9 360 57 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 timeout 0 wit inspect 960     1400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--mwifiex--mwifiex_pcie.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   3500 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    2600 true 2 wit inspect 46     960  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--orinoco--orinoco_nortel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 18   660 170 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 unknown 0 wit inspect 57     750  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--orinoco--orinoco_pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 12   580 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6200 true 2 wit inspect 13     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--orinoco--orinoco_tmd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.1 300 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 14     450  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--wl1251--wl1251_spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.4 460 78 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 12     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--wl12xx--wl12xx_sdio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2400 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    7000 true 2 wit inspect 15     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--parport--parport_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.8 300 48 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 14     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--pci--ioapic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 290 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 9.5   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--pci--pci-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 270 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    2100 true 2 wit inspect 31     1500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--asus-nb-wmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 280 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 9.3   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--intel_menlow.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 12   450 91 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 25     760  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--panasonic-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   4200 970 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 19     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.0 300 52 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    7000 true 2 wit inspect 14     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--toshiba_bluetooth.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.3 290 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 11     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--xo15-ebook.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.3 290 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 10     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--power--max8903_charger.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 10   450 86 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 14     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 94   2400 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 true 2 wit inspect 16     540  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--power--wm831x_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   3000 890 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 true 2 wit inspect 17     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--gpio-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   2200 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 15     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--max1586.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 16   790 150 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 unknown 0 wit inspect 48     590  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--max8649.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 51   2100 540 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 14     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--userspace-consumer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.1 290 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 false(unreach-call) -16 wit inspect 29     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--virtual.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.9 270 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    7000 true 2 wit inspect 19     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm831x-dcdc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   2300 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 23     650  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm831x-isink.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 6.0 300 48 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    7000 unknown 0 wit inspect 27     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm831x-ldo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2400 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 true 2 wit inspect 18     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm8400-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.7 300 42 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 true 2 wit inspect 15     440  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-da9052.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.3 300 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 15     440  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds1390.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 10     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds1553.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   1800 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 13     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds3232.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 10   430 82 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 15     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds3234.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.1 290 42 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 10     380  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-m41t93.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 20   980 190 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 14     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-m41t94.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.9 450 82 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 13     440  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-m48t86.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 14     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-max6902.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.8 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 true 2 wit inspect 11     380  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-mc13xxx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   3200 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 15     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-pcap.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.9 300 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 9.3   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-pcf2123.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   1800 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 16     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-r9701.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 49   2500 440 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 41     550  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-rs5c348.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.0 430 65 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 14     430  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-stk17ta8.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   1600 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 14     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-test.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 true 2 wit inspect 9.9   360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-v3020.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   4000 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 22     530  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 12   550 98 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 15     450  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--dmx3191d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   1800 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5600 true 2 wit inspect 14     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--iscsi_boot_sysfs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   1200 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 18     630  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--pcmcia--sym53c500_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 110   4700 960 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 24     770  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--qlogicfas408.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   2600 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5900 true 2 wit inspect 18     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--spi--spi-tle62x0.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   1600 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 12     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--android--switch--switch_gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 280 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 12     340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--comedi--drivers--8255.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3200 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6500 true 2 wit inspect 13     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--comedi--drivers--comedi_bond.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 20   1000 200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     1000  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--addac--adt7316-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3700 740 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 8.0   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad5930.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 290 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 11     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9832.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 7.1 300 55 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 true 2 wit inspect 17     540  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9850.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 280 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 8.7   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9852.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 43 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 18     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9910.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.0 300 51 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 18     530  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9951.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.0 300 46 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 510    7000 true 2 wit inspect 15     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--resolver--ad2s90.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 290 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 10     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--phison--phison.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.5 290 38 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    7000 true 2 wit inspect 14     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_acntsa.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 260 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 true 2 wit inspect 13     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_bns.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.8 260 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 12     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_dummy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.1 260 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 10     370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_ltlk.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 15   750 130 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 25     1000  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_soft.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2700 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 true 2 wit inspect 17     560  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_spkout.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   1300 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 12     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_txprt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.0 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 true 2 wit inspect 10     370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--telephony--ixj_pcmcia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 23   950 240 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 15     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--vme--boards--vme_vmivme7805.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 290 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 8.8   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--zram--zram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.5 310 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    510 true 2 wit inspect 17     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--target--loopback--tcm_loop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 15   600 130 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 true 2 wit inspect 28     790  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--altera_jtaguart.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   3100 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 16     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--altera_uart.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3600 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 22     640  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--mfd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   3100 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 26     610  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--uartlite.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3700 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 17     580  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--xilinx_uartps.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3700 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 19     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uio--uio_aec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 true 2 wit inspect 12     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uio--uio_pci_generic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 290 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 10     340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uio--uio_sercos3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.9 300 48 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 unknown 0 wit inspect 33     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--atm--xusbatm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.2 330 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  300 true 2 wit inspect 16     550  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--misc--cypress_cy7c63.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.5 290 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    7000 unknown 0 wit inspect 69     690  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--misc--cytherm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.9 290 50 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 unknown 0 wit inspect 27     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--otg--ab8500-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 11   450 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 true 2 wit inspect 14     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--otg--nop-usb-xceiv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.6 260 30 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 true 2 wit inspect 9.5   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--ipaq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 8.8 320 72 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    7000 out of memory 0 wit inspect 380     7000  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--ir-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3200 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6600 true 2 wit inspect 16     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--iuu_phoenix.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   2500 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 25     620  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--metro-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3100 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 18     650  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--spcp8x5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   3600 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 18     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-alauda.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.4 310 54 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    7000 true 2 wit inspect 9.9   400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-cypress.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 290 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    7000 true 2 wit inspect 15     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-datafab.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.3 330 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    7000 true 2 wit inspect 17     530  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-freecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.7 320 38 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 15     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-jumpshot.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.9 310 43 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 true 2 wit inspect 12     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-sddr09.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.5 320 51 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 47     1100  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-sddr55.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.4 320 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 11     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-usbat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.6 320 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 true 2 wit inspect 11     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uwb--i1480--i1480-est.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 290 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 8.3   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--ili9320.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 8.3 430 63 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 12     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--l4f00242t03.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 29   1000 280 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 13     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--lms283gf05.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   4400 960 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 16     440  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--tdo24m.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3800 1200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 15     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--vgg2432a4.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 19   1200 170 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6200 unknown 0 wit inspect 27     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--n411.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   3100 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3  350 true 2 wit inspect 8.3   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--masters--ds2490.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   3300 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 true 2 wit inspect 21     630  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--masters--matrox_w1.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 270 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 10     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--masters--w1-gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 3.8 280 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    7000 unknown 0 wit inspect 19     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_bq27000.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.9 280 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 8.1   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2408.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.3 290 56 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 true 2 wit inspect 73     800  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2423.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 280 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 6.1   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2431.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 8.1 340 61 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    5000 true 2 wit inspect 12     380  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2433.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   3600 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6800 true 2 wit inspect 17     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2760.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 9.0   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2780.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.7 290 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    7000 true 2 wit inspect 8.7   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2781.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 270 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 9.3   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_smem.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.0 250 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 5.8   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--watchdog--sbc_epx_c3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 8.7 380 71 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6200 timeout 0 wit inspect 920     900  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--watchdog--wm831x_wdt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 10   680 92 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 false(unreach-call) -16 wit inspect 15     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--gpu--drm--drm_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 300 38 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 6.4   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--keyboard--gpio_keys_polled.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   1800 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    7000 true 2 wit inspect 9.2   390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ab8500-ponkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 280 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5400 true 2 wit inspect 8.4   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ad714x-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 290 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 8.0   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ad714x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.6   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--adxl34x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 7.0 300 54 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 true 2 wit inspect 11     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--mma8450.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 290 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.1   360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--mpu3050.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.7 290 50 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 true 2 wit inspect 13     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--pcap_keys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.7 280 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 8.2   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--pcf50633-input.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 290 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    7000 true 2 wit inspect 7.9   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--pcspkr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.7 290 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 false(unreach-call) -16 wit inspect 22     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--rotary_encoder.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.8 330 56 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 11     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--wm831x-on.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 290 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 true 2 wit inspect 8.9   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--touchscreen--eeti_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.5 300 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 false(unreach-call) -16 wit inspect 24     430  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--touchscreen--max11801_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.4 290 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 false(unreach-call) -16 wit inspect 25     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--touchscreen--stmpe-ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.3 290 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 14     450  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--leds--leds-dac124s085.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.8 300 44 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 false(unreach-call) -16 wit inspect 9.8   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--leds--leds-pca9633.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.2 290 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 timeout 0 wit inspect 960     720  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--leds--leds-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.1 290 39 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 true 2 wit inspect 16     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--common--tuners--mt20xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99   4100 920 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 true 2 wit inspect 21     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-cinergyT2.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 97   1800 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 13     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-common.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.4 310 41 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 6.5   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtt200u.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 38   1700 380 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5700 false(unreach-call) -16 wit inspect 16     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-mxl111sf.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 10   460 82 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    7000 true 2 wit inspect 7.4   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 22   1100 200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 false(unreach-call) -16 wit inspect 16     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--frontends--isl6405.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 290 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 5.7   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--frontends--isl6421.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 290 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 5.5   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--frontends--lnbp21.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 290 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 6.3   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--dvb--frontends--lnbp22.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 280 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 7.8   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--media--video--cx88--cx88-vp3054-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 290 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 11     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--mtd--ar7part.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 56   3900 570 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 8.1   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--mtd--devices--doc2001plus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.0 300 39 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 6.5   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--irda--esi-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.4 300 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 unknown 0 wit inspect 17     380  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--irda--girbil-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 6.5 300 55 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5700 unknown 0 wit inspect 21     420  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--irda--mcp2120-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 5.7 330 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5700 unknown 0 wit inspect 21     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--irda--old_belkin-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.5 300 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 unknown 0 wit inspect 19     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--usb--cdc_subset.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.5 320 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 6.3   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--net--usb--plusb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 320 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 7.7   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--platform--x86--mxm-wmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.6 290 31 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 6.4   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--power--wm831x_backup.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.5 300 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6900 true 2 wit inspect 9.2   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--scsi--scsi_wait_scan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.6 260 23 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 5.3   250  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--android--switch--switch_class.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8 290 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    7000 true 2 wit inspect 7.0   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--comedi--drivers--comedi_parport.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.0 270 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 true 2 wit inspect 64     680  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--comedi--drivers--unioxx5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 95   2200 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 10     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--iio--addac--adt7316-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 96   2400 910 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 true 2 wit inspect 8.3   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--iio--kfifo_buf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.3 260 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 5.9   260  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--iio--meter--ade7854-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.5 310 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 820    7000 true 2 wit inspect 11     430  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--iio--ring_sw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 290 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 true 2 wit inspect 5.9   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--media--cxd2099--cxd2099.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   4200 930 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 true 2 wit inspect 46     1700  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--serqt_usb2--serqt_usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   3000 1200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 true 2 wit inspect 38     800  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--staging--zram--zram.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.0 330 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 6.3   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--dwc3--dwc3-pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 290 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    7000 true 2 wit inspect 7.8   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--misc--trancevibrator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 4.6 290 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    7000 false(unreach-call) -16 wit inspect 22     380  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--cp210x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 98   2500 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 true 2 wit inspect 28     640  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--empeg.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 280 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 7.9   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--usb--serial--funsoft.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.7 280 32 - wit inspect - wit inspect -