<
Tool ULTIMATE Taipan 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]
Date of execution 2017-12-02 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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 7.7 480 57 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0012 .26 - 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   5300 11000 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0041 .34 - 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   6100 8300 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0021 .30 - 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 7200 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0035 .31 - 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.4 350 41 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .81 50 error (invalid witness file) 0 wit inspect .0040 .34 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 160   1400 1300 timeout 0 wit inspect 92    1400 timeout 0 wit inspect 96     990   unknown 0 wit inspect 7.0  290 error (2) 0 wit inspect 1.8    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   4900 9100 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 51 error (invalid witness file) 0 wit inspect .0041 .26 - 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 170   3200 1800 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .039 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0037 .34 - 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   6200 12000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0036 .31 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 32   720 300 error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0035 .31 - 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   5500 12000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0044 .30 - 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   5000 11000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .050 4.8 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0040 .34 - 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 error (7) 0 wit inspect 78   1900 590 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 610   6200 6200 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0016 .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   5500 11000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 280   4900 2600 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .031 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .29 - 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   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 45   4700 390 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 45    1100 true 2 wit inspect 100     2600  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 92   5200 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 true 2 wit inspect 41     1600  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 21   660 160 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    7000 true 2 wit inspect 16     500  
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .025 4.9
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   6100 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .024 4.9
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 15   610 120 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 13     460  
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 840   5300 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 48     3100  
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 29   1000 240 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5800 true 2 wit inspect 37     810  
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 14   570 110 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 830    7000 true 2 wit inspect 14     530  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 31   1900 230 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5900 true 2 wit inspect 25     620  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 47   4200 490 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 36     880  
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 32   1700 270 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    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 60   3700 610 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5700 true 2 wit inspect 29     790  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 300   4900 3200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5500 true 2 wit inspect 52     1300  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 27   1200 220 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5800 true 2 wit inspect 19     540  
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 37   3000 340 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 21     810  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 23   1400 190 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 21     610  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 23   1200 180 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 8.6  270 true 2 wit inspect 24     550  
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 10   290 85 - 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.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 110   3700 960 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 5.0
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 63   2400 490 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5900 true 2 wit inspect 45     1400  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i error (7) 0 wit inspect 77   1100 770 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.9
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 47   4300 470 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6000 true 2 wit inspect 38     990  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
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   7300 9600 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0042 .29 - 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 timeout 0 wit inspect 900   6400 11000 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .046 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0041 .32 - 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   4900 8300 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0041 .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 unknown 0 wit inspect 5.7 350 49 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0034 .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 timeout 0 wit inspect 900   6300 9900 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0036 .26 - 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   6700 11000 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0039 .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 95 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .033 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0038 .28 - 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   5400 11000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0037 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--mtd--chips--cfi_cmdset_0001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 26   850 190 timeout 0 wit inspect 92    1800 timeout 0 wit inspect 96     1000   unknown 0 wit inspect 7.9  320 error (2) 0 wit inspect 2.4    31    - 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   4900 7900 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .043 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0036 .28 - 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) 0 wit inspect 38   1200 290 timeout 0 wit inspect 97    2500 timeout 0 wit inspect 96     860   unknown 0 wit inspect 7.9  300 error (2) 0 wit inspect 1.9    28    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 160   5200 1700 timeout 0 wit inspect 93    2300 timeout 0 wit inspect 97     2900   unknown 0 wit inspect 18    660 error (2) 0 wit inspect 8.4    83    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   7600 7400 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0043 .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 false(unreach-call) 0 wit inspect 17   550 140 timeout 0 wit inspect 93    2600 unknown 0 wit inspect 27     550   unknown 0 wit inspect 5.1  270 error (2) 0 wit inspect 1.4    22    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--storage--usb-storage.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900   5500 10000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0036 .28 - 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   6900 5700 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .040 5.0 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0047 .29 - 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   6300 12000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .017 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0047 .26 - 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 12   540 89 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .049 4.8 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0011 .34 - 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 90 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .86 48 error (invalid witness file) 0 wit inspect .0039 .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 13   610 91 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0037 .33 - 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 13   650 93 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .83 48 error (invalid witness file) 0 wit inspect .0011 .31 - 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   630 92 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .026 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0041 .34 - 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 13   590 96 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect .80 51 error (invalid witness file) 0 wit inspect .0040 .30 - 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   600 94 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .79 47 error (invalid witness file) 0 wit inspect .0040 .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   5000 15000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0010 .31 - 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 false(unreach-call) 0 wit inspect 250   1400 2000 timeout 0 wit inspect 93    2800 timeout 0 wit inspect 96     820   unknown 0 wit inspect 7.8  320 error (2) 0 wit inspect 2.1    30    - 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   3800 9200 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .045 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0019 .29 - 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   5100 10000 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0042 .29 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 62   1300 650 timeout 0 wit inspect 94    3000 timeout 0 wit inspect 97     1000   unknown 0 wit inspect 9.2  360 error (2) 0 wit inspect 2.6    34    - 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 unknown 0 wit inspect 130   1800 1300 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0022 .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 21   2100 210 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    7000 true 2 wit inspect 14     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.2 480 76 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 true 2 wit inspect 7.5   340  
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 20   1700 160 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480    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 1 wit inspect 20   1400 160 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6900 unknown 0 wit inspect 56     630  
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 16   990 130 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    7000 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--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 430   5100 5800 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    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--auxdisplay--cfag12864bfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 16   800 130 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 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--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 6.1 300 48 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    7000 true 2 wit inspect 5.8   270  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--aten.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 17   570 130 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 880    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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 29   920 230 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 760    7000 true 2 wit inspect 23     710  
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 21   650 190 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6900 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--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 22   660 220 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    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--block--paride--epat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 24   720 210 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 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--block--paride--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 22   670 180 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 19     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 13   530 110 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 570    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--block--paride--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 20   570 190 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 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--friq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 26   830 240 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 660    7000 true 2 wit inspect 27     640  
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 25   780 200 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 560    7000 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--block--paride--kbic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 26   900 230 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6800 true 2 wit inspect 21     610  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--ktti.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 15   550 120 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 640    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--block--paride--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 23   690 170 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 820    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--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 35   1100 290 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 true 2 wit inspect 34     980  
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 11   510 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 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--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 80   5400 1000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 27     1000  
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 10   430 96 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 7.2   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 13   510 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 11     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 9.8 500 96 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 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--cpufreq--cpufreq_powersave.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.0 430 79 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    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--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 19   1000 140 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 670    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--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 15   490 150 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 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--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 10   510 91 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 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--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 15   490 150 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 8.4   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 9.0 470 76 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 8.1   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 13   510 120 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 18   630 150 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 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--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 16   1200 130 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    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--gpu--stub--poulsbo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 10   510 89 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 7.4   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 11   530 95 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 8.0   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 12   520 98 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 8.6   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.8 480 86 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    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-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 12   510 120 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    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-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 12   530 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    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--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 9.8 480 91 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 7.7   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-keytouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 12   890 87 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 8.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 11   500 100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 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-monterey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 10   510 98 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 7.5   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 10   510 87 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 340    7000 true 2 wit inspect 7.2   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 12   510 98 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 410    7000 true 2 wit inspect 9.3   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-primax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 11   490 110 - wit inspect -