Tool 2LS 0.7.2-sv-comp19 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:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-06 10:31:50 CET 2018-12-12 19:28:33 CET 2018-12-06 06:59:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-2ls.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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 error (6) 0 --- inspect 3.0   3.0   290 25    .012  0      error (invalid witness file) 0 --- inspect .66 .41 40 0   0   error (2) 0 --- inspect .020 .020 5.7 0   0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0015 .0020 .41 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i error (6) 0 --- inspect 2.6   2.6   260 28    .0082 0      error (invalid witness file) 0 --- inspect .71 .44 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .95 .63 48 0   0   error (invalid witness file) 0 --- inspect .0057 .0069 .41 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i error (6) 0 --- inspect 2.6   2.6   330 21    .012  0      error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .021 .030 5.6 0   0   error (invalid witness file) 0 --- inspect .91 .61 46 0   0   error (invalid witness file) 0 --- inspect .0036 .0048 .52 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i error (6) 0 --- inspect 1.3   1.3   110 10    .0082 0      error (invalid witness file) 0 --- inspect .67 .41 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .98 .64 48 0   0   error (invalid witness file) 0 --- inspect .0022 .0028 .52 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i out of memory 0 --- inspect 98     98     15000 1000    .020  0      error (invalid witness file) 0 --- inspect .70 .43 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .59 47 0   0   error (invalid witness file) 0 --- inspect .0046 .0059 .53 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i error (6) 0 --- inspect 3.0   3.0   120 25    .0082 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .049 .051 5.7 0   0   error (invalid witness file) 0 --- inspect .97 .63 48 0   0   error (invalid witness file) 0 --- inspect .0065 .0084 .41 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i error (6) 0 --- inspect .72  .72  61 5.0  .0082 0      error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .035 .038 5.6 0   0   error (invalid witness file) 0 --- inspect .90 .60 47 0   0   error (invalid witness file) 0 --- inspect .0054 .0077 .53 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i error (6) 0 --- inspect 22     22     1400 140    .012  0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0   error (invalid witness file) 0 --- inspect .0048 .0067 .53 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i out of memory 0 --- inspect 130     130     15000 970    .025  0      error (invalid witness file) 0 --- inspect .72 .44 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .98 .63 47 0   0   error (invalid witness file) 0 --- inspect .0067 .0095 .54 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 (134) 0 --- inspect 1.3   1.3   68 12    .0082 0      error (invalid witness file) 0 --- inspect .71 .44 42 0   0   error (2) 0 --- inspect .026 .027 5.7 0   0   error (invalid witness file) 0 --- inspect .97 .63 47 0   0   error (invalid witness file) 0 --- inspect .0057 .0073 .53 0   0   - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i error (134) 0 --- inspect .47  .47  52 5.1  .0082 0      error (invalid witness file) 0 --- inspect .68 .43 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .99 .67 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0078 .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 .53  .53  54 4.0  .0082 0      error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .98 .64 47 0   0   error (invalid witness file) 0 --- inspect .0059 .0076 .41 0   0   - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i error (134) 0 --- inspect .40  .40  47 3.3  .0082 0      error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .044 .049 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0075 .53 0   0   - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i error (134) 0 --- inspect .42  .42  47 3.7  .0082 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .97 .61 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0019 .40 0   0   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 36     36     420 260    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 3.2   3.2   290 18    .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 40 0   0   error (2) 0 --- inspect .048 .050 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 1.6   1.6   130 19    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 26     26     5400 240    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .025 .027 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect .61  .61  59 5.4  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 4.9   4.9   460 32    .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect .33  .32  39 3.0  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .49 41 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect .63  .63  64 4.3  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect .27  .27  42 2.4  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 2.0   2.0   210 15    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 53     53     880 280    .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0  
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 1.6   1.6   110 13    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect .29  .29  40 3.1  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .043 .043 5.6 0    0  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect 2.8   2.8   110 18    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect 1.3   1.3   86 12    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect .60  .61  45 5.6  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0   error (2) 0 --- inspect .021 .021 5.5 0    0  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect .99  .99  51 10    .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 42 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0  
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect 7.2   7.2   96 56    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 41 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0  
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect .35  .35  43 3.7  .0082 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.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i error (6) 0 --- inspect .98  .98  59 8.9  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect .56  .56  47 4.7  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0  
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect 1.6   1.6   83 12    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .035 .039 5.5 0    0  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i error (134) 0 --- inspect 1.4   1.4   76 10    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 41 0   0   error (2) 0 --- inspect .021 .023 5.6 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 out of memory 0 --- inspect 110     110     15000 830    .025  0      error (invalid witness file) 0 --- inspect .57 .35 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0062 .013  .52 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 error (134) 0 --- inspect .55  .55  52 6.2  .0082 0      error (invalid witness file) 0 --- inspect .63 .37 41 0   0   error (2) 0 --- inspect .024 .026 5.6 0   0   error (invalid witness file) 0 --- inspect .98 .64 47 0   0   error (invalid witness file) 0 --- inspect .0063 .0085 .52 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 error (134) 0 --- inspect 1.5   1.5   75 13    .0082 0      error (invalid witness file) 0 --- inspect .67 .40 41 0   0   error (2) 0 --- inspect .022 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .99 .65 47 0   0   error (invalid witness file) 0 --- inspect .0021 .0027 .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 (134) 0 --- inspect 1.1   1.1   110 8.0  .0082 0      error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .97 .65 49 0   0   error (invalid witness file) 0 --- inspect .0025 .0036 .53 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 error (134) 0 --- inspect 2.7   2.7   250 21    .0082 0      error (invalid witness file) 0 --- inspect .72 .44 40 0   0   error (2) 0 --- inspect .023 .025 5.7 0   0   error (invalid witness file) 0 --- inspect .95 .61 46 0   0   error (invalid witness file) 0 --- inspect .0043 .0049 .39 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 (134) 0 --- inspect 340     340     6100 3900    .012  0      error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .64 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0023 .41 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 error (134) 0 --- inspect .89  .89  68 7.3  .0082 0      error (invalid witness file) 0 --- inspect .72 .44 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0034 .0047 .52 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 error (134) 0 --- inspect 1.1   1.1   84 8.1  .012  0      error (invalid witness file) 0 --- inspect .74 .47 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0   error (invalid witness file) 0 --- inspect .95 .63 47 0   0   error (invalid witness file) 0 --- inspect .0036 .0048 .42 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 (134) 0 --- inspect 1.5   1.5   130 14    .0082 0      error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .99 .64 46 0   0   error (invalid witness file) 0 --- inspect .0060 .010  .49 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 error (134) 0 --- inspect 1.1   1.1   79 9.1  .0082 0      error (invalid witness file) 0 --- inspect .68 .41 42 0   0   error (2) 0 --- inspect .023 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .64 48 0   0   error (invalid witness file) 0 --- inspect .0036 .0051 .54 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 (139) 0 --- inspect 320     320     190 3500    .012  0      error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 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.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 out of memory 0 --- inspect 110     110     15000 830    .025  .0041 error (invalid witness file) 0 --- inspect .77 .47 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .63 48 0   0   error (invalid witness file) 0 --- inspect .0050 .0063 .42 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 out of memory 0 --- inspect 110     110     15000 860    .029  0      error (invalid witness file) 0 --- inspect .85 .51 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .92 .59 47 0   0   error (invalid witness file) 0 --- inspect .0048 .0061 .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 error (134) 0 --- inspect .52  .52  56 4.5  .0082 0      error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0048 .0059 .41 0   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 timeout 0 --- inspect 900     900     15000 10000    .025  0      error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .92 .60 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0025 .41 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 (134) 0 --- inspect 110     110     3000 1100    .0082 0      error (invalid witness file) 0 --- inspect .63 .39 40 0   0   error (2) 0 --- inspect .021 .022 5.8 0   0   error (invalid witness file) 0 --- inspect .95 .63 48 0   0   error (invalid witness file) 0 --- inspect .0023 .0044 .42 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 (134) 0 --- inspect 13     13     1100 97    .0082 0      error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0   error (invalid witness file) 0 --- inspect .0047 .0058 .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 error (134) 0 --- inspect 1.2   1.2   180 10    .0082 0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect 1.0  .67 49 0   0   error (invalid witness file) 0 --- inspect .0051 .0063 .54 0   0   - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i error (134) 0 --- inspect 2.1   2.1   260 18    .0082 0      error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .022 .024 5.7 0   0   error (invalid witness file) 0 --- inspect .95 .61 46 0   0   error (invalid witness file) 0 --- inspect .0018 .0020 .40 0   0   - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.i error (134) 0 --- inspect 560     560     1400 5700    .012  0      error (invalid witness file) 0 --- inspect .74 .45 40 0   0   error (2) 0 --- inspect .021 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .98 .63 48 0   0   error (invalid witness file) 0 --- inspect .0019 .0025 .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 error (134) 0 --- inspect 4.3   4.3   280 37    .012  0      error (invalid witness file) 0 --- inspect .77 .48 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0021 .56 0   0   - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.i error (134) 0 --- inspect 2.0   2.0   220 22    .0082 0      error (invalid witness file) 0 --- inspect .67 .42 41 0   0   error (2) 0 --- inspect .024 .026 5.7 0   0   error (invalid witness file) 0 --- inspect .97 .62 47 0   0   error (invalid witness file) 0 --- inspect .0061 .0083 .52 0   0   - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.i error (134) 0 --- inspect 1.4   1.4   230 16    .0082 0      error (invalid witness file) 0 --- inspect .73 .47 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .62 47 0   0   error (invalid witness file) 0 --- inspect .0054 .0069 .52 0   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 out of memory 0 --- inspect 120     120     15000 920    .025  0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .96 .61 49 0   0   error (invalid witness file) 0 --- inspect .0062 .0081 .53 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 (6) 0 --- inspect 1.8   1.8   150 13    .0082 0      error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect 1.0  .64 48 0   0   error (invalid witness file) 0 --- inspect .0021 .0028 .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 (6) 0 --- inspect 8.1   8.1   700 63    .012  0      error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0045 .0056 .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 error (6) 0 --- inspect .88  .87  61 7.5  .0082 0      error (invalid witness file) 0 --- inspect .63 .38 40 0   0   error (2) 0 --- inspect .050 .053 5.7 0   0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0051 .0066 .53 0   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 (6) 0 --- inspect 29     29     3500 230    .0082 0      error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .97 .63 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0066 .54 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 (6) 0 --- inspect 40     40     5500 350    .0082 0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .97 .62 47 0   0   error (invalid witness file) 0 --- inspect .0052 .0063 .54 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 error (134) 0 --- inspect .30  .30  39 3.3  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0   error (2) 0 --- inspect .030 .033 5.7 0    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 (134) 0 --- inspect .20  .20  35 2.0  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 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--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .31  .31  38 2.9  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 41 0   0   error (2) 0 --- inspect .022 .032 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_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .25  .25  42 2.3  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 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--ata--pata_netcell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .25  .25  41 2.4  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .37 41 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--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .58  .58  80 5.6  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    860    6000 0   0   true 2 --- inspect 13     7.7   470   .62 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 (134) 0 --- inspect .22  .22  39 1.9  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 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--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .18  .18  30 1.9  0      0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 620    600    7000 0   0   true 2 --- inspect 12     7.0   440   .62 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 (134) 0 --- inspect .26  .25  41 1.9  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 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--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 1.5   1.5   130 12    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .41 40 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--block--paride--comm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .34  .34  53 3.9  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .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--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .41  .41  60 3.8  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .021 .033 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 (134) 0 --- inspect .89  .89  79 8.4  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .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--block--paride--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .48  .48  54 4.5  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .49 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--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .22  .22  37 1.8  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .43 41 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--block--paride--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .31  .31  49 2.6  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .38 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--block--paride--friq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .57  .57  74 5.8  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .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--block--paride--frpw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .58  .58  69 5.4  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .34 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--block--paride--kbic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .56  .56  69 6.0  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 41 0   0   error (2) 0 --- inspect .021 .033 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 (134) 0 --- inspect .24  .24  39 1.7  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .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--block--paride--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .48  .48  68 5.3  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .44 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--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 1.3   1.3   130 11    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 41 0   0   error (2) 0 --- inspect .048 .049 5.5 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 (5) 0 --- inspect .82  .82  30 9.3  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .40 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--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .31  .30  44 3.1  .0082 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--char--ramoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .41  .41  54 4.2  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 570    550    7000 0   0   true 2 --- inspect 18     11     540   .62 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 (134) 0 --- inspect 3.6   3.6   540 53    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .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--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .40  .40  54 4.7  0      0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5100 0   0   true 2 --- inspect 11     6.0   350   .62 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 true 2 wit inspect .17  .17  26 1.7  0      0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 580    570    7000 0   0   true 2 --- inspect 9.7   5.8   330   .62 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 (134) 0 --- inspect .42  .42  51 4.4  .0082 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--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .30  .29  36 4.1  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .022 .024 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 error (5) 0 --- inspect 5.0   5.0   120 61    .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .90 .56 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--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .27  .27  35 2.3  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0   error (2) 0 --- inspect .022 .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-tps65912.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .24  .24  31 2.0  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 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--gpio--gpio-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .26  .26  34 2.2  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 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--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .50  .50  49 4.5  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 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--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .31  .31  40 2.8  0      0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 390    370    7000 0   0   true 2 --- inspect 12     6.6   420   .62 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 true 2 wit inspect .29  .28  36 2.8  0      0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 480    470    7000 0   0   true 2 --- inspect 10     6.2   340   .62 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 (134) 0 --- inspect .16  .15  33 1.5  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 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--hid--hid-chicony.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 1.9   1.9   460 25    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 42 0   0   error (2) 0 --- inspect .032 .033 5.5 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 (134) 0 --- inspect .15  .15  32 1.4  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 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-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect .71  .71  160 9.3  0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .37 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--hid--hid-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error (134) 0 --- inspect 2.5   2.5   620 34    0      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .048 .049 5.4 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 (134) 0 --- inspect .33  .33  61 3.7  0      0      - ---