Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]
Run set sv-comp17.Systems_DeviceDriversLinux64_ReachSafety
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 4.5  4.5  50   250 .0082 0      error (invalid witness file) .48 .32 5.8 40 error (invalid witness file) 8.1 4.2 140 330 - -
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 240    240    1400   1000 .0082 0      error (invalid witness file) .73 .45 9.3 43 error (invalid witness file) 7.4 3.9 140 310 - -
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 25    25    300   340 .0082 0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 8.8 4.6 77 310 - -
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 54    54    380   2300 .0082 0      timeout 97    76    2100   3300 unknown 11   5.7 180 340 - -
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    9200   6900 .0082 0      error (invalid witness file) .48 .31 9.7 39 error (invalid witness file) 7.7 4.0 150 320 - -
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    5400   2700 .0082 0      error (invalid witness file) .51 .32 12   40 error (invalid witness file) 7.4 3.9 130 310 - -
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 5.8  5.8  65   180 .0082 0      error (invalid witness file) .50 .32 10   39 error (invalid witness file) 8.1 4.3 85 300 - -
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    4200   4400 .0082 0      error (invalid witness file) .49 .31 8.6 40 error (invalid witness file) 7.2 3.8 100 310 - -
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    10000   2700 .0082 0      error (invalid witness file) .50 .33 13   39 error (invalid witness file) 8.9 4.7 120 320 - -
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 5.0  5.0  56   270 .21   0      true 11    5.6  150   410 unknown 52   29   890 940 - -
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    7200   1300 12      0      error (invalid witness file) .54 .35 12   43 error (invalid witness file) 7.4 3.9 89 300 - -
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    4200   2800 .0082 13      error (invalid witness file) .47 .31 4.4 40 error (invalid witness file) 7.8 4.1 94 300 - -
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 42    42    450   3300 .0082 0      timeout 98    85    1100   3100 true 17   9.4 270 490 - -
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i error (134) 0 wit inspect 65    65    850   14000 .0082 0      error (invalid witness file) .53 .35 9.2 40 error (invalid witness file) 8.0 4.2 140 330 - -
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 36    36    470   700 1.6    0      timeout 97    73    2000   3800 true 18   9.7 380 500 - -
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i false(unreach-call) 0 wit inspect 2.7  2.7  29   290 .0082 0      timeout 97    74    1100   4200 true 30   17   670 790 - -
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    6200   4200 .0082 .0041 - - error (invalid witness file) .64 .41 7.8 39 error (invalid witness file) 7.4 3.9 140 310
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i true 1 wit inspect 680    680    6100   7100 29      0      - - exception 33    17    330   940 timeout 960   750   25000 1400
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    3400   810 0      0      - - error (invalid witness file) .48 .31 6.6 40 error (invalid witness file) 6.8 3.6 110 300
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    4100   3500 .0082 .55   - - error (invalid witness file) .59 .38 9.5 39 error (invalid witness file) 8.2 4.3 140 330
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    4100   2400 25      0      - - error (invalid witness file) .67 .43 7.5 40 error (invalid witness file) 7.3 3.8 150 330
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    8100   3200 65      0      - - error (invalid witness file) .63 .39 8.2 39 error (invalid witness file) 9.1 4.7 170 340
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    3000   2800 0      0      - - error (invalid witness file) .51 .33 7.7 40 error (invalid witness file) 7.1 3.7 110 300
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    4900   1200 26      0      - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 7.7 4.0 120 330
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    7000   3000 25      0      - - error (invalid witness file) .61 .37 9.3 42 error (invalid witness file) 7.2 3.8 140 310
ldv-linux-3.0/module_get_put-drivers-net-pppox.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    6300   3300 7.4    0      - - error (invalid witness file) .67 .42 8.6 39 error (invalid witness file) 6.3 3.4 110 300
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    4100   2600 .025  .16   - - error (invalid witness file) .48 .31 10   40 error (invalid witness file) 6.8 3.6 130 310
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    4800   5900 .0082 0      - - error (invalid witness file) .52 .33 9.3 40 error (invalid witness file) 7.5 4.0 150 320
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    7000   14000 32      11      - - error (invalid witness file) .50 .32 9.2 41 error (invalid witness file) 7.1 3.7 140 310
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    8300   3400 .0082 0      - - error (invalid witness file) .73 .45 8.4 41 error (invalid witness file) 9.6 5.0 110 310
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    5000   2100 5.3    0      - - error (invalid witness file) .57 .37 11   43 error (invalid witness file) 7.8 4.0 90 310
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    5800   3200 .025  .23   - - error (invalid witness file) .49 .31 9.1 40 error (invalid witness file) 7.5 3.9 160 310
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    5900   4700 28      0      - - error (invalid witness file) .62 .40 8.2 39 error (invalid witness file) 6.1 3.3 120 300
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    3900   1000 .025  0      - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.8 3.6 120 310
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    5500   1600 .0082 .36   - - error (invalid witness file) .70 .44 9.0 42 error (invalid witness file) 6.8 3.6 100 310
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    3800   2800 .0082 0      - - error (invalid witness file) .63 .39 7.1 40 error (invalid witness file) 7.8 4.1 160 310
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    4800   1800 7.9    0      - - error (invalid witness file) .68 .42 7.8 41 error (invalid witness file) 7.3 3.8 140 300
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    9300   910 .025  0      - - error (invalid witness file) .66 .42 7.2 39 error (invalid witness file) 7.9 4.1 150 320
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    9400   950 .025  0      - - error (invalid witness file) .57 .37 12   43 error (invalid witness file) 6.5 3.4 140 300
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i error (42) 0 wit inspect 850    850    6500   14000 .025  0      - - error (invalid witness file) .48 .32 11   40 error (invalid witness file) 7.3 3.8 130 320
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i error (1) 0 wit inspect 850    850    6700   5700 .0082 0      - - error (invalid witness file) .68 .42 7.8 40 error (invalid witness file) 6.9 3.6 130 310
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    5500   4800 .012  0      error (invalid witness file) .51 .33 12   41 error (invalid witness file) 8.5 4.4 140 330 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 4.5  4.5  58   1200 .012  0      error (invalid witness file) .54 .34 6.4 42 error (invalid witness file) 7.1 3.7 110 310 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 15    15    210   420 .012  0      error (invalid witness file) .60 .39 9.6 40 error (invalid witness file) 7.2 3.8 120 300 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--isdn--capi--kernelcapi.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 1 wit inspect 1.3  1.3  14   130 .012  0      false(unreach-call) 31    22    290   880 unknown 11   5.8 150 340 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (134) 0 wit inspect 75    75    960   14000 .012  .098  error (invalid witness file) .51 .34 9.6 40 error (invalid witness file) 8.2 4.3 170 330 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    2900   2800 .012  0      error (invalid witness file) .48 .32 7.3 40 error (invalid witness file) 7.5 4.0 150 310 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--mem2mem_testdev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (134) 0 wit inspect 40    40    450   13000 .012  .074  error (invalid witness file) .53 .34 14   42 error (invalid witness file) 7.0 3.7 100 310 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--vivi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (134) 0 wit inspect 45    45    620   13000 .012  .074  error (invalid witness file) .51 .33 12   40 error (invalid witness file) 8.0 4.2 120 310 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--mtd--chips--cfi_cmdset_0001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    6200   1100 .012  0      error (invalid witness file) .52 .33 7.4 40 error (invalid witness file) 7.5 4.0 140 320 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (134) 0 wit inspect 38    38    500   14000 .012  0      error (invalid witness file) .52 .33 12   40 error (invalid witness file) 7.0 3.6 130 310 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    4300   4900 .012  0      error (invalid witness file) .46 .31 5.3 40 error (invalid witness file) 8.8 4.6 110 310 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    7300   4400 .012  0      error (invalid witness file) .51 .33 13   40 error (invalid witness file) 8.5 4.4 150 350 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    5200   3700 .012  0      error (invalid witness file) .50 .32 5.2 41 error (invalid witness file) 10   5.3 130 330 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (134) 0 wit inspect 44    44    550   13000 .012  0      error (invalid witness file) .56 .38 13   44 error (invalid witness file) 7.2 3.8 130 310 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--storage--usb-storage.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    7500   3900 .012  0      error (invalid witness file) .54 .35 14   40 error (invalid witness file) 8.7 4.6 100 320 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--vhost--vhost_net.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c error (134) 0 wit inspect 130    130    1300   13000 .012  0      error (invalid witness file) .54 .35 13   40 error (invalid witness file) 7.3 3.8 150 330 - -
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    5000   3700 .012  0      error (invalid witness file) .49 .32 8.7 39 error (invalid witness file) 8.9 4.7 120 320 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c error (1) 0 wit inspect 4.2  4.2  52   440 .012  0      error (invalid witness file) .52 .35 10   42 error (invalid witness file) 9.1 4.7 140 340 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.c false(unreach-call) 0 wit inspect 440    440    2800   2400 .012  0      unknown 23    12    380   930 error 17   8.7 310 350 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c false(unreach-call) 0 wit inspect 6.1  6.0  64   630 .012  0      unknown 28    15    190   1300 error 19   10   210 360 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c error (1) 0 wit inspect 850    850    6300   2500 .012  0      error (invalid witness file) .55 .34 11   39 error (invalid witness file) 11   5.9 100 340 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c error (1) 0 wit inspect 850    850    4600   3800 .012  .61   error (invalid witness file) .49 .32 12   40 error (invalid witness file) 10   5.4 130 340 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c false(unreach-call) 0 wit inspect 7.5  7.5  88   1000 .012  0      unknown 26    14    560   1000 error 17   8.8 310 340 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c false(unreach-call) 0 wit inspect 1.8  1.8  17   180 .012  0      unknown 27    15    510   1300 error 18   9.5 270 350 - -
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--misc--sgi-xp--xpc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    3800   13000 .012  0      error (invalid witness file) .72 .46 6.5 43 error (invalid witness file) 7.6 4.0 140 320 - -
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--net--wireless--orinoco--orinoco_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    4200   4000 .012  0      error (invalid witness file) .54 .34 13   41 error (invalid witness file) 7.5 3.9 160 300 - -
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    6000   3600 .012  0      error (invalid witness file) .50 .33 13   39 error (invalid witness file) 9.3 4.8 100 320 - -
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c false(unreach-call) 0 wit inspect 570    570    3100   9100 .69   .66   timeout 97    81    1100   2200 true 31   17   500 810 - -
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    5000   5700 .012  0      error (invalid witness file) .48 .32 13   40 error (invalid witness file) 8.2 4.3 110 330 - -
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--pch_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 850    850    4100   7300 .012  0      error (invalid witness file) .50 .31 12   40 error (invalid witness file) 8.9 4.7 120 330 - -
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--apei--einj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4500   4700 55      0      - - error (invalid witness file) .59 .38 8.7 40 error (invalid witness file) 8.8 4.6 96 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--bgrt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5600   14000 58      0      - - error (invalid witness file) .64 .41 7.2 40 error (invalid witness file) 6.3 3.4 120 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    10000   14000 23      0      - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.8 3.6 140 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6900   1600 11      0      - - error (invalid witness file) .60 .38 9.5 40 error (invalid witness file) 6.7 3.6 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7000   14000 26      .074  - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 6.4 3.3 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6600   14000 29      .074  - - error (invalid witness file) .51 .32 7.9 42 error (invalid witness file) 6.4 3.4 100 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_netcell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4600   3800 35      0      - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.5 3.4 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--atm--adummy.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5100   14000 23      0      - - error (invalid witness file) .68 .43 7.2 42 error (invalid witness file) 6.9 3.6 140 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (1) 0 wit inspect 310    310    1600   15000 45      0      - - error (invalid witness file) .51 .34 9.5 40 error (invalid witness file) 6.2 3.2 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864bfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    10000   13000 12      0      - - error (invalid witness file) .48 .31 11   40 error (invalid witness file) 6.7 3.6 140 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4000   4700 6.0    0      - - error (invalid witness file) .54 .35 9.6 40 error (invalid witness file) 6.9 3.6 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--aten.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7900   14000 190      .074  - - error (invalid witness file) .69 .44 8.7 40 error (invalid witness file) 6.6 3.5 140 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6900   14000 .012  .074  - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 7.3 3.8 150 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--comm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5600   14000 120      .074  - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 7.1 3.7 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5100   14000 120      0      - - error (invalid witness file) .57 .37 14   46 error (invalid witness file) 8.2 4.3 110 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5200   14000 72      0      - - error (invalid witness file) .67 .42 7.8 41 error (invalid witness file) 7.6 3.9 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4900   14000 56      .074  - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.6 3.5 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    11000   14000 510      0      - - error (invalid witness file) .66 .43 7.4 39 error (invalid witness file) 6.0 3.2 130 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6200   14000 190      0      - - error (invalid witness file) .64 .40 7.8 40 error (invalid witness file) 6.8 3.6 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--friq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4800   14000 52      0      - - error (invalid witness file) .64 .40 7.9 40 error (invalid witness file) 8.4 4.4 170 320
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--frpw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4900   14000 48      0      - - error (invalid witness file) .53 .34 13   41 error (invalid witness file) 7.8 4.1 82 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--kbic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7600   14000 190      0      - - error (invalid witness file) .54 .33 12   41 error (invalid witness file) 7.3 3.8 150 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--ktti.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7700   14000 510      .012  - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.5 2.9 83 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7200   14000 170      .078  - - error (invalid witness file) .59 .36 8.6 40 error (invalid witness file) 6.7 3.6 140 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5300   14000 89      .078  - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 7.7 4.0 150 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--hw_random--virtio-rng.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    3900   14000 .012  .074  - - error (invalid witness file) .60 .38 9.6 40 error (invalid witness file) 5.9 3.1 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4600   13000 26      0      - - error (invalid witness file) .55 .35 10   39 error (invalid witness file) 6.5 3.4 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ramoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    3800   4700 6.7    0      - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.8 3.6 74 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--tpm--tpm_nsc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6700   14000 8.5    .074  - - error (invalid witness file) .63 .39 7.3 40 error (invalid witness file) 6.9 3.6 100 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--uv_mmtimer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7800   13000 94      0      - - error (invalid witness file) .53 .35 8.8 39 error (invalid witness file) 6.7 3.5 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4400   4500 38      0      - - error (invalid witness file) .67 .42 9.1 40 error (invalid witness file) 6.3 3.3 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--cpufreq_powersave.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4400   14000 16      .078  - - error (invalid witness file) .65 .41 8.5 40 error (invalid witness file) 5.9 3.1 110 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--pcc-cpufreq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8400   14000 30      .074  - - error (invalid witness file) .66 .43 7.9 41 error (invalid witness file) 6.5 3.4 120 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5000   13000 20      0      - - error (invalid witness file) .55 .35 9.7 39 error (invalid witness file) 5.8 3.1 91 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--firmware--google--gsmi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6000   3400 28      0      - - error (invalid witness file) .70 .44 7.6 40 error (invalid witness file) 6.8 3.6 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--firmware--google--memconsole.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    9300   13000 19      0      - - error (invalid witness file) .57 .36 8.6 42 error (invalid witness file) 6.4 3.4 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5700   1500 26      0      - - error (invalid witness file) .54 .34 11   42 error (invalid witness file) 6.2 3.3 100 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7600   14000 13      0      - - error (invalid witness file) .59 .38 10   41 error (invalid witness file) 6.5 3.4 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6000   2300 34      0      - - error (invalid witness file) .58 .37 8.9 40 error (invalid witness file) 6.7 3.5 110 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-tps65912.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    11000   13000 .47   13      - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 5.7 3.1 120 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6800   1900 110      0      - - error (invalid witness file) .64 .41 8.1 41 error (invalid witness file) 6.2 3.3 130 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--drm_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6300   5400 15      0      - - error (invalid witness file) .49 .30 12   39 error (invalid witness file) 6.1 3.3 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7100   13000 54      0      - - error (invalid witness file) .58 .36 8.8 41 error (invalid witness file) 6.1 3.3 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    3800   4300 6.4    0      - - error (invalid witness file) .54 .35 13   41 error (invalid witness file) 6.4 3.4 140 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--stub--poulsbo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8000   1400 10      0      - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.3 3.3 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-cherry.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6700   13000 52      0      - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 7.0 3.6 120 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-chicony.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6900   13000 33      0      - - error (invalid witness file) .50 .33 9.9 39 error (invalid witness file) 6.7 3.5 150 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5300   6000 39      0      - - error (invalid witness file) .66 .41 9.2 40 error (invalid witness file) 5.8 3.1 120 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6000   14000 20      0      - - error (invalid witness file) .60 .38 10   41 error (invalid witness file) 6.4 3.4 120 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6900   14000 29      13      - - error (invalid witness file) .63 .41 6.9 40 error (invalid witness file) 7.0 3.7 140 320
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6700   14000 22      0      - - error (invalid witness file) .48 .30 7.2 40 error (invalid witness file) 6.6 3.5 140 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-keytouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5100   11000 24      0      - - error (invalid witness file) .54 .33 7.9 40 error (invalid witness file) 6.3 3.4 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-lcpower.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7400   13000 47      0      - - error (invalid witness file) .61 .38 8.7 39 error (invalid witness file) 8.1 4.2 95 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-monterey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6600   13000 27      0      - - error (invalid witness file) .49 .32 13   39 error (invalid witness file) 6.7 3.6 140 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ortek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    2900   2500 31      13      - - error (invalid witness file) .54 .35 13   41 error (invalid witness file) 6.5 3.4 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-petalynx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8500   14000 16      .26   - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 6.7 3.5 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-primax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    9700   14000 1.9    .070  - - error (invalid witness file) .64 .41 8.2 42 error (invalid witness file) 6.5 3.4 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-saitek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5200   6700 36      0      - - error (invalid witness file) .65 .41 7.4 40 error (invalid witness file) 7.6 4.0 150 310
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.c error (42) 0 wit inspect 850    850    8400   14000 33      0      - - error (invalid witness file) .61 .39 9.3 43 error (invalid witness file) 7.0 3.7 140 300
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.c error (42) 0 wit inspect 850    850    5300   4600 23      0      - - error (invalid witness file) .64 .41 7.8 40 error (invalid witness file) 6.4 3.3 130 300
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.c error (42) 0 wit inspect 850    850    7100   14000 40      0      - - error (invalid witness file) .52 .35 12   39 error (invalid witness file) 7.4 3.9 85 300
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.c error (42) 0 wit inspect 850    850    6900   13000 37      0      - - error (invalid witness file) .68 .42 8.3 40 error (invalid witness file) 6.6 3.5 120 300
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.c error (42) 0 wit inspect 850    850    6700   14000 40      .074  - - error (invalid witness file) .50 .32 11   41 error (invalid witness file) 6.4 3.4 130 300
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.c error (42) 0 wit inspect 850    850    7300   13000 60      11      - - error (invalid witness file) .61 .39 9.2 40 error (invalid witness file) 6.0 3.2 110 300
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.c error (42) 0 wit inspect 850    850    4800   14000 15      13      - - error (invalid witness file) .60 .38 7.6 41 error (invalid witness file) 6.2 3.3 120 300
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.c error (42) 0 wit inspect 850    850    7100   14000 110      0      - - error (invalid witness file) .64 .41 7.7 40 error (invalid witness file) 6.4 3.4 110 300
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.c out of memory 0 wit inspect 730    730    8000   15000 53      .074  - - error (invalid witness file) .64 .41 8.2 42 error (invalid witness file) 6.4 3.4 120 300
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.c error (42) 0 wit inspect 850    850    8800   14000 81      .078  - - error (invalid witness file) .71 .46 7.9 43 error (invalid witness file) 5.7 3.0 110 290
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.c error (42) 0 wit inspect 850    850    6300   2800 47      0      - - error (invalid witness file) .53 .33 9.4 43 error (invalid witness file) 7.1 3.7 110 300
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.c error (42) 0 wit inspect 850    850    5400   13000 .037  0      - - error (invalid witness file) .53 .34 10   42 error (invalid witness file) 9.9 5.1 110 330
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.c error (42) 0 wit inspect 850    850    5400   14000 6.1    0      - - error (invalid witness file) .61 .39 5.5 39 error (invalid witness file) 6.2 3.3 130 300
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.c error (42) 0 wit inspect 850    850    9900   13000 25      .074  - - error (invalid witness file) .65 .40 7.5 40 error (invalid witness file) 6.7 3.6 140 320
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.c error (42) 0 wit inspect 850    850    6500   13000 22      .14   - - error (invalid witness file) .48 .31 10   39 error (invalid witness file) 7.5 3.9 79 310
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.c error (42) 0 wit inspect 850    850    4500   14000 6.6    0      - - error (invalid witness file) .51 .31 11   40 error (invalid witness file) 6.3 3.3 110 300
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.c error (42) 0 wit inspect 850    850    4800   1400 13      0      - - error (invalid witness file) .73 .47 8.9 45 error (invalid witness file) 6.6 3.5 130 300
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.c error (42) 0 wit inspect 850    850    4000   1400 15      0      - - error (invalid witness file) .65 .41 8.3 41 error (invalid witness file) 6.3 3.3 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--smsc47b397.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7400   13000 14      0      - - error (invalid witness file) .54 .35 10   40 error (invalid witness file) 6.7 3.5 130 300
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.c error (1) 0 wit inspect 850    850    6600   2100 .0041 0      - - error (invalid witness file) .64 .41 7.2 40 error (invalid witness file) 6.6 3.5 120 300
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.c error (42) 0 wit inspect 850    850    7900   13000 .012  0      - - error (invalid witness file) .75 .46 8.4 42 error (invalid witness file) 6.5 3.4 140 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--i2c--busses--i2c-stub.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .37 .37 3.9 26 .0082 0      - - exception 7.2  3.9  85   290 true 20   10   380 560
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.c error (42) 0 wit inspect 850    850    9700   14000 21      0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.3 3.3 130 300
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.c error (42) 0 wit inspect 850    850    7000   14000 19      .074  - - error (invalid witness file) .59 .39 8.6 39 error (invalid witness file) 8.2 4.3 90 300
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.c error (42) 0 wit inspect 850    850    9100   14000 79      0      - - error (invalid witness file) .66 .41 10   41 error (invalid witness file) 8.6 4.5 110 320
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.c error (42) 0 wit inspect 850    850    5300   3400 32      0      - - error (invalid witness file) .62 .40 7.6 40 error (invalid witness file) 6.9 3.7 110 300
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.c error (42) 0 wit inspect 850    850    6900   14000 120      0      - - error (invalid witness file) .56 .35 9.4 40 error (invalid witness file) 6.4 3.4 120 300
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.c error (42) 0 wit inspect 850    850    8800   13000 55      0      - - error (invalid witness file) .64 .41 8.0 40 error (invalid witness file) 6.7 3.5 100 310
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.c error (42) 0 wit inspect 850    850    7900   13000 33      0      - - error (invalid witness file) .55 .36 9.1 39 error (invalid witness file) 6.0 3.2 120 300
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.c error (42) 0 wit inspect 850    850    6200   13000 37      0      - - error (invalid witness file) .63 .40 6.5 41 error (invalid witness file) 6.4 3.4 93 300
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.c error (42) 0 wit inspect 850    850    9700   13000 15      0      - - error (invalid witness file) .63 .41 8.1 40 error (invalid witness file) 6.1 3.3 110 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--turbografx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    11000   13000 51      0      - - error (invalid witness file) .57 .35 7.9 40 error (invalid witness file) 6.7 3.6 120 290
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.c error (42) 0 wit inspect 850    850    6100   13000 160      0      - - error (invalid witness file) .54 .35 10   39 error (invalid witness file) 6.7 3.5 140 310
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.c error (42) 0 wit inspect 850    850    6000   13000 25      0      - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.8 3.6 120 300
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.c error (42) 0 wit inspect 850    850    6800   14000 9.8    0      - - error (invalid witness file) .68 .42 11   44 error (invalid witness file) 6.1 3.2 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--keyboard--gpio_keys_polled.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8000   14000 37      0      - - error (invalid witness file) .50 .32 11   41 error (invalid witness file) 6.8 3.5 130 300
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.c error (42) 0 wit inspect 850    850    8300   13000 30      0      - - error (invalid witness file) .67 .43 7.6 41 error (invalid witness file) 7.5 4.0 85 300
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.c error (42) 0 wit inspect 850    850    10000   14000 31      0      - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 7.0 3.7 130 300
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.c error (42) 0 wit inspect 850    850    8800   13000 29      0      - - error (invalid witness file) .68 .43 7.8 40 error (invalid witness file) 6.5 3.5 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--ab8500-ponkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6000   13000 6.5    0      - - error (invalid witness file) .52 .33 9.1 40 error (invalid witness file) 6.1 3.3 120 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--ad714x-i2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4900   14000 33      0      - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 8.2 4.3 97 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--ad714x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8200   14000 34      0      - - error (invalid witness file) .66 .41 12   43 error (invalid witness file) 6.1 3.3 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--adxl34x-spi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5000   4500 29      0      - - error (invalid witness file) .52 .33 6.8 42 error (invalid witness file) 6.3 3.3 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--apanel.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5800   14000 38      0      - - error (invalid witness file) .48 .32 11   39 error (invalid witness file) 6.1 3.2 110 290
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.c error (42) 0 wit inspect 850    850    7100   14000 98      0      - - error (invalid witness file) .60 .38 8.4 40 error (invalid witness file) 6.9 3.6 130 310
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.c error (42) 0 wit inspect 850    850    4400   13000 39      0      - - error (invalid witness file) .49 .32 13   39 error (invalid witness file) 6.5 3.4 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--mma8450.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8300   13000 4.1    0      - - error (invalid witness file) .48 .30 9.4 40 error (invalid witness file) 6.7 3.6 140 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--mpu3050.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8200   13000 16      0      - - error (invalid witness file) .65 .42 7.3 41 error (invalid witness file) 6.8 3.6 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--pcap_keys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7800   13000 7.5    0      - - error (invalid witness file) .67 .41 7.7 40 error (invalid witness file) 6.4 3.4 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--pcf50633-input.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8700   14000 10      0      - - error (invalid witness file) .53 .33 9.6 39 error (invalid witness file) 6.6 3.5 140 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--pcspkr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8400   13000 16      0      - - error (invalid witness file) .49 .31 8.8 39 error (invalid witness file) 6.7 3.4 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--rotary_encoder.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6600   14000 27      0      - - error (invalid witness file) .62 .38 11   43 error (invalid witness file) 6.6 3.5 130 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--misc--wm831x-on.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    6900   13000 6.6    0      - - error (invalid witness file) .50 .33 14   40 error (invalid witness file) 6.2 3.3 98 300
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.c error (42) 0 wit inspect 850    850    5900   14000 61      .18   - - error (invalid witness file) .50 .31 11   39 error (invalid witness file) 6.4 3.5 120 300
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.c error (42) 0 wit inspect 850    850    7200   13000 24      0      - - error (invalid witness file) .52 .33 8.8 39 error (invalid witness file) 6.6 3.4 97 310
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.c error (42) 0 wit inspect 850    850    5300   13000 20      0      - - error (invalid witness file) .65 .40 7.7 40 error (invalid witness file) 6.7 3.5 130 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--serio--ct82c710.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7400   13000 22      0      - - error (invalid witness file) .54 .34 10   40 error (invalid witness file) 6.3 3.3 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--serio--parkbd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c out of memory 0 wit inspect 540    540    3900   15000 90      0      - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 6.1 3.2 110 300
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.c error (42) 0 wit inspect 850    850    5600   4500 61      0      - - error (invalid witness file) .66 .41 7.2 40 error (invalid witness file) 6.2 3.3 89 300
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.c error (42) 0 wit inspect 850    850    6800   14000 46      0      - - error (invalid witness file) .56 .35 8.7 40 error (invalid witness file) 7.0 3.7 130 300
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.c error (42) 0 wit inspect 850    850    7300   14000 12      .074  - - error (invalid witness file) .61 .39 9.0 42 error (invalid witness file) 6.3 3.3 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--eeti_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    9000   13000 8.9    0      - - error (invalid witness file) .67 .42 8.6 40 error (invalid witness file) 7.8 4.1 110 310
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.c error (42) 0 wit inspect 850    850    8300   13000 23      .074  - - error (invalid witness file) .53 .33 13   39 error (invalid witness file) 7.9 4.2 85 290
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.c error (42) 0 wit inspect 850    850    7200   14000 12      0      - - error (invalid witness file) .55 .34 10   40 error (invalid witness file) 6.5 3.5 120 320
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.c error (42) 0 wit inspect 850    850    6800   14000 13      0      - - error (invalid witness file) .54 .34 10   39 error (invalid witness file) 6.3 3.4 130 300
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.c error (42) 0 wit inspect 850    850    7100   14000 13      .074  - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.7 3.5 110 300
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.c error (42) 0 wit inspect 850    850    7500   14000 11      0      - - error (invalid witness file) .49 .32 6.2 42 error (invalid witness file) 6.5 3.4 140 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--max11801_ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8100   14000 16      0      - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 6.2 3.3 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--mk712.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    4600   6600 53      0      - - error (invalid witness file) .63 .40 8.3 39 error (invalid witness file) 6.2 3.3 120 300
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.c error (42) 0 wit inspect 850    850    8100   13000 14      0      - - error (invalid witness file) .54 .35 9.7 40 error (invalid witness file) 5.7 3.1 120 290
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.c error (42) 0 wit inspect 850    850    6800   13000 120      .074  - - error (invalid witness file) .62 .41 8.4 40 error (invalid witness file) 6.1 3.2 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--stmpe-ts.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7100   13000 19      11      - - error (invalid witness file) .67 .42 8.5 39 error (invalid witness file) 6.2 3.3 100 300
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.c error (42) 0 wit inspect 850    850    8300   14000 12      0      - - error (invalid witness file) .62 .39 8.5 43 error (invalid witness file) 6.9 3.6 110 300
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.c error (42) 0 wit inspect 850    850    7600   14000 13      0      - - error (invalid witness file) .55 .35 11   42 error (invalid witness file) 6.5 3.4 140 300
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.c error (42) 0 wit inspect 850    850    7200   13000 11      .074  - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.4 3.4 120 300
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.c error (42) 0 wit inspect 850    850    6300   14000 13      0      - - error (invalid witness file) .64 .41 7.1 40 error (invalid witness file) 6.8 3.6 110 310
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.c error (42) 0 wit inspect 850    850    8700   14000 74      .074  - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.3 3.4 140 300
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.c error (42) 0 wit inspect 850    850    6500   14000 11      .074  - - error (invalid witness file) .51 .32 12   41 error (invalid witness file) 7.4 3.9 120 340
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.c error (42) 0 wit inspect 850    850    9000   14000 42      0      - - error (invalid witness file) .60 .36 8.0 40 error (invalid witness file) 7.3 3.9 98 310
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.c error (42) 0 wit inspect 850    850    9800   540 2.7    0      - - error (invalid witness file) .63 .41 9.5 45 error (invalid witness file) 6.3 3.3 120 300
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.c error (42) 0 wit inspect 850    850    8500   14000 14      .074  - - error (invalid witness file) .57 .36 11   41 error (invalid witness file) 6.3 3.3 130 300
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.c error (1) 0 wit inspect 850    850    2800   890 .012  0      - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 7.7 4.0 150 320
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.c error (42) 0 wit inspect 850    850    7800   14000 50      .18   - - error (invalid witness file) .56 .36 9.5 42 error (invalid witness file) 7.2 3.8 150 320
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.c error (42) 0 wit inspect 850    850    7000   14000 8.3    0      - - error (invalid witness file) .58 .38 9.2 39 error (invalid witness file) 6.4 3.4 120 300
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.c error (42) 0 wit inspect 850    850    6800   14000 8.2    .26   - - error (invalid witness file) .48 .31 9.2 39 error (invalid witness file) 6.4 3.4 120 300
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.c error (42) 0 wit inspect 850    850    6500   14000 8.5    0      - - error (invalid witness file) .57 .36 13   45 error (invalid witness file) 6.4 3.4 120 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--dell-led.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c true 2 wit inspect .59 .58 5.8 59 .0082 0      - - exception 7.4  3.9  130   330 true 16   8.8 330 490
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.c error (42) 0 wit inspect 850    850    8400   13000 53      0      - - error (invalid witness file) .52 .34 7.9 40 error (invalid witness file) 7.1 3.7 120 310
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-dac124s085.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8100   13000 31      .23   - - error (invalid witness file) .55 .34 9.2 39 error (invalid witness file) 7.4 3.8 130 320
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.c error (42) 0 wit inspect 850    850    9000   14000 56      0      - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 6.7 3.5 100 290
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.c error (42) 0 wit inspect 850    850    4300   2700 19      0      - - error (invalid witness file) .56 .37 9.4 41 error (invalid witness file) 5.8 3.1 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-pca9633.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7500   13000 37      .074  - - error (invalid witness file) .67 .41 8.3 41 error (invalid witness file) 5.8 3.1 110 290
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--leds--leds-regulator.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    7800   13000 40      0      - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.0 3.2 87 300
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.c error (42) 0 wit inspect 850    850    7700   14000 26      0      - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 8.2 4.3 82 300
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.c error (42) 0 wit inspect 850    850    6400   14000 67      .074  - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 5.8 3.1 110 290
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.c error (42) 0 wit inspect 850    850    6000   14000 42      0      - - error (invalid witness file) .67 .41 8.4 42 error (invalid witness file) 5.8 3.1 120 290
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.c error (42) 0 wit inspect 850    850    7400   13000 9.4    0      - - error (invalid witness file) .65 .40 8.6 39 error (invalid witness file) 6.7 3.5 140 290
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.c error (42) 0 wit inspect 850    850    7300   14000 22      .18   - - error (invalid witness file) .55 .35 9.2 39 error (invalid witness file) 6.1 3.2 130 300
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.c error (42) 0 wit inspect 850    850    6300   14000 .012  0      - - error (invalid witness file) .51 .32 9.3 40 error (invalid witness file) 6.8 3.6 120 300
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.c error (42) 0 wit inspect 850    850    6500   14000 42      0      - - error (invalid witness file) .62 .41 7.8 40 error (invalid witness file) 6.8 3.6 140 310
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.c error (42) 0 wit inspect 850    850    5400   14000 46      13      - - error (invalid witness file) .60 .37 9.4 40 error (invalid witness file) 7.1 3.7 110 300
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--common--tuners--mt20xx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5800   14000 69      .074  - - error (invalid witness file) .69 .44 8.2 42 error (invalid witness file) 6.6 3.5 150 310
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.c error (42) 0 wit inspect 850    850    5500   13000 47      0      - - error (invalid witness file) .47 .31 10   39 error (invalid witness file) 6.0 3.2 110 290
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.c error (42) 0 wit inspect 850    850    7800   14000 56      0      - - error (invalid witness file) .51 .32 9.8 39 error (invalid witness file) 6.6 3.5 120 290
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.c error (42) 0 wit inspect 850    850    3500   14000 .012  0      - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 7.4 3.9 160 320
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.c error (42) 0 wit inspect 850    850    8800   14000 40      0      - - error (invalid witness file) .65 .40 9.1 41 error (invalid witness file) 7.7 4.0 160 320
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.c error (42) 0 wit inspect 850    850    4700   14000 13      0      - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.5 3.4 130 300
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.c error (1) 0 wit inspect 850    850    5200   4800 .0041 0      - - error (invalid witness file) .61 .38 5.6 39 error (invalid witness file) 7.3 3.8 150 310
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.c error (42) 0 wit inspect 850    850    6400   14000 93      .20   - - error (invalid witness file) .60 .38 11   46 error (invalid witness file) 7.1 3.7 130 310
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.c error (42) 0 wit inspect 850    850    5300   14000 .037  0      - - error (invalid witness file) .48 .32 9.7 39 error (invalid witness file) 8.7 4.6 110 310
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.c error (42) 0 wit inspect 850    850    5600   14000 26      0      - - error (invalid witness file) .65 .42 8.6 40 error (invalid witness file) 9.0 4.7 91 320
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.c error (134) 0 wit inspect 33    33    460   13000 .0041 0      - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.8 3.7 130 300
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.c error (134) 0 wit inspect 44    44    540   14000 .012  0      - - error (invalid witness file) .55 .35 11   43 error (invalid witness file) 7.4 3.9 120 310
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.c error (134) 0 wit inspect 130    130    1300   12000 .037  0      - - error (invalid witness file) .62 .41 7.6 40 error (invalid witness file) 7.4 3.9 140 310
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.c error (134) 0 wit inspect 33    33    400   13000 .012  0      - - error (invalid witness file) .67 .42 9.5 42 error (invalid witness file) 7.2 3.8 160 310
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.c error (42) 0 wit inspect 850    850    6700   13000 17      0      - - error (invalid witness file) .57 .35 12   44 error (invalid witness file) 7.5 3.9 140 310
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_main1_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5400   14000 18      0      - - error (invalid witness file) .55 .34 7.0 39 error (invalid witness file) 7.1 3.7 150 310
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-common.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    5100   6700 9.5    0      - - error (invalid witness file) .65 .41 6.2 41 error (invalid witness file) 6.7 3.6 130 300
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.c error (42) 0 wit inspect 850    850    7500   14000 36      0      - - error (invalid witness file) .58 .38 12   41 error (invalid witness file) 8.9 4.6 99 310
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.c error (42) 0 wit inspect 850    850    10000   470 5.6    0      - - error (invalid witness file) .70 .44 8.9 39 error (invalid witness file) 6.2 3.3 120 300
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.c error (134) 0 wit inspect 41    41    540   14000 .012  .074  - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 8.0 4.2 160 320
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.c error (42) 0 wit inspect 850    850    9300   14000 25      0      - - error (invalid witness file) .67 .42 6.9 39 error (invalid witness file) 7.0 3.7 140 310
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_main1_sequence_infinite_withcheck_stateful.cil.out.c error (42) 0 wit inspect 850    850    8200   14000 32      0      - - error (invalid witness file) .49 .34 4.2 40 error (invalid witness file) 7.2 3.8 150 310
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.c error (134) 0 wit inspect 34    34    510   13000 .0041 0      - - error (invalid witness file) .62 .39 10   42 error (invalid witness file) 6.8 3.5 130 310