Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 02:16:29 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i false(unreach-call) 1 wit inspect 15     15     4700 170    .85 0      false(unreach-call) 1 wit inspect 25    15    750 0     0     error (7) 0 --- inspect 64     37     970   .66 0   timeout 0 --- inspect 7.8  130    390 .97 0    error (2) 0 --- inspect 6.3    6.3    89    9.9  0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i unknown 0 --- inspect .43  .43  130 5.0  .85 0      error (invalid witness file) 0 --- inspect .65 .39 41 0     0     error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .59 47 0    0    error (invalid witness file) 0 --- inspect .0063 .0084 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i unknown 0 --- inspect .87  .87  210 13    .85 0      error (invalid witness file) 0 --- inspect .73 .44 41 0     0     error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .63 49 0    0    error (invalid witness file) 0 --- inspect .0058 .0074 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i false(unreach-call) 0 wit inspect 24     24     2000 260    1.0  0      true -32 wit inspect 40    27    930 0     0     timeout 0 --- inspect 96     78     3500   2.4  0   unknown 0 --- inspect 10    5.6  340 0    0    error (2) 0 --- inspect 2.2    2.2    33    .48 0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i false(unreach-call) 1 wit inspect 40     40     3000 440    .85 0      false(unreach-call) 1 wit inspect 63    47    1100 0     0     unknown 0 --- inspect 9.0   5.2   320   .62 0   unknown 0 --- inspect 12    6.4  380 0    0    error (1) 0 --- inspect 2.2    2.2    34    .47 0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i out of memory 0 --- inspect 160     160     15000 1900    1.0  0      error (invalid witness file) 0 --- inspect .59 .38 40 0     0     error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .64 48 0    0    error (invalid witness file) 0 --- inspect .0038 .0043 .40 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i true -32 wit inspect 47     47     1000 590    .85 0      timeout 0 wit inspect 93    64    2400 0     0     timeout 0 --- inspect 97     85     4400   2.1  0   unknown 0 --- inspect 1.0  .67 49 0    0    error (1) 0 --- inspect .079  .078  11    0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900     900     6500 9300    1.0  0      error (invalid witness file) 0 --- inspect .62 .38 40 0     0     error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .62 49 0    0    error (invalid witness file) 0 --- inspect .0047 .0059 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i false(unreach-call) 0 wit inspect 6.2   6.2   1300 97    .85 0      timeout 0 wit inspect 98    77    2000 0     0     timeout 0 --- inspect 97     67     3300   1.8  0   unknown 0 --- inspect 16    8.6  530 0    0    error (2) 0 --- inspect 4.7    4.7    70    7.0  .94   - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i false(unreach-call) 1 wit inspect 1.0   1.0   320 11    1.0  0      false(unreach-call) 1 wit inspect 14    8.0  500 0     0     true -32 --- inspect 33     20     1100   .62 0   unknown 0 --- inspect 7.3  4.0  300 0    .34 error (2) 0 --- inspect 1.7    1.7    27    1.9  .29   - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i false(unreach-call) 0 wit inspect 4.9   4.9   250 59    .85 0      timeout 0 wit inspect 98    81    2000 0     0     timeout 0 --- inspect 97     85     4200   1.7  0   unknown 0 --- inspect 6.7  3.7  280 0    0    error (2) 0 --- inspect 1.3    1.3    24    1.1  0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i false(unreach-call) 0 wit inspect 1.1   1.1   140 13    1.0  0      true -32 wit inspect 27    18    610 0     0     true -32 --- inspect 24     13     530   .62 0   unknown 0 --- inspect 6.9  3.8  290 0    0    error (2) 0 --- inspect 1.4    1.3    24    1.2  0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i false(unreach-call) 0 wit inspect 1.4   1.5   130 21    .85 0      timeout 0 wit inspect 97    71    2400 0     0     true -32 --- inspect 22     13     850   .62 0   unknown 0 --- inspect 7.3  4.0  290 0    0    error (2) 0 --- inspect 1.2    1.2    22    .91 .016  - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i false(unreach-call) 0 wit inspect .63  .63  120 8.9  .85 0      timeout 0 wit inspect 98    76    1400 0     0     error (7) 0 --- inspect 27     15     520   .68 0   unknown 0 --- inspect 6.1  3.4  280 0    0    error (2) 0 --- inspect 1.2    1.2    22    .92 0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i out of memory 0 --- inspect 880     880     15000 5900    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .43 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i out of memory 0 --- inspect 62     62     15000 700    .93 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     2200 6300    .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     10000 7500    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     1800 11000    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i unknown 0 --- inspect 19     19     6100 220    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 42 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     1800 8100    .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i true 2 wit inspect 3.5   3.5   230 43    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 680    610    7000 0   0      true 2 --- inspect 49     31     2200   .62 0     
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i true 2 wit inspect .33  .32  39 3.7  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 710    690    7000 0   0      true 2 --- inspect 25     14     490   .66 0     
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     3800 6300    .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .43 42 0   0      error (2) 0 --- inspect .025 .026 5.7 0    0     
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     2300 6600    .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i true 2 wit inspect 89     89     1400 940    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    830    5400 0   0      true 2 --- inspect 130     110     3300   .62 0     
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i false(unreach-call) -16 wit inspect .35  .35  57 4.0  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.4  3.9  300 0   0      true 2 --- inspect 15     8.0   460   .66 0     
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     9400 7000    .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i true 2 wit inspect 640     640     3700 4400    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    740    6500 0   0      true 2 --- inspect 42     26     1500   .62 0     
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i true 2 wit inspect 12     11     240 160    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 620    530    7000 0   0      true 2 --- inspect 22     12     560   .66 0     
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     14000 12000    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0     
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i out of memory 0 --- inspect 360     360     15000 2900    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i timeout 0 --- inspect 900     900     5800 11000    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i out of memory 0 --- inspect 480     480     15000 4400    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0      error (2) 0 --- inspect .026 .028 5.7 0    0     
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i false(unreach-call) -16 wit inspect 1.9   1.9   130 23    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    850    5200 0   0      true 2 --- inspect 23     12     650   .66 0     
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i true 2 wit inspect 150     150     3600 1600    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    610    6200 0   0      true 2 --- inspect 37     22     1100   .62 0     
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i true 2 wit inspect 21     21     570 200    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    650    6100 0   0      true 2 --- inspect 30     17     1100   .62 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 false(unreach-call) 0 wit inspect 62     62     2300 660    .85 0      timeout 0 wit inspect 98    70    2300 0     0     timeout 0 --- inspect 97     73     2900   1.9  0   unknown 0 --- inspect 21    11    880 0    .51 error (2) 0 --- inspect 7.4    7.4    92    15    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 false(unreach-call) 1 wit inspect 7.0   7.0   150 95    1.0  0      false(unreach-call) 1 wit inspect 23    17    610 0     0     true -32 --- inspect 23     13     500   .62 0   unknown 0 --- inspect 8.3  4.5  340 0    0    error (2) 0 --- inspect 1.2    1.2    23    1.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 timeout 0 --- inspect 900     900     6600 14000    1.0  0      error (invalid witness file) 0 --- inspect .62 .39 40 0     0     error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0    0    error (invalid witness file) 0 --- inspect .0017 .0022 .54 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 false(unreach-call) 1 wit inspect .99  .99  170 9.0  .85 0      false(unreach-call) 1 wit inspect 72    66    670 0     0     unknown 0 --- inspect 12     6.5   320   .66 0   exception 0 --- inspect 8.6  4.7  340 0    .31 error (2) 0 --- inspect 2.8    2.8    32    2.7  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 false(unreach-call) 0 wit inspect 2.3   2.3   420 26    .85 0      timeout 0 wit inspect 95    84    2400 0     0     unknown 0 --- inspect 8.6   4.8   450   .61 0   unknown 0 --- inspect 12    6.8  480 0    0    error (2) 0 --- inspect 5.4    5.4    62    8.5  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 timeout 0 --- inspect 900     900     330 12000    .86 0      error (invalid witness file) 0 --- inspect .66 .41 40 0     0     error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .93 .60 48 0    0    error (invalid witness file) 0 --- inspect .0052 .0064 .52 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 unknown 0 --- inspect .48  .48  120 6.5  .85 0      error (invalid witness file) 0 --- inspect .64 .40 41 0     0     error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 48 0    0    error (invalid witness file) 0 --- inspect .0052 .0069 .54 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--vivi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unknown 0 --- inspect .59  .59  140 5.5  .85 0      error (invalid witness file) 0 --- inspect .66 .40 41 0     0     error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 48 0    0    error (invalid witness file) 0 --- inspect .0017 .0023 .54 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 unknown 0 --- inspect .89  .89  150 11    .85 0      error (invalid witness file) 0 --- inspect .64 .39 40 0     0     error (2) 0 --- inspect .022 .024 5.8 0    0   error (invalid witness file) 0 --- inspect .92 .59 47 0    0    error (invalid witness file) 0 --- inspect .0046 .0057 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(unreach-call) 1 wit inspect 2.4   2.4   140 27    .85 0      false(unreach-call) 1 wit inspect 14    7.8  500 0     0     true -32 --- inspect 28     17     710   .62 0   unknown 0 --- inspect 7.7  4.2  300 0    0    error (2) 0 --- inspect 1.7    1.7    27    1.9  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 false(unreach-call) 1 wit inspect .65  .65  94 6.9  1.0  0      false(unreach-call) 1 wit inspect 13    7.6  450 0     0     true -32 --- inspect 30     17     650   .62 0   unknown 0 --- inspect 8.4  4.6  310 0    0    error (2) 0 --- inspect 1.8    1.8    28    2.1  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 timeout 0 --- inspect 900     900     1700 12000    .86 0      error (invalid witness file) 0 --- inspect .67 .42 40 0     0     error (2) 0 --- inspect .023 .024 5.5 0    0   error (invalid witness file) 0 --- inspect 1.2  .75 48 0    0    error (invalid witness file) 0 --- inspect .0018 .0025 .53 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 false(unreach-call) 0 wit inspect 1.5   1.5   220 15    .85 0      timeout 0 wit inspect 95    87    1100 0     0     timeout 0 --- inspect 97     75     1900   2.2  0   unknown 0 --- inspect 9.8  5.4  350 0    .16 error (2) 0 --- inspect 3.3    3.3    42    2.4  .63   - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(unreach-call) 1 wit inspect .34  .34  58 4.6  1.0  0      false(unreach-call) 1 wit inspect 9.6  5.9  310 0     0     true -32 --- inspect 22     13     540   .62 0   unknown 0 --- inspect 6.0  3.4  280 0    .16 error (2) 0 --- inspect 1.3    1.3    24    1.2  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 false(unreach-call) 1 wit inspect 1.2   1.2   210 12    .85 0      false(unreach-call) 1 wit inspect 68    60    1300 0     0     timeout 0 --- inspect 96     78     3200   1.2  0   exception 0 --- inspect 9.5  5.2  330 0    0    error (2) 0 --- inspect 3.0    3.0    39    4.3  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 false(unreach-call) 1 wit inspect 7.2   7.2   310 85    .85 0      false(unreach-call) 1 wit inspect 16    10    560 0     0     timeout 0 --- inspect 97     66     1400   1.4  0   unknown 0 --- inspect 11    6.1  360 0    .50 error (2) 0 --- inspect 2.8    2.8    38    1.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 true -32 wit inspect 190     190     910 1600    .85 0      timeout 0 wit inspect 97    71    2200 0     0     timeout 0 --- inspect 96     80     3600   1.6  0   unknown 0 --- inspect .99 .64 48 0    0    error (1) 0 --- inspect .080  .085  11    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 unknown 0 --- inspect .42  .42  110 4.9  0    0      error (invalid witness file) 0 --- inspect .70 .43 40 0     0     error (2) 0 --- inspect .032 .033 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .64 47 0    0    error (invalid witness file) 0 --- inspect .0045 .0059 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i unknown 0 --- inspect .73  .73  180 7.7  0    0      error (invalid witness file) 0 --- inspect .61 .37 42 0     0     error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .62 49 0    0    error (invalid witness file) 0 --- inspect .0058 .0073 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.i unknown 0 --- inspect .81  .81  200 12    0    0      error (invalid witness file) 0 --- inspect .62 .38 40 0     0     error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0    0    error (invalid witness file) 0 --- inspect .0022 .0030 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.i unknown 0 --- inspect 1.4   1.4   250 15    .85 0      error (invalid witness file) 0 --- inspect .64 .39 40 0     0     error (2) 0 --- inspect .025 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .60 47 0    0    error (invalid witness file) 0 --- inspect .0051 .0070 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.i unknown 0 --- inspect .61  .61  150 7.4  0    0      error (invalid witness file) 0 --- inspect .60 .38 41 0     0     error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .74 47 0    0    error (invalid witness file) 0 --- inspect .0044 .0054 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.i unknown 0 --- inspect 1.2   1.2   200 12    .85 0      error (invalid witness file) 0 --- inspect .76 .46 42 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .90 .61 46 0    0    error (invalid witness file) 0 --- inspect .0049 .0064 .53 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 timeout 0 --- inspect 900     900     770 12000    .86 0      error (invalid witness file) 0 --- inspect .63 .39 41 0     0     error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .90 .58 46 0    0    error (invalid witness file) 0 --- inspect .0059 .0084 .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 timeout 0 --- inspect 900     900     2800 11000    .86 0      error (invalid witness file) 0 --- inspect .63 .40 41 0     0     error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 49 0    0    error (invalid witness file) 0 --- inspect .0048 .0062 .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 timeout 0 --- inspect 900     900     3000 6700    .86 0      error (invalid witness file) 0 --- inspect .67 .42 41 0     0     error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0    0    error (invalid witness file) 0 --- inspect .0048 .0058 .52 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 true -32 wit inspect 54     54     1700 600    .85 0      timeout 0 wit inspect 93    70    2900 0     0     timeout 0 --- inspect 97     74     970   2.2  0   unknown 0 --- inspect 1.0  .67 50 0    0    error (1) 0 --- inspect .080  .081  11    0    .21   - --- 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 out of memory 0 --- inspect 380     380     15000 2900    .85 0      error (invalid witness file) 0 --- inspect .67 .40 40 0     0     error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .93 .59 47 0    0    error (invalid witness file) 0 --- inspect .0021 .0028 .41 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 out of memory 0 --- inspect 130     130     15000 1400    .86 0      error (invalid witness file) 0 --- inspect .68 .41 41 0     0     error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .61 47 0    0    error (invalid witness file) 0 --- inspect .0049 .0059 .53 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 true 2 wit inspect .42  .42  38 5.1  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 750    740    7000 0   0      true 2 --- inspect 20     13     920   .66 0     
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .36  .36  36 4.3  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 890    850    7000 0   0      true 2 --- inspect 12     7.1   390   .66 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 true 2 wit inspect .46  .46  37 5.2  .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 690    670    7000 0   0      true 2 --- inspect 19     12     720   .66 0     
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .74  .74  53 9.6  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5600 0   0      true 2 --- inspect 14     7.8   450   .66 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 true 2 wit inspect .30  .30  40 3.7  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6700 0   0      true 2 --- inspect 12     6.8   410   .66 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 .47  .47  32 6.1  .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    850    6000 0   0      true 2 --- inspect 15     8.4   480   .66 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 true 2 wit inspect .28  .28  37 4.2  .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6700 0   0      true 2 --- inspect 22     15     1300   .66 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 .22  .22  31 2.6  .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 590    580    7000 0   0      true 2 --- inspect 15     8.0   450   .66 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 true 2 wit inspect 3.9   3.9   92 44    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 520    480    7000 0   0      true 2 --- inspect 20     12     470   .66 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 true 2 wit inspect 800     800     2200 5500    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    870    6500 0   0      true 2 --- inspect 26     15     570   .66 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 true 2 wit inspect 13     13     190 130    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 620    520    7000 0   0      true 2 --- inspect 23     14     540   .66 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 true 2 wit inspect 19     19     180 170    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 630    540    7000 0   0      true 2 --- inspect 25     15     530   .62 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 true 2 wit inspect 150     150     690 1800    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 640    580    7000 0   0      true 2 --- inspect 27     15     570   .66 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 true 2 wit inspect 70     70     580 520    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    640    6700 0   0      true 2 --- inspect 22     13     530   .62 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 true 2 wit inspect 2.5   2.5   68 37    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5800 0   0      true 2 --- inspect 18     9.9   430   .66 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 true 2 wit inspect 7.5   7.5   140 90    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 670    640    7000 0   0      true 2 --- inspect 22     13     550   .62 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 true 2 wit inspect 90     90     400 990    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 850    740    7000 0   0      true 2 --- inspect 28     16     600   .62 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 true 2 wit inspect 70     70     400 510    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 670    570    7000 0   0      true 2 --- inspect 34     20     540   .66 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 true 2 wit inspect 72     72     520 590    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    700    6800 0   0      true 2 --- inspect 27     16     560   .66 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 true 2 wit inspect 2.8   2.8   72 33    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 840    810    7000 0   0      true 2 --- inspect 16     9.1   430   .66 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 true 2 wit inspect 21     21     170 200    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 720    700    7000 0   0      true 2 --- inspect 30     17     570   .62 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 true 2 wit inspect 340     340     950 2300    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5500 0   0      true 2 --- inspect 36     21     830   .66 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 true 2 wit inspect .50  .50  34 5.5  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3600 0   0      true 2 --- inspect 12     6.8   340   .66 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 true 2 wit inspect .64  .64  53 8.0  .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4300 0   0      true 2 --- inspect 38     24     590   .66 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 .31  .32  35 3.8  .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 580    560    7000 0   0      true 2 --- inspect 20     12     520   .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 true 2 wit inspect 1.7   1.7   89 18    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5800 0   0      true 2 --- inspect 17     9.2   470   .66 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 .23  .23  29 3.1  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    4800 0   0      true 2 --- inspect 13     7.4   350   .66 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 .11  .11  28 1.5  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 640    630    7000 0   0      true 2 --- inspect 9.2   5.2   320   .66 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 true 2 wit inspect 2.0   2.0   75 29    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 790    760    7000 0   0      true 2 --- inspect 32     20     610   .66 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 true 2 wit inspect .49  .49  37 6.1  .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5600 0   0      true 2 --- inspect 19     12     440   .66 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 true 2 wit inspect .31  .31  35 4.4  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5900 0   0      true 2 --- inspect 15     10     400   .66 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 true 2 wit inspect .50  .50  36 5.5  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4900 0   0      true 2 --- inspect 18     12     410   .66 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 true 2 wit inspect .49  .49  33 6.6  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 400    380    7000 0   0      true 2 --- inspect 14     8.6   420   .66 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 true 2 wit inspect 1.4   1.4   53 20    1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    870    5900 0   0      true 2 --- inspect 20     12     500   .66 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 true 2 wit inspect 3.7   3.7   95 51    .85 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4800 0   0      true 2 --- inspect 22     13     570   .66 0     
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect .20  .20  38 3.1  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 480    460    7000 0   0      true 2 --- inspect 14     7.8   420   .66 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 .18  .18  34 2.4  1.0  .0041 - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 570    560    7000 0   0      true 2 --- inspect 12     6.6   330   .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 true 2 wit inspect .31  .31  35 4.7  1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 460    450    7000 0   0      true 2 --- inspect 14     7.6   340   .66 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 true 2 wit inspect 3.1   3.1   170 42    1.0  0      - ---