Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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-12-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.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 14     4800 160    false(unreach-call) 1 wit inspect 25    630 error (7) 0 wit inspect 4.4   440   timeout 0 wit inspect 4.5  280 error (2) 0 wit inspect 6.6    82    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .40  120 5.2  error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0022 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .69  210 7.3  error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 52 error (invalid witness file) 0 wit inspect .0036 .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 false(unreach-call) 0 wit inspect 8.8   660 94    timeout 0 wit inspect 91    1200 true -32 wit inspect 32     800   unknown 0 wit inspect 8.4  330 error (2) 0 wit inspect 2.7    33    - 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 8.6   700 110    false(unreach-call) 1 wit inspect 78    840 unknown 0 wit inspect 5.8   300   unknown 0 wit inspect 6.0  320 error (2) 0 wit inspect 2.7    35    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i out of memory 0 wit inspect 69     15000 880    error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0011 .26 - 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     5900 7600    error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 2.2   780 27    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 5.2   1300 64    error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .73 51 error (invalid witness file) 0 wit inspect .0012 .30 - 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) 0 wit inspect 3.7   130 42    error (invalid witness file) 0 wit inspect 3.9  200 true -32 wit inspect 11     400   error (invalid witness file) 0 wit inspect 4.0  220 error (1) 0 wit inspect .92   19    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 6.3   160 73    timeout 0 wit inspect 92    2300 true -32 wit inspect 15     480   unknown 0 wit inspect 7.6  410 error (2) 0 wit inspect 1.1    20    - 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 unknown 0 wit inspect .75  320 9.6  error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0011 .26 - 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) 0 wit inspect 1.5   130 14    timeout 0 wit inspect 92    1600 true -32 wit inspect 17     500   unknown 0 wit inspect 3.8  270 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 3.9   200 50    timeout 0 wit inspect 91    1100 true -32 wit inspect 19     500   unknown 0 wit inspect 4.0  270 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .44  97 4.9  error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 9.2   260 110    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 3.4   360 47    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 50     7800 520    - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 41    1100 true 2 wit inspect 97     2700  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 17     430 230    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 42     1900  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     12000 6900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.9
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     13000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .023 5.0
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 23     6300 310    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6500 timeout 0 wit inspect 960     5300  
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     2100 7100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .022 4.8
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 2.0   190 23    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 56     2800  
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 2.5   440 26    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5800 true 2 wit inspect 45     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 .24  40 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    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 79     4200 760    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 30     600  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 370     13000 3800    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 44     860  
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 19     1300 210    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 32     1400  
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 18     460 250    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5700 true 2 wit inspect 32     810  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i false(unreach-call) -16 wit inspect 3.8   120 40    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4  210 true 2 wit inspect 12     380  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 28     730 280    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 5.0
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 21     1600 260    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6000 true 2 wit inspect 19     820  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 21     150 180    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 19     620  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i out of memory 0 wit inspect 330     15000 4700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.8
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i out of memory 0 wit inspect 98     15000 940    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .024 4.9
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     7100 9500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 2.6   280 34    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .33  77 3.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 4.9
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 12     420 110    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 5.0
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 17     390 180    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6000 true 2 wit inspect 37     1200  
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 out of memory 0 wit inspect 120     15000 1400    error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0013 .28 - 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 42     400 470    timeout 0 wit inspect 92    2500 true -32 wit inspect 14     490   unknown 0 wit inspect 5.3  410 error (2) 0 wit inspect 1.3    21    - 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 timeout 0 wit inspect 900     11000 12000    error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0018 .29 - 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 1.4   170 13    false(unreach-call) 1 wit inspect 19    610 unknown 0 wit inspect 5.3   310   unknown 0 wit inspect 4.9  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 unknown 0 wit inspect 1.5   390 18    error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .28 - 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 unknown 0 wit inspect .47  160 5.3  error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .044 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0011 .26 - 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 unknown 0 wit inspect .17  50 1.5  error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0037 .29 - 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 unknown 0 wit inspect .19  67 2.0  error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0012 .29 - 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 unknown 0 wit inspect .72  150 6.2  error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0012 .27 - 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) 1 wit inspect 8.6   460 110    false(unreach-call) 1 wit inspect 12    480 true -32 wit inspect 18     590   unknown 0 wit inspect 6.5  280 error (2) 0 wit inspect 1.7    25    - 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 1.2   110 11    false(unreach-call) 1 wit inspect 7.2  390 true -32 wit inspect 13     590   unknown 0 wit inspect 4.8  290 error (2) 0 wit inspect 1.8    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 timeout 0 wit inspect 900     1800 11000    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0031 .26 - 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 false(unreach-call) 0 wit inspect 1.7   220 17    timeout 0 wit inspect 92    1300 timeout 0 wit inspect 97     4600   unknown 0 wit inspect 8.9  360 error (2) 0 wit inspect 3.3    39    - 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 .51  66 6.0  false(unreach-call) 1 wit inspect 8.2  290 true -32 wit inspect 9.7   470   unknown 0 wit inspect 3.5  270 error (2) 0 wit inspect 1.3    21    - 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) 0 wit inspect 1.4   210 12    timeout 0 wit inspect 94    2700 true -32 wit inspect 43     1300   unknown 0 wit inspect 8.3  330 error (2) 0 wit inspect 3.0    35    - 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) 0 wit inspect 13     610 160    timeout 0 wit inspect 92    1900 true -32 wit inspect 33     920   unknown 0 wit inspect 7.0  430 error (2) 0 wit inspect 3.0    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 900     3100 9300    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c unknown 0 wit inspect .43  120 4.0  error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .26 - 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 unknown 0 wit inspect .37  110 4.5  error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c unknown 0 wit inspect .62  180 8.3  error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c unknown 0 wit inspect .74  200 7.1  error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0010 .27 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c unknown 0 wit inspect 1.5   300 15    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c unknown 0 wit inspect .57  160 5.2  error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c unknown 0 wit inspect 1.3   250 10    error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - 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     1500 10000    error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .32 - 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 900     3700 11000    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0011 .26 - 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 out of memory 0 wit inspect 760     15000 5500    error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .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 true -32 wit inspect 20     450 260    timeout 0 wit inspect 92    3000 timeout 0 wit inspect 96     2600   unknown 0 wit inspect .68 51 error (1) 0 wit inspect .094  9.1  - 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 out of memory 0 wit inspect 73     15000 770    error (invalid witness file) 0 wit inspect .42 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .26 - 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 true -32 wit inspect 44     1800 490    timeout 0 wit inspect 95    2100 timeout 0 wit inspect 98     1300   unknown 0 wit inspect .72 51 error (1) 0 wit inspect .094  9.4  - 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 .28  38 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 14     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 2 wit inspect .26  34 2.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6700 true 2 wit inspect 9.4   350  
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 .29  37 3.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 13     460  
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 .48  48 5.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6600 true 2 wit inspect 9.7   450  
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 .25  40 2.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 890    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--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  33 3.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    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--auxdisplay--cfag12864bfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .23  37 2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 true 2 wit inspect 6.7   370  
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 .18  31 1.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 6.2   280  
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 1.2   72 16    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 170     1000 1100    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 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--block--paride--comm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8   140 39    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6900 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--block--paride--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.3   140 56    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 24     570  
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 41     410 300    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    7000 true 2 wit inspect 25     580  
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 17     310 150    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 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--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .76  55 9.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 620    7000 true 2 wit inspect 13     460  
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 2.2   100 23    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 true 2 wit inspect 11     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 17     280 120    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 25     610  
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 14     280 110    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    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 17     340 170    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6800 true 2 wit inspect 18     620  
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 .78  58 8.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    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--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0   140 44    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 28     590  
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 68     620 460    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 900    7000 true 2 wit inspect 32     880  
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 .47  33 5.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 11     330  
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 .47  51 5.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 33     750  
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 .23  35 2.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    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--char--uv_mmtimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .93  73 10    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 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--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .21  31 2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 7.4   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 .096 28 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 9.0   300  
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 .68  71 7.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    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--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  36 3.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    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--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .22  34 2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 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--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .27  35 3.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 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--gpio--gpio-tps65912.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .26  32 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 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--gpio--gpio-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .48  39 5.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 13     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 1.0   65 15    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 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--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .17  38 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    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--stub--poulsbo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .15  34 2.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 9.9   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 .24  33 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 7.8   330  
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 1.8   120 18    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 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--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .16  32 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.1   310  
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 .21  33 2.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    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-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.2   84 16    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6900 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--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .16  32 1.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 9.4   320  
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 .12  32 1.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 9.3   330  
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 .53  50 6.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 7.6   330  
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 .26  35 3.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 13     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 .14  32 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    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--hid--hid-petalynx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .68  48 6.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 9.6   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 .49  35 6.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    1700 true 2 wit inspect 8.6   340  
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 .17  32 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    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 1.5   90 20    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 13     430  
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 .18  34 1.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    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--hid--hid-sunplus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .22  33 2.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    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--hid--hid-tivo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .38  42 4.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 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--hid--hid-topseed.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.3   150 25    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 900    7000 true 2 wit inspect 8.7   350  
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 5.4   320 70    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    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 .19  33 2.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 18     700  
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 2.4   99 29    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    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--hid--hid-waltop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .49  42 7.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 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--hid--hid-zydacron.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.5   90 17    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 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--hwmon--ads7871.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .26  38 3.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 8.2   410  
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 35     640 430    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6500 true 2 wit inspect 42     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 2 wit inspect .66  52 9.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 true 2 wit inspect 16     530  
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  53 11    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 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--hwmon--max1111.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .23  36 2.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 9.2   360  
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 900    6400 true 2 wit inspect 13     450  
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 .17  32 1.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 true 2 wit inspect 10     310  
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 .23  33 2.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5200 true 2 wit inspect 9.3   320  
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 6.7   85 64    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6400 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--i2c--busses--i2c-diolan-u2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 8.6   170 88    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    3500 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-tiny-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .73  59 9.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 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 .27  38 3.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    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--ide--cmd640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.7   70 50    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 true 2 wit inspect 20     620  
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 .29  39 2.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    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--input--gameport--lightning.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .67  39 8.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 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--input--joystick--magellan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .44  40 5.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 9.5   380  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--spaceball.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .78  60 8.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 14     440  
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 .59  52 7.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5000 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--input--joystick--stinger.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .33  35 3.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    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--input--joystick--twidjoy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .41  38 5.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 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--input--joystick--warrior.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .52  45 6.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 9.9   390  
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 2 wit inspect .29  34 3.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    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--input--keyboard--newtonkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .27  35 3.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 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--input--keyboard--stowaway.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  35 2.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    7000 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--input--keyboard--xtkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .27  35 3.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    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--input--misc--atlas_btns.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .20  36 1.9  - 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--input--misc--cma3000_d0x_i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .23  36 2.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 7.2   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 .41  46 4.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    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--input--mouse--gpio_mouse.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .25  37 3.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 true 2 wit inspect 9.2   370  
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 2 wit inspect 9.6   470 110    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 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--input--touchscreen--ad7879-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .92  46 11    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6900 true 2 wit inspect 6.4   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 .40  42 5.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    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--input--touchscreen--dynapro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .32  35 3.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 11     370  
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 .42  42 5.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 7.2   380  
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 2 wit inspect .32  35 3.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    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--input--touchscreen--gunze.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .32  35 3.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    7000 true 2 wit inspect 9.7   370  
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 2 wit inspect .33  36 3.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 9.3   380  
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 2 wit inspect .30  35 3.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 true 2 wit inspect 8.9   360  
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 2 wit inspect .30  36 3.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 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--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 650    7000 true 2 wit inspect 13     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 2 wit inspect .32  35 3.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    7000 true 2 wit inspect 11     370  
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 out of memory 0 wit inspect 610    7000 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--input--touchscreen--touchwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .32  35 3.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 true 2 wit inspect 8.9   360  
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 2 wit inspect .37  36 4.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 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--input--touchscreen--wacom_w8001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.1   93 24    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 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--isdn--hardware--avm--avm_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .36  39 4.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 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--isdn--hardware--avm--b1pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .66  63 8.0  - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 9.6  590 true 2 wit inspect 11     480  
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 .19  34 1.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 11     320  
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 .41  47 5.4  - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 10    490 true 2 wit inspect 14     440  
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 unknown 0 wit inspect .31  63 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
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 .24  37 2.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    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--isdn--hisax--elsa_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .37  40 3.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 15     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 .33  39 4.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 840    7000 true 2 wit inspect 14     440  
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 .34  40 4.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 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--leds--leds-bd2802.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.1   100 13    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 24     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 .92  75 12    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    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--leds--leds-ot200.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .19  37 2.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 true 2 wit inspect 13     720  
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 .21  37 2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 8.8   360  
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 .17  30 1.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 6.0   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 .19  34 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 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--macintosh--mac_hid.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .30  34 3.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 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--md--dm-zero.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .18  35 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    7000 true 2 wit inspect 7.8   330  
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 1.4   64 20    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 17     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 .83  52 8.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 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--media--common--tuners--mt2060.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .66  50 7.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 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--media--common--tuners--mt2131.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .46  46 3.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 13     430  
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 .59  50 8.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 13     450  
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 timeout 0 wit inspect 900     2000 7700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .018 5.0
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 5.2   140 51    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 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--media--common--tuners--tda18218.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6   93 50    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 true 2 wit inspect 12     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 4.1   140 48    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 32     590  
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 timeout 0 wit inspect 900     1800 7600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 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--bt8xx--dvb-bt8xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8   180 50    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 true 2 wit inspect 32     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-a800.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .29  50 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 20     730  
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 .44  55 5.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 16     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-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     7100 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.8
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 timeout 0 wit inspect 900     3900 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.8
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 .41  60 4.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 28     750  
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 .48  70 5.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    7000 true 2 wit inspect 38     1000  
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 1.6   90 17    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 62     2400  
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 .24  47 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 19     730  
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 .89  73 11    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 760    7000 true 2 wit inspect 24     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 1.0   110 13    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 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 .45  56 5.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 true 2 wit inspect 28     590  
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 .45  55 5.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 27     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-mxl111sf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 710     1700 6700    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5100 true 2 wit inspect 110     3900  
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 .40  55 3.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 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-pctv452e.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     3700 8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.9
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 1.3   100 16    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6900 true 2 wit inspect 67     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 3.0   130 38    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 58     2400  
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 .33  52 4.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 14     750  
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 timeout 0 wit inspect 900     2300 9400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.8
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 2.4   77 25    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 22     650  
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 89     480 710    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5600 true 2 wit inspect 36     820  
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 true 2 wit inspect 32     630 400    - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 7.7  400 true 2 wit inspect 34     830  
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 16     200 190    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 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--frontends--dvb_dummy_fe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .71  57 9.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 36     1400  
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 .55  48 6.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 true 2 wit inspect 19     600  
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 7.5   230 81    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 out of memory 0 wit inspect 570     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 2.6   110 35    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 26     760  
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 .58  43 6.4  - 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--media--dvb--frontends--tda18271c2dd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 7.3   190 82    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 51     2300  
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 .41  41 4.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    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--media--dvb--frontends--tua6100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .57  43 7.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 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--media--dvb--ttpci--budget-patch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .59  81 6.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 23     530  
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 5.1   220 53    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 34     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 .13  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 5.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-alink-dtu-m.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 8.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-anysee.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    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-apac-viewcomp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .093 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    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-asus-pc39.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .14  27 .97 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 9.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-ati-tv-wonder-hd-600.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .092 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    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-ati-x10.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .094 27 .92 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 9.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-avermedia-a16d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .094 27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    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-avermedia-cardbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .93 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 11     320  
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 .094 27 1.0  - 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-avermedia-m135a.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  28 .99 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 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--media--rc--keymaps--rc-avermedia-m733a-rm-k6.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .099 27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.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-avermedia-rm-ks.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    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-avermedia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .98 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    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-avertv-303.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    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-azurewave-ad-tu700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 .97 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 10     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 .12  27 .94 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 7.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-behold.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .92 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    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-budget-ci-old.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 9.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-cinergy-1400.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    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-cinergy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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--media--rc--keymaps--rc-dib0700-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .096 27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 510    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--media--rc--keymaps--rc-dib0700-rc5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  28 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 15     510  
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 .096 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    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-digittrade.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .91 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    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-dm1105-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .10  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    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-dntv-live-dvb-t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .83 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 7.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-dntv-live-dvbt-pro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .095 27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 9.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-em-terratec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    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-encore-enltv-fm53.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .14  27 .84 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    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-encore-enltv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .095 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    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-encore-enltv2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .099 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.1   310  
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 .096 27 .99 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 6.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-eztv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .89 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    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-flydvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .097 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 6.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-flyvideo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .80 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 4.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-fusionhdtv-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .097 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 7.7   330  
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 .093 27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    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-genius-tvgo-a11mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .096 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 7.7   290  
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 .13  27 .89 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    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-hauppauge.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .10  28 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 11     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 .097 28 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 620    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-imon-pad.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .096 27 1.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 9.6   360  
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 .11  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    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-it913x-v1.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .094 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 5.6   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-v2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 .99 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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-kaiomy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .96 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    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-315u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .098 27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    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 .095 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 9.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-kworld-plus-tv-analog.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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-leadtek-y04g0051.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 true 2 wit inspect 8.1   310  
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 .10  27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 error (7) 0 wit inspect 9.2   200  
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 .12  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 true 2 wit inspect 11     320  
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 .097 27 .99 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 7.6   310  
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 .10  27 1.1  - 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-msi-digivox-ii.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .097 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 6.7   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 .097 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    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-msi-tvanywhere-plus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 .97 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 9.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.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    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--media--rc--keymaps--rc-nebula.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .097 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    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-nec-terratec-cinergy-xs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 11     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 .098 27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    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-npgtech.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .093 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    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-pctv-sedna.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .095 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 9.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-color.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .092 27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    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-pinnacle-grey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .096 27 .92 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    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 .093 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    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-pixelview-002t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 8.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-pixelview-mk12.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .099 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    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-pixelview-new.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    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--media--rc--keymaps--rc-pixelview.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .095 27 .97 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    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-powercolor-real-angel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .098 27 .97 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 7.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-proteus-2309.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .095 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    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-purpletv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .097 27 .91 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 7.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-pv951.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .091 27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    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-rc6-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .099 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    7000 true 2 wit inspect 10     310  
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 .096 27 .96 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 7.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-snapstream-firefly.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 7.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-streamzap.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .10  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 7.7   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 .11  27 .94 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    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-technisat-usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 .90 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    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-terratec-cinergy-xs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .095 27 .92 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 9.1   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 .12  27 .77 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 6.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-terratec-slim.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 .98 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    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-tevii-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .092 27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 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--media--rc--keymaps--rc-tivo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .093 27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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-total-media-in-hand.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .93 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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-trekstor.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .10  27 1.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    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-tt-1500.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .095 27 .98 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 5.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-twinhan1027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 true 2 wit inspect 8.6   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 .14  27 .89 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    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 .091 27 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    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-videomate-tv-pvr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .092 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    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-winfast-usbii-deluxe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .099 27 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 290    7000 true 2 wit inspect 6.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-winfast.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  27 .97 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 9.8   320  
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 unknown 0 wit inspect .34  72 3.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.9
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 unknown 0 wit inspect .57  120 5.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .025 4.8
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 .39  46 4.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 error (7) 0 wit inspect 8.7   210  
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 timeout 0 wit inspect 900     2800 9500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 4.9
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 timeout 0 wit inspect 900     2800 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8
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 .71  64 9.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 16     640  
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 timeout 0 wit inspect 900     2400 8900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.8
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 timeout 0 wit inspect 900     2400 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.9
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 4.1   75 45    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 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--message--i2o--i2o_bus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unknown 0 wit inspect .11  32 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
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 unknown 0 wit inspect .27  53 2.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 5.0
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 .37  43 4.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 16     410  
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 .16  31 1.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 9.8   320  
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 timeout 0 wit inspect 900     5500 8500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.9
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 2 wit inspect .22  34 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    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--mfd--tps65217.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .34  39 4.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 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--mfd--ucb1400_core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .22  38 2.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 760    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--mfd--wl1273-core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .39  42 5.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    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--mfd--wm8400-core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .55  50 6.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 18     610  
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 timeout 0 wit inspect 900     4000 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8
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 .38  43 4.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 13     450  
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 timeout 0 wit inspect 900     2000 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .022 4.8
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 .35  47 4.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 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--isl29020.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .20  35 2.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 8.5   370  
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 unknown 0 wit inspect .11  28 .70 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .019 4.9
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 .15  33 1.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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--misc--tifm_core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .58  57 6.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    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--mmc--host--sdricoh_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.0   99 33    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 18     490  
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 .54  51 6.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 8.1   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 .17  31 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    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--mtd--ftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 21     260 240    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 26     600  
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 97     580 690    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5500 true 2 wit inspect 31     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 1.0   60 15    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 true 2 wit inspect 10     400  
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 .14  30 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    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--mtd--nftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 99     550 760    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5900 true 2 wit inspect 31     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 .28  41 2.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 true 2 wit inspect 7.4   450  
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 .24  47 2.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    1500 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--mtd--tests--mtd_pagetest.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .19  43 2.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    630 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--mtd--ubi--gluebi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c out of memory 0 wit inspect 780     15000 7600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .024 5.0
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 .84  65 9.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 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--net--irda--act200l-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .24  40 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 8.8   370  
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 .20  39 2.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6600 true 2 wit inspect 7.7   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 2 wit inspect .21  40 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.7   370  
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 2 wit inspect .25  40 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 9.3   360  
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 .18  35 1.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 true 2 wit inspect 8.2   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 9.9   200 110    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 19     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 .20  38 1.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    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--net--phy--davicom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  39 3.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 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--net--phy--et1011c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .18  38 2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 9.7   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 .19  41 2.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    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--net--phy--lxt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .25  40 2.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 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--net--phy--marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .29  51 3.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 true 2 wit inspect 22     690  
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 .32  41 4.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 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--net--phy--national.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .24  39 2.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 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--net--phy--qsemi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .20  38 2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 true 2 wit inspect 9.0   350  
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 .16  34 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 7.4   330  
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 .39  44 4.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 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--net--phy--spi_ks8995.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     9400 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8
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 .28  39 2.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 9.1   360  
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 .17  36 1.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    7000 true 2 wit inspect 8.6   340  
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 7.4   140 98    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    3800 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--net--ppp--ppp_mppe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 9.7   150 110    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 error (7) 0 wit inspect 7.0   260  
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 22     190 200    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    7000 true 2 wit inspect 21     640  
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 .20  39 2.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    7000 true 2 wit inspect 8.4   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 4.0   150 50    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 9.0   380  
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 .35  43 4.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 12     460  
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 2 wit inspect .71  58 7.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 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--net--wireless--mwifiex--mwifiex_pcie.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unknown 0 wit inspect .57  120 5.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.8
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 2 wit inspect .39  48 3.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    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--wireless--orinoco--orinoco_pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .31  42 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 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--net--wireless--orinoco--orinoco_tmd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .39  42 4.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    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--net--wireless--wl1251--wl1251_spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .85  57 12    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 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--net--wireless--wl12xx--wl12xx_sdio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .92  66 10    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    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--parport--parport_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .44  43 5.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 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--pci--ioapic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  35 2.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 520    7000 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--pci--pci-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .13  31 1.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    1500 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--platform--x86--asus-nb-wmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .15  35 1.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 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--platform--x86--intel_menlow.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.5   56 18    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 26     750  
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 1.0   62 11    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 true 2 wit inspect 19     610  
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 .27  36 3.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    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 .20  35 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 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--platform--x86--xo15-ebook.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .30  36 3.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 13     430  
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 1.1   66 13    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3800 true 2 wit inspect 13     460  
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 .77  46 9.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 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--power--wm831x_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .89  58 9.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 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--regulator--gpio-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.4   90 30    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6600 true 2 wit inspect 12     460  
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 2 wit inspect 1.2   61 14    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 13     430  
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 1.3   63 20    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 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--regulator--userspace-consumer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .27  32 2.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 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--regulator--virtual.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .45  43 5.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    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--regulator--wm831x-dcdc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 11     370 130    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 24     660  
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 2 wit inspect 1.6   63 18    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 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--regulator--wm831x-ldo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.7   270 80    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 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 .94  51 14    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 16     430  
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 .57  44 6.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 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--rtc--rtc-ds1390.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .91  52 13    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 true 2 wit inspect 8.9   380  
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 .93  64 11    - 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--rtc--rtc-ds3232.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     5000 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 5.0
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 .38  38 4.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 9.1   370  
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 .65  56 8.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 true 2 wit inspect 12     460  
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 .56  47 7.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 12     430  
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 2.0   42 22    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 6.8   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 .36  38 4.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 true 2 wit inspect 9.4   370  
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 .56  48 6.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    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--rtc--rtc-pcap.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .20  36 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 620    7000 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--rtc--rtc-pcf2123.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .78  73 8.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    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--rtc--rtc-r9701.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .78  55 11    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6900 true 2 wit inspect 10     400  
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 .59  48 7.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 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--rtc--rtc-stk17ta8.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.1   67 14    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    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 .37  37 4.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 9.0   350  
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 2.4   73 28    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 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--rtc--rtc-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .94  51 12    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 true 2 wit inspect 11     420  
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 1.9   130 22    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5600 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--scsi--iscsi_boot_sysfs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.3   67 21    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 17     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 5.7   160 78    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 23     640  
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 2.7   92 33    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5800 true 2 wit inspect 17     490  
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 .43  44 4.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 16     410  
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 .27  32 3.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 true 2 wit inspect 8.4   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 .52  49 6.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    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 2 wit inspect 1.4   100 19    - 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--staging--iio--addac--adt7316-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .21  34 2.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 true 2 wit inspect 6.8   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 .21  35 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 290    7000 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--staging--iio--dds--ad9832.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .69  69 8.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 17     490  
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 .19  34 2.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 260    7000 true 2 wit inspect 9.4   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 timeout 0 wit inspect 900     9100 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .019 4.8
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 timeout 0 wit inspect 900     9100 9100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .022 4.8
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 timeout 0 wit inspect 900     9400 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.9
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 .24  35 2.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 270    7000 true 2 wit inspect 11     350  
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 .25  42 2.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 13     430  
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 .18  38 1.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 890    7000 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--staging--speakup--speakup_bns.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .15  37 1.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 true 2 wit inspect 11     370  
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 .17  37 1.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 12     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 .19  47 2.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 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--staging--speakup--speakup_soft.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .65  79 7.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 true 2 wit inspect 16     570  
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 .18  41 1.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 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--speakup--speakup_txprt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .14  38 1.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 14     380  
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 .60  54 6.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    7000 true 2 wit inspect 13     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 .18  33 2.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 8.5   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 .67  75 6.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    480 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--target--loopback--tcm_loop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.2   110 13    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 true 2 wit inspect 29     650  
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 .62  62 7.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 true 2 wit inspect 8.4   490  
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 1.2   87 16    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 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--tty--serial--mfd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.9   260 130    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 23     600  
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 1.4   87 16    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 900    7000 true 2 wit inspect 18     620  
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 3.4   120 39    - 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 .38  41 4.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 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 .26  34 3.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    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 2 wit inspect .88  55 12    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 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--usb--atm--xusbatm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .27  55 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  300 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--usb--misc--cypress_cy7c63.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .33  41 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 510    7000 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--usb--misc--cytherm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .36  50 4.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 9.2   350  
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 .98  65 14    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 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--usb--otg--nop-usb-xceiv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .23  33 2.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    7000 true 2 wit inspect 8.0   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 2 wit inspect .53  83 5.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 200     6800  
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 .61  64 8.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6600 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--serial--iuu_phoenix.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.9   170 82    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 31     610  
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 1.6   86 17    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 true 2 wit inspect 16     620  
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 3.1   120 32    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 17     490  
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 .55  96 4.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 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--usb--storage--ums-cypress.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .23  44 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    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--usb--storage--ums-datafab.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .34  58 3.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    7000 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--usb--storage--ums-freecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .27  44 2.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    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--usb--storage--ums-jumpshot.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .33  55 3.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 530    7000 true 2 wit inspect 8.0   350  
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 .51  83 4.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 21     1000  
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 .36  64 3.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 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--usb--storage--ums-usbat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .43  73 4.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 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--uwb--i1480--i1480-est.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .15  33 1.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 610    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--video--backlight--ili9320.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .49  45 4.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 true 2 wit inspect 12     460  
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 3.3   94 40    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 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--video--backlight--lms283gf05.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .90  53 11    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 16     450  
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 2.3   110 31    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 11     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 2 wit inspect .24  39 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 9.6   360  
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 .18  37 1.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  340 true 2 wit inspect 7.6   330  
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 timeout 0 wit inspect 900     2600 9200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .022 4.9
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 .32  36 3.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    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--w1--masters--w1-gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .24  33 1.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 8.2   330  
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 timeout 0 wit inspect 900     2300 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 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--w1--slaves--w1_ds2408.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .22  39 2.3  - 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--w1--slaves--w1_ds2423.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .11  31 1.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 6.5   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 timeout 0 wit inspect 900     3800 8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 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--w1--slaves--w1_ds2433.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     3100 7200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9
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 timeout 0 wit inspect 900     3800 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.9
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 timeout 0 wit inspect 900     3500 9000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8
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 timeout 0 wit inspect 900     3500 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.8
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 .12  29 .86 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 7.3   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 2 wit inspect .28  34 2.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 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--watchdog--wm831x_wdt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     3900 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .017 4.8
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 .21  39 2.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 6.4   320  
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 .63  46 6.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 15     400  
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 .27  34 3.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5300 true 2 wit inspect 7.7   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 .24  37 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 7.7   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 .21  38 2.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 290    7000 true 2 wit inspect 9.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--adxl34x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .31  37 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 true 2 wit inspect 9.9   350  
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 .24  38 3.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    7000 true 2 wit inspect 7.7   350  
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 .46  47 5.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 13     410  
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 .28  34 3.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    7000 true 2 wit inspect 8.6   320  
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 .26  36 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 7.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--pcspkr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .25  36 2.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.3   320  
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 .60  48 7.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 9.9   390  
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 .47  39 5.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 9.2   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 2 wit inspect .40  43 4.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 true 2 wit inspect 10     400  
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 2 wit inspect .37  40 4.9  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 8.3   370  
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 .52  50 6.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6200 true 2 wit inspect 10     430  
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 2 wit inspect .32  37 4.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6600 true 2 wit inspect 9.2   360  
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 2 wit inspect .44  43 5.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 730    7000 true 2 wit inspect 9.5   340  
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 timeout 0 wit inspect 900     6300 8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 5.0
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 5.9   150 73    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 true 2 wit inspect 22     510  
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 .63  74 8.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 11     460  
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 .30  54 3.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 8.0   320  
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 2 wit inspect .64  96 6.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4500 true 2 wit inspect 11     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 .97  180 8.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 6.7   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 timeout 0 wit inspect 900     1400 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 4.9
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 .16  36 1.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 5.8   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 .14  36 1.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    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--lnbp21.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .15  37 1.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 7.2   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--lnbp22.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .16  37 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 6.2   260  
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 .23  43 2.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 8.7   390  
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 .34  32 3.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 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--mtd--devices--doc2001plus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .30  53 3.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 true 2 wit inspect 8.4   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 2 wit inspect .22  39 2.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 9.1   330  
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 2 wit inspect .23  40 2.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 7.9   370  
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 2 wit inspect .24  40 2.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    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--net--irda--old_belkin-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .19  39 2.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 7.5   340  
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 .24  40 2.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    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 .22  39 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    7000 true 2 wit inspect 7.3   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 .13  33 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 7.1   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 .28  33 3.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 true 2 wit inspect 10     340  
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 .077 27 .78 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 4.8   240  
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 .18  34 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 620    7000 true 2 wit inspect 7.2   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 .32  45 3.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 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--staging--comedi--drivers--unioxx5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .46  47 5.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    5700 true 2 wit inspect 12     370  
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 .43  39 5.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    7000 true 2 wit inspect 8.0   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 .11  32 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 510    7000 true 2 wit inspect 6.6   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 .29  42 3.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 9.7   420  
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 .19  41 2.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    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--staging--media--cxd2099--cxd2099.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     1200 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.8
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 timeout 0 wit inspect 900     11000 7000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .018 4.8
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 .35  64 3.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5500 true 2 wit inspect 5.7   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 .24  35 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 8.3   330  
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 2 wit inspect .25  37 3.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 9.6   330  
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 timeout 0 wit inspect 900     14000 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .024 4.8
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 .23  39 2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 true 2 wit inspect 12     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 .17  36 1.8  - wit inspect - wit