Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 14     4800 160    false(unreach-call) 1 wit inspect 25    630 error (7) 0 wit inspect 4.4   440   timeout 0 wit inspect 4.5  280 error (2) 0 wit inspect 6.6    82    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .40  120 5.2  error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0022 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .69  210 7.3  error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 52 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 8.8   660 94    timeout 0 wit inspect 91    1200 true -32 wit inspect 32     800   unknown 0 wit inspect 8.4  330 error (2) 0 wit inspect 2.7    33    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 1 wit inspect 8.6   700 110    false(unreach-call) 1 wit inspect 78    840 unknown 0 wit inspect 5.8   300   unknown 0 wit inspect 6.0  320 error (2) 0 wit inspect 2.7    35    - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i out of memory 0 wit inspect 69     15000 880    error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     5900 7600    error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 2.2   780 27    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 5.2   1300 64    error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .73 51 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 3.7   130 42    error (invalid witness file) 0 wit inspect 3.9  200 true -32 wit inspect 11     400   error (invalid witness file) 0 wit inspect 4.0  220 error (1) 0 wit inspect .92   19    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 6.3   160 73    timeout 0 wit inspect 92    2300 true -32 wit inspect 15     480   unknown 0 wit inspect 7.6  410 error (2) 0 wit inspect 1.1    20    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .75  320 9.6  error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 1.5   130 14    timeout 0 wit inspect 92    1600 true -32 wit inspect 17     500   unknown 0 wit inspect 3.8  270 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 3.9   200 50    timeout 0 wit inspect 91    1100 true -32 wit inspect 19     500   unknown 0 wit inspect 4.0  270 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .44  97 4.9  error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 9.2   260 110    error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 3.4   360 47    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 50     7800 520    - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 41    1100 true 2 wit inspect 97     2700  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 17     430 230    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 true 2 wit inspect 42     1900  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     12000 6900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.9
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     13000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .023 5.0
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i true 1 wit inspect 23     6300 310    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6500 timeout 0 wit inspect 960     5300  
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     2100 7100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .022 4.8
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 2.0   190 23    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 56     2800  
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 2.5   440 26    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    5800 true 2 wit inspect 45     830  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect .24  40 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 740    7000 true 2 wit inspect 15     510  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 79     4200 760    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 30     600  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 370     13000 3800    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 44     860  
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 19     1300 210    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 32     1400  
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 18     460 250    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960    5700 true 2 wit inspect 32     810  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i false(unreach-call) -16 wit inspect 3.8   120 40    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4  210 true 2 wit inspect 12     380  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 28     730 280    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .022 5.0
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 21     1600 260    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6000 true 2 wit inspect 19     820  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 21     150 180    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2600 true 2 wit inspect 19     620  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i out of memory 0 wit inspect 330     15000 4700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.8
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i out of memory 0 wit inspect 98     15000 940    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .024 4.9
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i timeout 0 wit inspect 900     7100 9500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 2.6   280 34    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect .33  77 3.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 4.9
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i unknown 0 wit inspect 12     420 110    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 5.0
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i true 2 wit inspect 17     390 180    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6000 true 2 wit inspect 37     1200  
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c out of memory 0 wit inspect 120     15000 1400    error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb_false-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 42     400 470    timeout 0 wit inspect 92    2500 true -32 wit inspect 14     490   unknown 0 wit inspect 5.3  410 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     11000 12000    error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--isdn--capi--kernelcapi.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 1 wit inspect 1.4   170 13    false(unreach-call) 1 wit inspect 19    610 unknown 0 wit inspect 5.3   310   unknown 0 wit inspect 4.9  330 error (2) 0 wit inspect 2.9    30    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unknown 0 wit inspect 1.5   390 18    error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unknown 0 wit inspect .47  160 5.3  error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .044 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--mem2mem_testdev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unknown 0 wit inspect .17  50 1.5  error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--vivi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unknown 0 wit inspect .19  67 2.0  error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--mtd--chips--cfi_cmdset_0001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c unknown 0 wit inspect .72  150 6.2  error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 1 wit inspect 8.6   460 110    false(unreach-call) 1 wit inspect 12    480 true -32 wit inspect 18     590   unknown 0 wit inspect 6.5  280 error (2) 0 wit inspect 1.7    25    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 1 wit inspect 1.2   110 11    false(unreach-call) 1 wit inspect 7.2  390 true -32 wit inspect 13     590   unknown 0 wit inspect 4.8  290 error (2) 0 wit inspect 1.8    26    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     1800 11000    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0031 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 1.7   220 17    timeout 0 wit inspect 92    1300 timeout 0 wit inspect 97     4600   unknown 0 wit inspect 8.9  360 error (2) 0 wit inspect 3.3    39    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 1 wit inspect .51  66 6.0  false(unreach-call) 1 wit inspect 8.2  290 true -32 wit inspect 9.7   470   unknown 0 wit inspect 3.5  270 error (2) 0 wit inspect 1.3    21    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--storage--usb-storage.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 1.4   210 12    timeout 0 wit inspect 94    2700 true -32 wit inspect 43     1300   unknown 0 wit inspect 8.3  330 error (2) 0 wit inspect 3.0    35    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--vhost--vhost_net.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 13     610 160    timeout 0 wit inspect 92    1900 true -32 wit inspect 33     920   unknown 0 wit inspect 7.0  430 error (2) 0 wit inspect 3.0    35    - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     3100 9300    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c unknown 0 wit inspect .43  120 4.0  error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.c unknown 0 wit inspect .37  110 4.5  error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c unknown 0 wit inspect .62  180 8.3  error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c unknown 0 wit inspect .74  200 7.1  error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0010 .27 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c unknown 0 wit inspect 1.5   300 15    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c unknown 0 wit inspect .57  160 5.2  error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c unknown 0 wit inspect 1.3   250 10    error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--misc--sgi-xp--xpc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     1500 10000    error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--net--wireless--orinoco--orinoco_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c timeout 0 wit inspect 900     3700 11000    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c out of memory 0 wit inspect 760     15000 5500    error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true -32 wit inspect 20     450 260    timeout 0 wit inspect 92    3000 timeout 0 wit inspect 96     2600   unknown 0 wit inspect .68 51 error (1) 0 wit inspect .094  9.1  - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c out of memory 0 wit inspect 73     15000 770    error (invalid witness file) 0 wit inspect .42 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--pch_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true -32 wit inspect 44     1800 490    timeout 0 wit inspect 95    2100 timeout 0 wit inspect 98     1300   unknown 0 wit inspect .72 51 error (1) 0 wit inspect .094  9.4  - wit inspect - wit inspect
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  38 3.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 650    7000 true 2 wit inspect 14     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .26  34 2.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6700 true 2 wit inspect 9.4   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .29  37 3.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 460    7000 true 2 wit inspect 13     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .48  48 5.7  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6600 true 2 wit inspect 9.7   450  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_netcell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .25  40 2.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 890    7000 true 2 wit inspect 11     410  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  33 3.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 12     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864bfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .23  37 2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 true 2 wit inspect 6.7   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .18  31 1.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6700 true 2 wit inspect 6.2   280  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--aten.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.2   72 16    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6500 true 2 wit inspect 13     480  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 170     1000 1100    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 870    7000 true 2 wit inspect 18     630  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--comm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 3.8   140 39    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 930    6900 true 2 wit inspect 18     510  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.3   140 56    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 490    7000 true 2 wit inspect 24     570  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 41     410 300    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 790    7000 true 2 wit inspect 25     580  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 17     310 150    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6600 true 2 wit inspect 17     520  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .76  55 9.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 620    7000 true 2 wit inspect 13     460  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 2.2   100 23    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 true 2 wit inspect 11     500  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--friq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 17     280 120    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 700    7000 true 2 wit inspect 25     610  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--frpw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 14     280 110    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    7000 true 2 wit inspect 24     610  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--kbic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 17     340 170    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6800 true 2 wit inspect 18     620  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--ktti.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .78  58 8.7  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 13     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 4.0   140 44    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 750    7000 true 2 wit inspect 28     590  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 68     620 460    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 900    7000 true 2 wit inspect 32     880  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--hw_random--virtio-rng.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .47  33 5.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 true 2 wit inspect 11     330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .47  51 5.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6000 true 2 wit inspect 33     750  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ramoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .23  35 2.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 600    7000 true 2 wit inspect 5.2   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--uv_mmtimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .93  73 10    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 12     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .21  31 2.1  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 7.4   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--cpufreq_powersave.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .096 28 1.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 420    7000 true 2 wit inspect 9.0   300  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .68  71 7.8  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 720    7000 true 2 wit inspect 15     470  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .28  36 3.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    7000 true 2 wit inspect 10     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .22  34 2.2  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5700 true 2 wit inspect 10     350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .27  35 3.8  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4800 true 2 wit inspect 12     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-tps65912.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .26  32 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 430    7000 true 2 wit inspect 10     330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .48  39 5.9  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 13     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.0   65 15    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 true 2 wit inspect 14     490  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .17  38 2.2  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 590    7000 true 2 wit inspect 11     390  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--stub--poulsbo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .15  34 2.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 9.9   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-cherry.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .24  33 2.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 300    7000 true 2 wit inspect 7.8   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-chicony.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.8   120 18    - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 8.8   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .16  32 1.3  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380    7000 true 2 wit inspect 8.1   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .21  33 2.1  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450    7000 true 2 wit inspect 9.1   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect 1.2   84 16    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6900 true 2 wit inspect 10     360  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .16  32 1.6  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 310    7000 true 2 wit inspect 9.4   320  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-keytouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .12  32 1.4  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 350    7000 true 2 wit inspect 9.3   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-lcpower.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .53  50 6.6  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6500 true 2 wit inspect 7.6   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-monterey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .26  35 3.0  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 390    7000 true 2 wit inspect 13     330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ortek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .14  32 1.5  - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 8.3   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-petalynx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .68  48 6.8  - wit inspect - wit inspect - wit