Tool CPAchecker 1.6.1-svn 26758M 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-11-30 11:20:26 CET 2017-12-01 07:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 21   600 190 true -32 wit inspect 13    510 error (7) 0 wit inspect 7.1   460   timeout 0 wit inspect 6.6  300 error (2) 0 wit inspect 6.9    82    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 15   660 130 timeout 0 wit inspect 93    2000 true -32 wit inspect 24     560   unknown 0 wit inspect 6.6  280 error (2) 0 wit inspect 1.5    24    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 13   510 92 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0014 .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 true -32 wit inspect 55   1400 430 timeout 0 wit inspect 93    2300 timeout 0 wit inspect 97     1200   unknown 0 wit inspect .72 51 error (1) 0 wit inspect .070  9.4  - 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) 0 wit inspect 24   760 200 true -32 wit inspect 13    400 unknown 0 wit inspect 5.2   290   unknown 0 wit inspect 9.2  330 error (2) 0 wit inspect 2.9    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 false(unreach-call) 0 wit inspect 13   490 110 timeout 0 wit inspect 91    1500 true -32 wit inspect 23     620   unknown 0 wit inspect 7.4  280 error (2) 0 wit inspect 1.9    25    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 12   480 100 timeout 0 wit inspect 92    1000 true -32 wit inspect 22     610   unknown 0 wit inspect 6.0  270 error (2) 0 wit inspect 1.6    23    - 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 910   6700 10000 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .80 50 error (invalid witness file) 0 wit inspect .0011 .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 false(unreach-call) 0 wit inspect 100   4100 890 timeout 0 wit inspect 92    1300 true -32 wit inspect 64     1600   unknown 0 wit inspect 12    460 error (2) 0 wit inspect 5.3    61    - 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 250   5600 2400 true -32 wit inspect 6.9  270 true -32 wit inspect 10     430   unknown 0 wit inspect 4.6  260 error (2) 0 wit inspect 1.0    20    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900   9700 10000 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 13   500 120 timeout 0 wit inspect 93    2300 true -32 wit inspect 22     600   unknown 0 wit inspect 6.5  290 error (2) 0 wit inspect 1.8    25    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 510   7200 4100 timeout 0 wit inspect 92    2000 true -32 wit inspect 15     490   unknown 0 wit inspect 5.6  270 error (2) 0 wit inspect 1.4    22    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 57   2700 490 true -32 wit inspect 20    550 true -32 wit inspect 16     500   unknown 0 wit inspect 5.7  280 error (2) 0 wit inspect 1.9    22    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 23   870 180 timeout 0 wit inspect 93    2400 true -32 wit inspect 15     480   unknown 0 wit inspect 3.7  270 error (2) 0 wit inspect 1.3    21    - 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   9400 7300 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 6.7 280 58 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 true 2 wit inspect 30     740  
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 10   520 120 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 34    1100 true 2 wit inspect 110     2500  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 4.7 280 48 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 42     1800  
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 6.4 290 61 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 890    7000 true 2 wit inspect 21     500  
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 5.3 290 48 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 6.6  290 true 2 wit inspect 150     6000  
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 11   850 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 timeout 0 wit inspect 910     7000  
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 5.0 280 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 16     460  
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 5.1 280 48 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 true 2 wit inspect 46     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 6.7 280 61 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5800 true 2 wit inspect 46     840  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i.pp.i true 1 wit inspect 10   440 78 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    7000 false(unreach-call) -16 wit inspect 7.2   340  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 6.5 280 60 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5900 true 2 wit inspect 30     620  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 7.7 290 79 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 42     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 6.3 280 63 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 40     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 5.8 290 58 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5700 true 2 wit inspect 31     790  
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 73   4300 620 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  270 true 2 wit inspect 11     410  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 6.3 290 53 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5800 true 2 wit inspect 25     540  
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 6.8 290 69 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 28     820  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 4.9 290 46 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 22     640  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 5.4 290 52 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 6.0  290 true 2 wit inspect 23     530  
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i true 1 wit inspect 7.3 290 73 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4300 error (7) 0 wit inspect 11     240  
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 8.4 430 66 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5700 true 2 wit inspect 69     2200  
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 9.4 440 83 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 51     1400  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i true 1 wit inspect 600   7800 6300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 error (7) 0 wit inspect 610     750  
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 7.0 290 66 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 46     1000  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 6.2 280 63 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 35     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 false(unreach-call) 0 wit inspect 20   810 190 timeout 0 wit inspect 93    2500 true -32 wit inspect 82     2300   unknown 0 wit inspect 16    550 error (2) 0 wit inspect 9.2    82    - 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 13   510 100 timeout 0 wit inspect 93    2500 true -32 wit inspect 14     500   unknown 0 wit inspect 6.2  290 error (2) 0 wit inspect 1.4    24    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 19   710 150 timeout 0 wit inspect 93    2600 true -32 wit inspect 22     590   unknown 0 wit inspect 7.2  290 error (2) 0 wit inspect 1.7    26    - 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) 0 wit inspect 8.2 350 67 true -32 wit inspect 10    360 unknown 0 wit inspect 5.4   300   unknown 0 wit inspect 7.6  330 error (2) 0 wit inspect 3.1    31    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 23   1200 220 timeout 0 wit inspect 92    2000 timeout 0 wit inspect 97     4600   unknown 0 wit inspect 10    500 error (2) 0 wit inspect 5.9    60    - 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 false(unreach-call) 0 wit inspect 12   470 140 timeout 0 wit inspect 93    2200 true -32 wit inspect 38     1000   unknown 0 wit inspect 10    450 error (2) 0 wit inspect 4.7    42    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--mem2mem_testdev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 9.0 470 79 timeout 0 wit inspect 92    1800 error (7) 0 wit inspect 10     270   unknown 0 wit inspect 6.6  280 error (2) 0 wit inspect 1.8    24    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--vivi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 14   520 130 timeout 0 wit inspect 93    2600 true -32 wit inspect 27     860   unknown 0 wit inspect 7.3  290 error (2) 0 wit inspect 2.1    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 8.1 400 72 timeout 0 wit inspect 97    3800 true -32 wit inspect 41     910   timeout 0 wit inspect 97    3800 error (2) 0 wit inspect 2.5    30    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 9.7 460 95 true -32 wit inspect 26    610 true -32 wit inspect 20     600   unknown 0 wit inspect 6.8  300 error (2) 0 wit inspect 1.9    26    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 9.6 450 85 timeout 0 wit inspect 93    2400 true -32 wit inspect 21     610   unknown 0 wit inspect 7.2  290 error (2) 0 wit inspect 2.0    27    - 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 16   500 160 timeout 0 wit inspect 93    2300 true -32 wit inspect 71     2200   timeout 0 wit inspect 97    3900 error (2) 0 wit inspect 8.7    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 false(unreach-call) 0 wit inspect 8.6 380 79 true -32 wit inspect 16    570 timeout 0 wit inspect 97     4600   unknown 0 wit inspect 5.7  330 error (2) 0 wit inspect 3.7    40    - 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 7.7 350 83 timeout 0 wit inspect 93    2600 unknown 0 wit inspect 28     550   unknown 0 wit inspect 5.6  270 error (2) 0 wit inspect 1.5    22    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--storage--usb-storage.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 9.8 430 92 timeout 0 wit inspect 93    2600 timeout 0 wit inspect 96     3200   unknown 0 wit inspect 9.1  370 error (2) 0 wit inspect 3.3    36    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--vhost--vhost_net.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 14   510 140 timeout 0 wit inspect 92    1700 true -32 wit inspect 32     920   unknown 0 wit inspect 9.6  340 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--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 34   1300 280 timeout 0 wit inspect 93    2100 true -32 wit inspect 29     1000   unknown 0 wit inspect 11    490 error (2) 0 wit inspect 3.9    52    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c false(unreach-call) 0 wit inspect 24   920 210 timeout 0 wit inspect 98    2200 error (7) 0 wit inspect 11     480   timeout 0 wit inspect 6.3  280 error (1) 0 wit inspect .91   21    - 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 19   910 160 error (invalid witness file) 0 wit inspect .58 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 .0014 .27 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c false(unreach-call) 0 wit inspect 13   1400 130 true -32 wit inspect 27    810 error (7) 0 wit inspect 12     530   timeout 0 wit inspect 6.4  270 error (1) 0 wit inspect 1.0    21    - 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 39   1800 310 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .81 47 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-net-wireless-p54-p54usb.cil.out.c unknown 0 wit inspect 29   1700 210 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .90 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-staging-media-dt3155v4l-dt3155v4l.cil.out.c false(unreach-call) 0 wit inspect 12   1200 120 true -32 wit inspect 79    1500 error (7) 0 wit inspect 11     520   timeout 0 wit inspect 6.5  270 error (1) 0 wit inspect .95   21    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c false(unreach-call) 0 wit inspect 10   1300 100 timeout 0 wit inspect 92    1700 error (7) 0 wit inspect 11     520   timeout 0 wit inspect 6.7  260 error (1) 0 wit inspect .91   21    - 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 false(unreach-call) 0 wit inspect 21   630 190 timeout 0 wit inspect 94    2700 true -32 wit inspect 41     940   unknown 0 wit inspect 9.8  360 error (2) 0 wit inspect 3.4    38    - 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 16   610 130 timeout 0 wit inspect 94    2700 true -32 wit inspect 22     630   unknown 0 wit inspect 8.1  320 error (2) 0 wit inspect 2.1    29    - 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 false(unreach-call) 0 wit inspect 200   6400 1600 timeout 0 wit inspect 92    1600 true -32 wit inspect 40     910   unknown 0 wit inspect 11    480 error (2) 0 wit inspect 3.5    46    - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 18   690 150 timeout 0 wit inspect 92    1900 true -32 wit inspect 10     510   unknown 0 wit inspect 6.7  280 error (2) 0 wit inspect 1.6    27    - 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 16   520 150 timeout 0 wit inspect 94    2900 true -32 wit inspect 37     760   unknown 0 wit inspect 9.1  340 error (2) 0 wit inspect 2.7    36    - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--pch_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 14   530 130 timeout 0 wit inspect 94    2900 true -32 wit inspect 29     720   unknown 0 wit inspect 9.7  320 error (2) 0 wit inspect 2.5    29    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.5 290 45 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 680    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--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 280 42 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 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--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 280 43 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    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--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.6 280 52 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 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--ata--pata_netcell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.6 280 53 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 860    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--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.6 280 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    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 4.8 290 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 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--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 true 2 wit inspect 8.4   290  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--aten.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.5 270 36 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 850    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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 270 44 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    7000 true 2 wit inspect 28     640  
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 270 38 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6800 true 2 wit inspect 17     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.9 280 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 550    7000 true 2 wit inspect 20     560  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 280 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 820    7000 true 2 wit inspect 25     600  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 280 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6700 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--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.4 270 36 - 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 3.8 270 34 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    7000 true 2 wit inspect 18     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--friq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 270 45 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    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 4.3 270 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    7000 true 2 wit inspect 28     600  
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 4.2 270 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6800 true 2 wit inspect 25     600  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--ktti.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.4 270 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 540    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 3.8 270 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 true 2 wit inspect 26     580  
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 5.7 280 68 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 880    7000 true 2 wit inspect 36     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 3.6 280 33 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 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--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 280 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 true 2 wit inspect 35     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 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 8.0   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--uv_mmtimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.6 280 41 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 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--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 7.9   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--cpufreq_powersave.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.3 280 27 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 7.5   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.8 280 48 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 19     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.3 280 44 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 690    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--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.3 280 34 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5900 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--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 280 37 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 9.7   380  
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 3.6 280 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 400    7000 true 2 wit inspect 9.6   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 3.7 280 33 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 true 2 wit inspect 11     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 5.7 280 49 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 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--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.4 270 35 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 500    7000 true 2 wit inspect 14     400  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--stub--poulsbo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.7 280 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 510    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-cherry.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 280 42 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 320    7000 true 2 wit inspect 7.8   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 4.3 280 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 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--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0 280 39 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 7.9   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 280 39 - 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--hid--hid-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.4 280 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    7000 true 2 wit inspect 8.9   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 280 40 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 330    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-keytouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.1 280 37 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    7000 true 2 wit inspect 9.6   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 4.1 280 39 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6800 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--hid--hid-monterey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 280 43 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 360    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--hid--hid-ortek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.2 280