Tool CBMC CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 07:35:27 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i false(unreach-call) 1 wit inspect 3.1  3.1  220   26   .016  0      false(unreach-call) 1 wit inspect 21    13    670 0    0     error (7) 0 --- inspect 74     44     960   .66 0   timeout 0 --- inspect 7.6  130    390 .0082 0     error (2) 0 --- inspect 6.3    6.4    90    9.9  .016  - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i error 0 --- inspect 880    880    1900   5300   .090  0      error (invalid witness file) 0 --- inspect .65 .41 41 0    0     error (2) 0 --- inspect .020 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .61 46 0      0     error (invalid witness file) 0 --- inspect .0021 .0029 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i false(valid-deref) 0 wit inspect 600    600    4000   5400   .016  0      timeout 0 wit inspect 97    76    2000 0    0     timeout (error (7)) 0 --- inspect 90     62     1500   .71 0   unknown 0 --- inspect 8.8  4.8  300 0      .97  error (2) 0 --- inspect 1.6    1.6    26    .31 0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i false(unreach-call) 0 wit inspect 120    120    2100   820   .016  0      true -32 wit inspect 21    11    760 0    0     timeout 0 --- inspect 97     81     4100   1.2  0   unknown 0 --- inspect 12    6.5  460 0      1.0   error (2) 0 --- inspect 2.3    2.3    33    .48 0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i error 0 --- inspect 880    880    3900   6900   .090  .0082 error (invalid witness file) 0 --- inspect .75 .46 40 0    0     error (2) 0 --- inspect .024 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .67 48 0      0     error (invalid witness file) 0 --- inspect .0021 .0023 .40 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i error 0 --- inspect 880    880    2100   6700   .11   0      error (invalid witness file) 0 --- inspect .78 .49 42 0    0     error (2) 0 --- inspect .026 .027 5.5 0    0   error (invalid witness file) 0 --- inspect .97 .62 48 0      0     error (invalid witness file) 0 --- inspect .0042 .0047 .40 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i error (42) 0 --- inspect 880    880    2100   4200   .094  0      error (invalid witness file) 0 --- inspect .72 .44 41 0    0     error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0      0     error (invalid witness file) 0 --- inspect .0026 .0033 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i error 0 --- inspect 880    880    2900   4600   .090  0      error (invalid witness file) 0 --- inspect .62 .38 40 0    0     error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0      0     error (invalid witness file) 0 --- inspect .0041 .0057 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i error 0 --- inspect 880    880    1900   11000   .094  0      error (invalid witness file) 0 --- inspect .76 .47 41 0    0     error (2) 0 --- inspect .029 .031 5.5 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0      0     error (invalid witness file) 0 --- inspect .0058 .0073 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i error 0 --- inspect 880    880    2000   4500   .086  0      error (invalid witness file) 0 --- inspect .80 .48 42 0    0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .63 47 0      0     error (invalid witness file) 0 --- inspect .0057 .0071 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i error (6) 0 --- inspect 22    22    97   320   .012  0      error (invalid witness file) 0 --- inspect .74 .46 40 0    0     error (2) 0 --- inspect .020 .022 5.8 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0      0     error (invalid witness file) 0 --- inspect .0062 .0083 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i error (134) 0 --- inspect 110    110    3000   1600   .012  0      error (invalid witness file) 0 --- inspect .76 .47 42 0    0     error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .62 47 0      0     error (invalid witness file) 0 --- inspect .0049 .0060 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i false(valid-deref) 0 wit inspect 1.2  1.2  83   14   .012  0      timeout 0 wit inspect 97    70    2400 0    0     true -32 --- inspect 28     16     790   .62 0   unknown 0 --- inspect 9.8  5.3  440 0      .86  error (2) 0 --- inspect 1.3    1.3    23    .19 0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i false(valid-deref) 0 wit inspect 2.6  2.6  210   33   .016  0      timeout 0 wit inspect 98    71    2400 0    0     error (7) 0 --- inspect 27     15     520   .71 0   unknown 0 --- inspect 7.8  4.3  290 0      1.3   error (2) 0 --- inspect 1.3    1.3    23    .97 0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    4100   6900   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 41 0   0     error (2) 0 --- inspect .027 .029 5.6 0     0  
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i false(valid-deref) 0 wit inspect 9.7  9.7  470   110   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    900    4000 0   0     error (7) 0 --- inspect 65     38     890   .70  0  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i error (42) 0 --- inspect 880    880    5300   5000   .082  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0     error (2) 0 --- inspect .022 .023 5.7 0     0  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    3300   7300   .12   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i error (42) 0 --- inspect 880    880    1700   5700   .10   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i false(valid-free) 0 wit inspect 5.9  5.9  360   50   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    840    4500 0   0     timeout 0 --- inspect 960     890     5500   .62  0  
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i false(valid-free) 0 wit inspect 2.3  2.3  180   27   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    740    6400 0   0     true 2 --- inspect 14     7.9   440   .66  0  
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i false(valid-free) 0 wit inspect .99 .98 51   12   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    18    1100 0   0     true 2 --- inspect 48     32     2200   .62  0  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i error (42) 0 --- inspect 880    880    1100   9900   4.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i out of memory 0 --- inspect 330    330    13000   4100   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    4100   4900   .090  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .025 .027 5.6 0     0  
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    3800   3900   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i false(valid-deref) 0 wit inspect .64 .63 60   8.6 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    19    700 0   0     true 2 --- inspect 16     8.6   460   .66  0  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    2400   4700   .086  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i false(valid-free) 0 wit inspect 140    140    2900   900   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960    570    5500 0   0     error (7) 0 --- inspect 55     33     1400   .71  0  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i error (42) 0 --- inspect 880    880    1200   4400   .094  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    1200   5000   .098  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .022 .024 5.6 0     0  
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    2500   4300   .094  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i false(valid-free) 0 wit inspect .69 .68 60   9.6 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 170    140    1700 0   0     true 2 --- inspect 17     9.7   560   .62  0  
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i false(valid-free) 0 wit inspect 16    16    710   180   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    900    3800 0   0     error (7) 0 --- inspect 41     24     900   .75  0  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    970   7000   .098  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0     error (2) 0 --- inspect .020 .020 5.6 0     0  
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i out of memory 0 --- inspect 100    100    14000   1000   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 42 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i error 0 --- inspect 880    880    2800   5800   .090  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0  
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.i error 0 --- inspect 880    880    4800   6000   .086  .0041 error (invalid witness file) 0 --- inspect .74 .44 40 0    0     error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .61 47 0      0     error (invalid witness file) 0 --- inspect .0048 .0055 .40 0    0      - --- inspect - --- 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.i out of memory 0 --- inspect 510    510    13000   6200   .020  0      error (invalid witness file) 0 --- inspect .60 .36 41 0    0     error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0      0     error (invalid witness file) 0 --- inspect .0048 .0060 .53 0    0      - --- inspect - --- 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.i out of memory 0 --- inspect 48    48    13000   590   .016  0      error (invalid witness file) 0 --- inspect .76 .47 41 0    0     error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .62 47 0      0     error (invalid witness file) 0 --- inspect .0030 .0039 .52 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    1700   5300   .090  0      error (invalid witness file) 0 --- inspect .76 .47 41 0    0     error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0      0     error (invalid witness file) 0 --- inspect .0065 .0085 .52 0    0      - --- inspect - --- 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.i out of memory 0 --- inspect 85    85    13000   1100   .016  0      error (invalid witness file) 0 --- inspect .66 .41 40 0    0     error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0      0     error (invalid witness file) 0 --- inspect .0018 .0024 .53 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    2100   4400   .090  0      error (invalid witness file) 0 --- inspect .64 .39 40 0    0     error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .62 47 0      0     error (invalid witness file) 0 --- inspect .0056 .0073 .53 0    0      - --- inspect - --- 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.i out of memory 0 --- inspect 65    65    13000   790   .016  0      error (invalid witness file) 0 --- inspect .69 .42 41 0    0     error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .63 47 0      0     error (invalid witness file) 0 --- inspect .0055 .0072 .54 0    0      - --- inspect - --- 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.i out of memory 0 --- inspect 68    68    14000   860   .016  0      error (invalid witness file) 0 --- inspect .61 .37 40 0    0     error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .64 47 0      0     error (invalid witness file) 0 --- inspect .0020 .0024 .52 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    740   8300   .090  .0041 error (invalid witness file) 0 --- inspect .69 .44 40 0    0     error (2) 0 --- inspect .025 .026 5.5 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0      0     error (invalid witness file) 0 --- inspect .0043 .0064 .53 0    0      - --- inspect - --- 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.i out of memory 0 --- inspect 51    51    13000   580   .016  0      error (invalid witness file) 0 --- inspect .69 .42 40 0    0     error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 48 0      0     error (invalid witness file) 0 --- inspect .0022 .0038 .42 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    4300   4800   .090  0      error (invalid witness file) 0 --- inspect .73 .44 41 0    0     error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .63 48 0      0     error (invalid witness file) 0 --- inspect .0019 .0037 .54 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    8300   7200   .086  0      error (invalid witness file) 0 --- inspect .61 .37 40 0    0     error (2) 0 --- inspect .020 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 48 0      0     error (invalid witness file) 0 --- inspect .0060 .0078 .54 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    2600   5600   .090  0      error (invalid witness file) 0 --- inspect .74 .46 41 0    0     error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0      0     error (invalid witness file) 0 --- inspect .0015 .0021 .54 0    0      - --- inspect - --- 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.i false(unreach-call) 0 wit inspect 35    35    2200   330   .012  0      true -32 wit inspect 9.7  5.1  350 0    0     unknown 0 --- inspect 57     38     800   .68 0   unknown 0 --- inspect 6.8  3.8  280 0      .16  error (2) 0 --- inspect 1.4    1.4    24    .24 0      - --- inspect - --- 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.i error 0 --- inspect 880    880    1700   11000   .090  0      error (invalid witness file) 0 --- inspect .65 .40 40 0    0     error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .64 48 0      0     error (invalid witness file) 0 --- inspect .0038 .0048 .54 0    0      - --- inspect - --- 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.i error (42) 0 --- inspect 880    880    6800   5700   .086  0      error (invalid witness file) 0 --- inspect .72 .43 40 0    0     error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0      0     error (invalid witness file) 0 --- inspect .0052 .0065 .54 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    4300   5900   .086  0      error (invalid witness file) 0 --- inspect .60 .36 42 0    0     error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .59 47 0      0     error (invalid witness file) 0 --- inspect .0039 .0053 .42 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.i false(unreach-call) 0 wit inspect 830    830    2300   8700   .016  0      error (parsing failed) 0 --- inspect 12    6.4  730 0    0     error (7) 0 --- inspect 15     8.6   450   .70 0   timeout 0 --- inspect 7.1  130    400 .0041 0     error (1) 0 --- inspect .75   .75   22    .94 0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i out of memory 0 --- inspect 39    39    12000   570   .016  0      error (invalid witness file) 0 --- inspect .57 .36 40 0    0     error (2) 0 --- inspect .027 .028 5.5 0    0   error (invalid witness file) 0 --- inspect 1.2  .75 48 0      0     error (invalid witness file) 0 --- inspect .0041 .0054 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.i error 0 --- inspect 880    880    2000   5000   .090  .0082 error (invalid witness file) 0 --- inspect .67 .41 40 0    0     error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .62 48 0      0     error (invalid witness file) 0 --- inspect .0022 .0028 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.i false(valid-free) 0 wit inspect 41    41    970   590   .016  0      timeout 0 wit inspect 96    63    2200 0    0     error (7) 0 --- inspect 16     9.3   610   .66 0   timeout 0 --- inspect 8.4  130    540 .0041 0     error (1) 0 --- inspect .90   .93   25    2.2  1.6    - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.i false(unreach-call) 0 wit inspect 14    14    620   170   .012  0      timeout 0 wit inspect 98    59    2200 0    .057 error (7) 0 --- inspect 16     8.4   480   .70 0   timeout 0 --- inspect 7.6  130    430 .0041 0     error (1) 0 --- inspect .78   .78   23    1.4  0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.i false(unreach-call) 0 wit inspect 54    54    4300   430   .012  0      timeout 0 wit inspect 98    73    2000 0    0     error (7) 0 --- inspect 18     11     500   .70 0   timeout 0 --- inspect 7.8  130    430 .0041 0     error (1) 0 --- inspect .80   .80   23    1.6  0      - --- inspect - --- 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.i error 0 --- inspect 880    880    3400   5700   .10   0      error (invalid witness file) 0 --- inspect .69 .44 40 0    0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .66 48 0      0     error (invalid witness file) 0 --- inspect .0030 .0039 .52 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    3000   4300   .098  0      error (invalid witness file) 0 --- inspect .76 .45 40 0    0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0      0     error (invalid witness file) 0 --- inspect .0019 .0025 .53 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    2800   4500   .090  0      error (invalid witness file) 0 --- inspect .68 .42 40 0    0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0      0     error (invalid witness file) 0 --- inspect .0056 .0075 .53 0    0      - --- inspect - --- 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.i false(unreach-call) 0 wit inspect 6.0  6.0  580   68   .012  0      unknown 0 wit inspect 9.3  4.8  350 0    0     error (7) 0 --- inspect 75     53     730   .68 0   unknown 0 --- inspect 16    8.5  610 0      .77  error (1) 0 --- inspect 1.3    1.3    27    .21 0      - --- inspect - --- 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.i error 0 --- inspect 880    880    3100   4400   .090  0      error (invalid witness file) 0 --- inspect .61 .37 41 0    0     error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0      0     error (invalid witness file) 0 --- inspect .0019 .0036 .42 0    0      - --- inspect - --- 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.i error 0 --- inspect 880    880    6000   5200   .086  0      error (invalid witness file) 0 --- inspect .73 .45 41 0    0     error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0      0     error (invalid witness file) 0 --- inspect .0038 .0054 .42 0    0      - --- inspect - --- 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.i false(valid-free) 0 wit inspect 31    31    1300   450   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.8  5.2  340 0   0     true 2 --- inspect 23     14     910   .66  0  
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.i error (42) 0 --- inspect 880    880    1600   8100   15      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0     error (2) 0 --- inspect .021 .023 5.6 0     0  
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.i false(unreach-call) -16 wit inspect 30    30    1300   440   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 14    7.3  460 0   0     true 2 --- inspect 21     12     640   .66  0  
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.i error (42) 0 --- inspect 880    880    13000   6700   21      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    2900   8300   20      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0     error (2) 0 --- inspect .027 .029 5.7 0     0  
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.i out of memory 0 --- inspect 440    440    15000   2900   90      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   9700   16      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    4100   4100   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .028 .030 5.7 0     0  
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.i error (42) 0 --- inspect 880    880    13000   8000   250      .16   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   4900   .094  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 41 0   0     error (2) 0 --- inspect .025 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   6500   150      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   6400   150      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .84 .50 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   5000   .10   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 42 0   0     error (2) 0 --- inspect .025 .026 5.7 0     0  
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.i error (42) 0 --- inspect 880    880    13000   5100   72      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0     error (2) 0 --- inspect .025 .027 5.8 0     0  
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.i error (42) 0 --- inspect 880    880    13000   6800   260      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   7200   130      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0     error (2) 0 --- inspect .022 .023 5.7 0     0  
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.i error (42) 0 --- inspect 880    880    13000   3900   67      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   4900   62      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .027 .028 5.7 0     0  
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.i error (42) 0 --- inspect 880    880    13000   5400   56      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .52 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   6300   200      .14   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   7200   140      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   3900   .098  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    12000   4100   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   5200   43      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 41 0   0     error (2) 0 --- inspect .027 .029 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    4300   4100   6.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0     error (2) 0 --- inspect .023 .025 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   10000   14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    1500   5600   57      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    13000   5500   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0     error (2) 0 --- inspect .022 .024 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    2500   4600   57      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    12000   9200   8.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .48 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
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.i out of memory 0 --- inspect 210    210    15000   2500   2.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .44 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   9100   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
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.i out of memory 0 --- inspect 410    410    13000   3700   13      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .025 .025 5.6 0     0  
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.i out of memory 0 --- inspect 110    110    13000   1400   4.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i false(valid-free) 0 wit inspect 110    110    7700   1200   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 33    17    880 0   0     true 2 --- inspect 18     11     560   .66  0  
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.i error (42) 0 --- inspect 880    880    4000   3700   6.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    380   10000   6.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   7100   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 41 0   0     error (2) 0 --- inspect .025 .025 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   7500   40      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    4300   8400   26      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .45 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   9100   24      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   7800   31      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   10000   26      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0     error (2) 0 --- inspect .027 .029 5.8 0     0  
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.i error (42) 0 --- inspect 880    880    7300   8000   34      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   7900   14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   7700   28      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    3900   7500   19      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    14000   6700   23      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0     error (2) 0 --- inspect .027 .029 5.6 0     0  
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.i error (42) 0 --- inspect 880    880    10000   12000   .057  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .44 40 0   0     error (2) 0 --- inspect .031 .032 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-saitek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4900   7300   24      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-samsung.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8100   40      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-speedlink.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1900   7000   12      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-sunplus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7400   33      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-tivo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7500   36      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-topseed.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8000   36      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-twinhan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8900   58      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 42 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-uclogic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7500   9.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .027 .038 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-wacom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 39    39    13000   500   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0     error (2) 0 --- inspect .026 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-waltop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 390    390    14000   4800   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-zydacron.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 46    46    13000   490   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--ads7871.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 830    830    13000   7200   27      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--asus_atk0110.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 120    120    14000   1600   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--emc1403.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect .57 .56 45   6.5 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    18    860 0   0     true 2 --- inspect 18     9.8   550   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--gpio-fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 74    74    13000   870   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--max1111.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 460    460    14000   5200   6.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pcf8591.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect .51 .50 40   6.4 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 57    34    1600 0   0     true 2 --- inspect 18     9.7   540   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pmbus--max16064.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1600   7100   19      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pmbus--max8688.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1700   5900   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--algos--i2c-algo-pca.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    2500   4800   .082  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0     error (2) 0 --- inspect .030 .031 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--busses--i2c-diolan-u2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 48    48    13000   550   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--busses--i2c-tiny-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 42    42    3400   470   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960    600    6500 0   0     true 2 --- inspect 20     12     480   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--i2c-smbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 2.1  2.1  220   25   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.6  4.0  300 0   0     true 2 --- inspect 20     12     510   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ide--cmd640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8000   110      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .028 .029 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ide--ide-pnp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4700   8600   43      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .022 .023 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--gameport--lightning.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1200   7500   100      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .44 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--magellan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 150    150    14000   1500   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--spaceball.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 150    150    14000   1400   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--spaceorb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 170    170    13000   1700   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--stinger.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 1.3  1.3  130   18   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    16    820 0   0     true 2 --- inspect 16     9.8   420   .38  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--twidjoy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 130    130    14000   1500   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--warrior.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 30    30    1200   370   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    25    2000 0   0     true 2 --- inspect 16     9.5   440   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--zhenhua.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 15    15    480   170   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 36    19    1900 0   0     true 2 --- inspect 16     9.5   380   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--newtonkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    12000   12000   15      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .025 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--stowaway.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    7700   13000   14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--xtkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 340    340    13000   3500   25      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 42 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--atlas_btns.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8600   69      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .43 40 0   0     error (2) 0 --- inspect .023 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--cma3000_d0x_i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    12000   5800   56      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--xen-kbdfront.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8300   78      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--mouse--gpio_mouse.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7300   34      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--mouse--vsxxxaa.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 2.1  2.1  230   29   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--ad7879-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 79    79    14000   800   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--cyttsp_spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 1.1  1.1  180   16   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--dynapro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 17    17    520   210   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    23    2000 0   0     true 2 --- inspect 17     9.9   420   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--egalax_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 850    850    13000   11000   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--fujitsu_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 15    15    490   200   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 25    13    730 0   0     true 2 --- inspect 13     8.7   400   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--gunze.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 18    18    550   250   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 47    26    2000 0   0     true 2 --- inspect 13     8.5   410   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--hampshire.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 17    17    530   220   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 40    23    2000 0   0     true 2 --- inspect 17     10     430   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--inexio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 16    16    530   200   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 41    23    2000 0   0     true 2 --- inspect 13     8.6   430   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--mtouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 20    20    730   250   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 46    25    2000 0   0     true 2 --- inspect 16     10     420   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--penmount.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 58    58    14000   650   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchit213.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 18    18    560   230   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 46    25    2000 0   0     true 2 --- inspect 15     9.3   430   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchright.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 17    17    530   240   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    20    2000 0   0     true 2 --- inspect 15     9.2   400   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 19    19    620   240   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 43    23    1900 0   0     true 2 --- inspect 14     8.9   400   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--tsc40.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 17    17    550   210   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 37    20    2000 0   0     true 2 --- inspect 18     10     430   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--wacom_w8001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 52    52    14000   630   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--avm_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8600   12      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--b1pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 59    59    13000   710   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 42 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--b1pcmcia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    520   11000   1.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--avm--t1pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 100    100    12000   1200   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 42 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hardware--eicon--divadidd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    870   3700   .090  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--avma1_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   9800   74      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--elsa_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7400   64      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--sedlbauer_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8000   72      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--isdn--hisax--teles_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7300   68      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .47 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-bd2802.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 50    50    14000   570   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0     error (2) 0 --- inspect .021 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-lp5521.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 100    100    15000   1300   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-ot200.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    2900   7800   31      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-backlight.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 25    25    2200   280   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.3  3.9  270 0   0     true 2 --- inspect 12     7.2   360   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-default-on.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   9400   86      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--ledtrig-gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 34    34    2800   320   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.5  3.9  300 0   0     true 2 --- inspect 14     8.0   390   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--macintosh--mac_hid.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect .34 .33 29   4.2 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    11    520 0   0     true 2 --- inspect 13     8.4   400   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--md--dm-zero.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7500   14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--max2165.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 49    49    13000   600   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mc44s803.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 130    130    10000   1600   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    6.6  440 0   0     true 2 --- inspect 21     14     520   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2060.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 100    100    7800   920   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 16    8.3  450 0   0     true 2 --- inspect 28     18     760   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2131.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 10    10    900   110   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    8.7  470 0   0     true 2 --- inspect 26     18     1300   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt2266.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 16    16    1300   150   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.2  520 0   0     true 2 --- inspect 29     19     1200   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mxl5007t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 210    210    12000   1500   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0     error (2) 0 --- inspect .025 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--qt1010.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 58    58    14000   620   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda18218.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 55    55    14000   600   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda8290.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    5200   4400   .10   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--tda9887.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 26    26    2400   330   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    660    5700 0   0     true 2 --- inspect 35     22     900   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--bt8xx--dvb-bt8xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 140    140    13000   1300   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .022 .023 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-a800.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 420    420    12000   4800   .79   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 42 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-au6610.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 280    280    12000   3400   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 42 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 46    46    12000   550   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 240    240    14000   3600   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .45 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-ce6230.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 2.3  2.3  280   36   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .025 .038 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-cinergyT2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 99    99    13000   1100   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-mb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7800   53      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dibusb-mc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    760   11000   7.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-digitv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 58    58    13000   800   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtt200u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 230    230    14000   2200   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dtv5100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 240    240    13000   2800   .0082 .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-gl861.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 290    290    12000   3400   .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-mxl111sf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    5200   4500   .094  .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 43 0   0     error (2) 0 --- inspect .029 .030 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-nova-t-usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   6600   39      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-pctv452e.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 68    68    13000   910   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0     error (2) 0 --- inspect .026 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-rtl28xxu.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 1.1  1.1  71   12   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-ttusb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 140    140    6400   1000   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-umt-010.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   11000   6.9    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 97    97    13000   1100   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--mxl111sf-demod.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 73    73    13000   820   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--cxd2820r.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    1600   11000   .098  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dib3000mb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    2000   9600   .094  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dib3000mc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 210    210    4800   1500   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dvb_dummy_fe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 67    67    13000   970   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .023 .024 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--ec100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 59    59    14000   490   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--it913x-fe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 84    84    14000   900   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--rtl2830.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 80    80    14000   890   .016  .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--stb6000.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 100    100    7600   920   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    5.8  370 0   0     true 2 --- inspect 24     16     580   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tda18271c2dd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 160    160    11000   1300   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    890    3700 0   0     true 2 --- inspect 96     79     3700   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tda826x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 37    37    3200   400   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.7  5.1  310 0   0     true 2 --- inspect 28     17     610   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--tua6100.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 110    110    8400   1100   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    5.6  360 0   0     true 2 --- inspect 29     19     610   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--ttpci--budget-patch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 620    620    13000   3600   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (2) 0 --- inspect .030 .031 5.5 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--ttpci--budget.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    6300   6500   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-adstech-dvb-t-pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3700   7.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-alink-dtu-m.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3900   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .028 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-anysee.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4000   6.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .026 .027 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-apac-viewcomp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4500   5100   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0     error (2) 0 --- inspect .024 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-asus-pc39.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4300   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-ati-tv-wonder-hd-600.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3600   8.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-ati-x10.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3300   6.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-a16d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3700   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-cardbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4500   6100   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .021 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-dvbt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4400   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 40 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-m135a.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   3600   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-m733a-rm-k6.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4100   8.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0     error (2) 0 --- inspect .025 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia-rm-ks.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4000   7.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .022 .023 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avermedia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4900   7100   7.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-avertv-303.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4500   7.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0     error (2) 0 --- inspect .022 .023 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-azurewave-ad-tu700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3700   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-behold-columbus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4000   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 41 0   0     error (2) 0 --- inspect .030 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-behold.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   3700   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-budget-ci-old.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4900   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-cinergy-1400.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4800   6400   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-cinergy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4800   7.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dib0700-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3600   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dib0700-rc5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4600   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 42 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-digitalnow-tinytwin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4400   5700   8.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-digittrade.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3400   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dm1105-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3900   7.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dntv-live-dvb-t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3800   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-dntv-live-dvbt-pro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4200   8.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-em-terratec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3700   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0     error (2) 0 --- inspect .029 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-encore-enltv-fm53.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3800   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-encore-enltv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4100   6.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-encore-enltv2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4200   5300   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0     error (2) 0 --- inspect .027 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-evga-indtube.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4000   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-eztv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4100   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 40 0   0     error (2) 0 --- inspect .024 .025 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-flydvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4200   5300   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-flyvideo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4500   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-fusionhdtv-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4300   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-gadmei-rm008z.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4000   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .024 .025 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-genius-tvgo-a11mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4500   6.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-gotview7135.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4700   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 42 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-hauppauge.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4200   5400   6.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-imon-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4100   7.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .021 .024 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-imon-pad.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3900   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0     error (2) 0 --- inspect .023 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-iodata-bctv7e.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4600   7.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-it913x-v1.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3600   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 42 0   0     error (2) 0 --- inspect .022 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-it913x-v2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3900   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kaiomy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4200   6.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kworld-315u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   5000   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kworld-pc150u.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3900   6.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-kworld-plus-tv-analog.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4400   6.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-leadtek-y04g0051.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   5100   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-lirc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4000   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .46 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-lme2510.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4100   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-manli.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 870    880    3900   3500   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-medion-x10.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4100   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-digivox-ii.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3700   8.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .56 .35 40 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-digivox-iii.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4600   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0     error (2) 0 --- inspect .029 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-tvanywhere-plus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4000   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-msi-tvanywhere.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3700   7.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-nebula.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3600   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 41 0   0     error (2) 0 --- inspect .029 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-nec-terratec-cinergy-xs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3800   6.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .031 .034 5.5 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-norwood.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4200   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-npgtech.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4400   4900   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pctv-sedna.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   3400   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pinnacle-color.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4700   6000   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 42 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pinnacle-grey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4600   5700   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0     error (2) 0 --- inspect .028 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pinnacle-pctv-hd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3900   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .50 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview-002t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4700   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0     error (2) 0 --- inspect .021 .021 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview-mk12.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3800   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview-new.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4600   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0     error (2) 0 --- inspect .026 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pixelview.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4000   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-powercolor-real-angel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4200   8.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-proteus-2309.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3900   7.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-purpletv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3900   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .034 .035 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-pv951.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4200   4900   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-rc6-mce.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4000   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .38 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-real-audio-220-32-keys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3800   6.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-snapstream-firefly.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4200   7.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .36 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-streamzap.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4600   6.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tbs-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   3900   6.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-technisat-usb2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   3300   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-terratec-cinergy-xs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4100   8.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-terratec-slim-2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4000   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .020 .021 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-terratec-slim.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   3800   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tevii-nec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   2800   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tivo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   3900   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0     error (2) 0 --- inspect .024 .026 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-total-media-in-hand.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4600   7.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0     error (2) 0 --- inspect .026 .026 5.5 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-trekstor.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4400   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-tt-1500.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4600   5600   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-twinhan1027.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   3700   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-videomate-m1f.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4700   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .025 .026 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-videomate-s350.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4200   6000   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0     error (2) 0 --- inspect .020 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-videomate-tv-pvr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4000   4700   7.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0     error (2) 0 --- inspect .026 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-winfast-usbii-deluxe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 870    880    4200   6000   7.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0     error (2) 0 --- inspect .020 .020 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--rc--keymaps--rc-winfast.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4400   6200   6.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0     error (2) 0 --- inspect .021 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--cx231xx--cx231xx-dvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 120    120    13000   1500   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--em28xx--em28xx-dvb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    1600   5700   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .46 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_benq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3400   10000   120      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .023 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_finepix.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 4.8  4.8  650   56   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_jl2005bcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 18    18    4200   240   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .021 .023 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_pac207.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 57    57    13000   850   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_sq905c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3400   9400   21      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--gspca--gspca_stv0680.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8800   59      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--zoran--zr36016.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 71    71    5500   660   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 46    25    1200 0   0     true 2 --- inspect 23     13     530   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--message--i2o--i2o_bus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   6500   23      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--message--i2o--i2o_scsi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 6.3  6.3  780   77   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--janz-cmodio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 89    89    14000   1400   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 41 0   0     error (2) 0 --- inspect .025 .026 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--rdc321x-southbridge.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1500   12000   15      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--tps6105x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 460    460    13000   4700   4.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--tps6507x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect .40 .39 27   4.5 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 18    9.0  440 0   0     true 2 --- inspect 15     9.5   400   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--tps65217.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   10000   16      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--ucb1400_core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 2.4  2.4  250   29   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    610 0   0     true 2 --- inspect 13     7.2   360   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--wl1273-core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 710    710    14000   7800   19      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mfd--wm8400-core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 110    110    14000   1100   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--apds9802als.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4600   5800   40      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .47 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--bmp085.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 100    100    14000   1200   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--c2port--c2port-duramar2150.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1200   7300   44      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--eeprom--eeprom_93xx46.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 500    500    14000   5300   12      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--isl29020.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3600   6500   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--sgi-xp--xp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4400   3600   8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 42 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--ti_dac7512.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7700   30      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0     error (2) 0 --- inspect .032 .033 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--misc--tifm_core.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    7900   8800   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .027 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mmc--host--sdricoh_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   4700   40      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--docprobe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect 340    340    2800   4500   17      0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory (out of native memory) 0 --- inspect 830    810    7000 0   0     true 2 --- inspect 170     110     650   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--mtdram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    6900   8200   8.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--ftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 29    29    4400   390   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--inftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 290    290    13000   3300   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0     error (2) 0 --- inspect .021 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--maps--intel_vr_nor.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 370    370    12000   4800   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--mtdblock_ro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 440    440    13000   5100   2.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--nftl.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 170    170    5200   2000   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--onenand--onenand_sim.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 32    32    13000   390   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 42 0   0     error (2) 0 --- inspect .020 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--tests--mtd_oobtest.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .30 .30 24   3.4 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    2100 0   0     true 2 --- inspect 45     36     590   .086 0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--tests--mtd_pagetest.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .29 .29 23   3.4 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 13    7.5  820 0   0     true 2 --- inspect 21     13     520   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--mtd--ubi--gluebi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 46    46    2400   610   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 44    23    1200 0   0     error (7) 0 --- inspect 39     25     480   .71  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--arcnet--com20020_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 56    57    14000   580   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--act200l-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   6400   34      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .029 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--litelink-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   6200   31      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--ma600-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7900   6.6    .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--irda--tekram-sir.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7900   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--amd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8600   29      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .87 .53 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--broadcom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   4900   45      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0     error (2) 0 --- inspect .032 .033 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--cicada.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   5500   6.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 42 0   0     error (2) 0 --- inspect .026 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--davicom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7900   43      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--et1011c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7200   45      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--icplus.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7700   46      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--lxt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7200   35      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .38 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4800   6500   10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--micrel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8900   25      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 0   0     error (2) 0 --- inspect .023 .025 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--national.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8400   56      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--qsemi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7400   41      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--realtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   5600   8.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .43 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--smsc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7000   28      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--spi_ks8995.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 250    250    14000   3000   3.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--ste10Xp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   5700   62      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--phy--vitesse.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4100   6.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--ppp--bsd_comp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 49    49    13000   590   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--ppp--ppp_mppe.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 3.5  3.5  180   41   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 42 0   0     error (2) 0 --- inspect .026 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--sungem_phy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   5000   .074  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0     error (2) 0 --- inspect .026 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--team--team_mode_activebackup.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   9600   17      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--team--team_mode_roundrobin.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8800   56      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--airo_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 59    59    4600   590   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    5.5  440 0   0     true 2 --- inspect 15     8.2   480   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--ath--ath6kl--ath6kl_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 11    11    4000   150   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .34 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--mwifiex--mwifiex_pcie.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 48    48    12000   620   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--orinoco--orinoco_nortel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7500   140      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--orinoco--orinoco_pci.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   6300   43      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0     error (2) 0 --- inspect .024 .025 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--orinoco--orinoco_tmd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   6000   27      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--wl1251--wl1251_spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    2000   12000   .057  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--net--wireless--wl12xx--wl12xx_sdio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 79    79    14000   1000   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .40 42 0   0     error (2) 0 --- inspect .020 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--parport--parport_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 190    190    12000   1800   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 12    6.3  440 0   0     true 2 --- inspect 18     10     470   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--pci--ioapic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 370    370    13000   4000   2.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--pci--pci-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1400   11000   15      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--asus-nb-wmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7800   55      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--intel_menlow.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7300   51      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--panasonic-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 3.4  3.4  370   44   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 58    57    2200   710   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 6.8  3.6  280 0   0     true 2 --- inspect 21     13     920   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--toshiba_bluetooth.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 870    880    13000   6900   26      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--platform--x86--xo15-ebook.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 88    88    4500   920   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    8.9  460 0   0     true 2 --- inspect 19     12     720   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (6) 0 --- inspect 120    120    13000   1400   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--power--wm831x_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 110    110    13000   1200   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--gpio-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 42    42    13000   530   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--max1586.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 590    590    13000   3500   1.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--max8649.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 540    540    13000   3600   1.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--userspace-consumer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 1.6  1.6  190   23   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 32    16    740 0   0     true 2 --- inspect 17     9.4   450   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--virtual.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 260    260    13000   2900   7.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm831x-dcdc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 74    74    13000   1100   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 42 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm831x-isink.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7000   47      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm831x-ldo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8100   50      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .39 41 0   0     error (2) 0 --- inspect .026 .027 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--regulator--wm8400-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    11000   6100   26      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 42 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-da9052.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7400   37      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds1390.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 400    400    14000   3800   1.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .034 .035 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds1553.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   7500   55      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .37 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds3232.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 53    53    14000   560   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-ds3234.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8400   36      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 40 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-m41t93.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   6400   55      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0     error (2) 0 --- inspect .027 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-m41t94.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7000   37      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0     error (2) 0 --- inspect .027 .029 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-m48t86.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7200   81      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-max6902.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7700   35      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-mc13xxx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   6800   21      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0     error (2) 0 --- inspect .026 .027 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-pcap.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   6400   44      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 42 0   0     error (2) 0 --- inspect .025 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-pcf2123.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 54    54    14000   530   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 41 0   0     error (2) 0 --- inspect .023 .025 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-r9701.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   6900   110      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-rs5c348.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 55    55    14000   600   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .47 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-stk17ta8.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   6600   65      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-test.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   5200   33      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-v3020.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 390    390    13000   2100   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0     error (2) 0 --- inspect .031 .031 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--rtc--rtc-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   9500   32      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .43 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--dmx3191d.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    620   8000   9.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 42 0   0     error (2) 0 --- inspect .026 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--iscsi_boot_sysfs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 65    65    6600   560   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 20    10    570 0   0     true 2 --- inspect 23     13     670   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--pcmcia--sym53c500_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 48    48    13000   590   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--scsi--qlogicfas408.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   5500   .090  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--spi--spi-tle62x0.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 120    120    13000   1600   .70   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--android--switch--switch_gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 520    520    14000   5500   15      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--comedi--drivers--8255.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    1700   6300   .11   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--comedi--drivers--comedi_bond.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 5.0  5.0  1100   75   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--addac--adt7316-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    2900   7900   38      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad5930.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   10000   33      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 41 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9832.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   5600   75      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9850.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   10000   33      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9852.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   9600   28      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 40 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9910.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   10000   56      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .39 41 0   0     error (2) 0 --- inspect .022 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--dds--ad9951.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   10000   34      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--iio--resolver--ad2s90.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   10000   41      .16   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--phison--phison.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3300   8200   31      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 42 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_acntsa.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8300   140      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 40 0   0     error (2) 0 --- inspect .024 .025 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_bns.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4300   7.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_dummy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4600   6800   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0     error (2) 0 --- inspect .023 .025 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_ltlk.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    15000   9200   150      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_soft.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   9500   41      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_spkout.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    2900   5200   14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 42 0   0     error (2) 0 --- inspect .023 .024 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--speakup--speakup_txprt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4800   8.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 42 0   0     error (2) 0 --- inspect .020 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--telephony--ixj_pcmcia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 55    55    14000   580   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--vme--boards--vme_vmivme7805.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    12000   7600   33      .13   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0     error (2) 0 --- inspect .027 .029 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--staging--zram--zram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 400    400    13000   4600   29      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--target--loopback--tcm_loop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    10000   5500   .094  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--altera_jtaguart.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8900   140      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--altera_uart.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   6300   100      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--mfd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 41    41    13000   530   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--uartlite.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   5700   49      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0     error (2) 0 --- inspect .026 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--tty--serial--xilinx_uartps.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7100   110      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uio--uio_aec.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 42    42    3400   440   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    5.8  370 0   0     true 2 --- inspect 13     7.6   380   .62  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uio--uio_pci_generic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-free) 0 wit inspect 6.4  6.4  450   90   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    5.7  360 0   0     true 2 --- inspect 13     8.4   340   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uio--uio_sercos3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 33    33    13000   490   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .031 .032 5.5 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--atm--xusbatm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .41 .40 34   3.5 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.7  5.1  350 0   0     true 2 --- inspect 24     14     680   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--misc--cypress_cy7c63.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 1.2  1.2  120   15   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    13    680 0   0     true 2 --- inspect 17     9.2   490   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--misc--cytherm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 1.4  1.4  130   19   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 49    29    1500 0   0     true 2 --- inspect 21     11     530   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--otg--ab8500-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 140    140    14000   1600   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 42 0   0     error (2) 0 --- inspect .025 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--otg--nop-usb-xceiv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 530    530    14000   5700   11      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--ipaq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    7200   4600   44      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--ir-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 370    370    14000   3600   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .35 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--iuu_phoenix.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 43    43    12000   500   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--metro-usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 140    140    14000   1800   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--serial--spcp8x5.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 48    48    13000   610   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .42 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-alauda.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8600   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-cypress.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8900   17      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-datafab.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8500   22      .16   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 40 0   0     error (2) 0 --- inspect .023 .025 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-freecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8700   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 42 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-jumpshot.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   9400   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 41 0   0     error (2) 0 --- inspect .023 .024 5.8 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-sddr09.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   11000   38      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-sddr55.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   9900   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--usb--storage--ums-usbat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8700   22      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--uwb--i1480--i1480-est.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4300   4600   7.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .42 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--ili9320.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 49    49    13000   600   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .39 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--l4f00242t03.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 51    51    13000   510   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0     error (2) 0 --- inspect .027 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--lms283gf05.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 280    280    14000   2400   19      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--tdo24m.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    3800   4600   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--backlight--vgg2432a4.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3900   7800   43      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--video--n411.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .17 .17 19   2.1 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.9  5.3  370 0   0     true 2 --- inspect 14     8.0   480   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--masters--ds2490.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(valid-deref) 0 wit inspect 4.3  4.3  450   56   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960    700    5700 0   0     true 2 --- inspect 22     13     530   .66  0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--masters--matrox_w1.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 480    480    13000   6000   9.7    .16   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--masters--w1-gpio.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 --- inspect 880    880    4100   7000   .086  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .45 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_bq27000.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7800   34      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0     error (2) 0 --- inspect .026 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2408.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    2900   4600   38      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 42 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2423.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    590   13000   9.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2431.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 3.0  3.0  180   39   .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2433.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 56    56    14000   600   .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2760.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7800   27      .061  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0     error (2) 0 --- inspect .024 .024 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2780.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8400   29      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_ds2781.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   10000   26      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 40 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--w1--slaves--w1_smem.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    4100   4700   8.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--watchdog--sbc_epx_c3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    3800   6000   26      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0     error (2) 0 --- inspect .028 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--watchdog--wm831x_wdt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   7600   41      .16   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 41 0   0     error (2) 0 --- inspect .028 .031 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--gpu--drm--drm_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    1600   9500   8.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--keyboard--gpio_keys_polled.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 160    160    13000   1500   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0     error (2) 0 --- inspect .029 .030 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ab8500-ponkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   9800   7.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .43 40 0   0     error (2) 0 --- inspect .027 .028 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ad714x-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    13000   8200   48      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--ad714x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   8800   49      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--adxl34x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (42) 0 --- inspect 880    880    14000   9000   44      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .37 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--mma8450.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 180    180    14000   1800   .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--mpu3050.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 440    440    14000   4700   1.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .40 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--pcap_keys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 540    540    13000   5100   8.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3_false-termination.4-32_1-drivers--input--misc--pcf50633-input.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 800    800    14000   11000   7.1    0      - --- inspect - --- inspect