Tool ULTIMATE Kojak 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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 error (7) 0 wit inspect 8.2 490 57 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4900 10000 error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5400 11000 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 10000 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - 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 unknown 0 wit inspect 5.8 350 44 error (invalid witness file) 0 wit inspect .73 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 10000 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0013 .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   5000 12000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5100 9900 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .94 49 error (invalid witness file) 0 wit inspect .0020 .30 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   2600 9000 error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   3600 10000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .26 - 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 timeout 0 wit inspect 900   5200 11000 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0015 .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 timeout 0 wit inspect 900   4900 9700 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0018 .30 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5200 9200 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5200 8400 error (invalid witness file) 0 wit inspect .62 45 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect 1.2  47 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5200 8900 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .97 49 error (invalid witness file) 0 wit inspect .0017 .30 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.9
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5300 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .018 5.0
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   1500 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
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   5600 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .019 5.0
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   2200 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 4.8
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5300 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 45 error (2) 0 wit inspect .019 4.9
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   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 42 error (2) 0 wit inspect .020 4.9
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   1800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.9
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 710   2100 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .021 4.9
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 12   500 100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 true 2 wit inspect 15     540  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.9
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5400 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 45 error (2) 0 wit inspect .020 4.8
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   1800 7100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .018 4.8
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5300 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.8
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5100 7600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .020 4.9
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .017 5.0
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 9.5 290 80 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 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   5000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5300 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 5.0
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4900 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .017 4.8
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5300 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .023 5.0
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   2900 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.8
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 timeout 0 wit inspect 900   3300 12000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0015 .30 - 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 error (7) 0 wit inspect 510   2300 6200 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.1  51 error (invalid witness file) 0 wit inspect .0016 .29 - 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   5300 8200 error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0018 .28 - 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 unknown 0 wit inspect 6.6 360 49 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0016 .26 - 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 timeout 0 wit inspect 900   4700 11000 error (invalid witness file) 0 wit inspect .64 46 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   2100 10000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0016 .28 - 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 error (7) 0 wit inspect 11   320 85 error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .96 47 error (invalid witness file) 0 wit inspect .0018 .27 - 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 timeout 0 wit inspect 900   1700 8600 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--mtd--chips--cfi_cmdset_0001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   1000 10000 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.2  49 error (invalid witness file) 0 wit inspect .0015 .34 - 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 timeout 0 wit inspect 900   4800 9900 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0016 .29 - 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 timeout 0 wit inspect 900   4900 10000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .83 48 error (invalid witness file) 0 wit inspect .0015 .29 - 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   3700 9000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   4800 9400 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .035 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0020 .26 - 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 error (7) 0 wit inspect 380   900 4600 error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .28 - 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 timeout 0 wit inspect 900   2400 11000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .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 timeout 0 wit inspect 900   1800 11000 error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0016 .27 - 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   2100 11000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c error (7) 0 wit inspect 13   530 96 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0015 .29 - 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 error (7) 0 wit inspect 11   490 84 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c error (7) 0 wit inspect 12   630 97 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect 1.1  48 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c error (7) 0 wit inspect 14   650 110 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .72 49 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c error (7) 0 wit inspect 13   640 100 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.2  49 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c error (7) 0 wit inspect 12   590 95 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .98 49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c error (7) 0 wit inspect 12   590 99 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0014 .30 - 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   1600 11000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .71 49 error (invalid witness file) 0 wit inspect .0016 .29 - 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   4800 11000 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0017 .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 timeout 0 wit inspect 900   1800 12000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0020 .30 - 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 timeout 0 wit inspect 900   3600 10000 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   3800 13000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0013 .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 timeout 0 wit inspect 900   4900 10000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.2  47 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 440   1300 2900 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 15     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 18   790 150 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 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--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 400   1600 2900 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 14     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 1 wit inspect 310   1300 3300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6700 unknown 0 wit inspect 66     670  
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 220   860 2400 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    7000 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--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 54   620 620 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 12     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864bfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 180   900 2200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 true 2 wit inspect 11     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 7.1 350 65 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 820    7000 true 2 wit inspect 7.0   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--aten.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 47   850 440 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 true 2 wit inspect 16     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 160   2200 1800 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 780    7000 true 2 wit inspect 43     760  
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 93   1200 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 true 2 wit inspect 19     530  
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 89   1600 910 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 470    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--block--paride--epat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 140   4500 1700 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 25     590  
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 130   1200 1400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6600 true 2 wit inspect 21     540  
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 45   790 540 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    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--block--paride--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 74   990 750 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 840    7000 true 2 wit inspect 23     510  
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 140   1400 1400 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    7000 true 2 wit inspect 32     650  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--frpw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 100   1400 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    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 210   1200 2300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 true 2 wit inspect 34     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 47   830 480 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    7000 true 2 wit inspect 16     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 84   1600 800 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 840    7000 true 2 wit inspect 26     610  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 130   3500 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 true 2 wit inspect 41     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 64   540 670 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 9.2   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   1500 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 44 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--char--ramoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 15   450 160 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    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--char--uv_mmtimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 30   600 310 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 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--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 94   510 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 8.4   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--cpufreq_powersave.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 57   490 640 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .027 4.8
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 190   550 2500 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 760    7000 true 2 wit inspect 8.9   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 93   530 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 true 2 wit inspect 9.5   360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 160   540 2100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 true 2 wit inspect 10     370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-tps65912.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 43   560 540 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.8   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 130   830 1700 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 460   920 6200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 20     520  
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 250   980 3000 - 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 92   530 1000 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440    7000 true 2 wit inspect 6.1   330  
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 58   530 640 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    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--hid--hid-chicony.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 49   620 520 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 8.2   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 43   510 500 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 65   530 930 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    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-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 78   640 860 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 8.6   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 80   520 860 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 290    7000 true 2 wit inspect 7.6   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 140   760 1400 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 6.5   350  
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 57   530 570 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6400 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--hid--hid-monterey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 60   510 650 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 280    7000 true 2 wit inspect 7.9   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ortek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 55   520 620 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 9.2   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-petalynx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 82   750 1100 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    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--hid--hid-primax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 66   640 860 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    1700 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--hid--hid-saitek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit