Tool CPAchecker 1.7-svn 29794 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* [apollon033; apollon040; apollon065; apollon082; apollon124; apollon167] apollon* [apollon003; apollon016; apollon052] 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:41:10 CET 2018-12-05 15:42:34 CET 2018-12-05 19:29:29 CET 2018-12-05 19:51:06 CET 2018-12-12 19:31:17 CET 2018-12-05 12:23:59 CET 2018-12-05 16:20:39 CET
Run set cpa-bam-bnb.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety
Options -svcomp19-bam-bnb -disable-java-assertions -heap 10000m -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/cpa-bam-bnb.2018-12-04_2241.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-bam-bnb.2018-12-04_2241.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/cpa-bam-bnb.2018-12-04_2241.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-bam-bnb.2018-12-04_2241.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cpa-bam-bnb.2018-12-04_2241.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-bam-bnb.2018-12-04_2241.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 53   17   1700 470 .020 0      false(unreach-call) 1 wit inspect 20    11    670 0     0      error (7) 0 --- inspect 67     39     990   .66  0      timeout 0 --- inspect 7.5  130    380 .90   0     error (2) 0 --- inspect 6.6    6.6    89    9.9  0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i false(unreach-call) 1 wit inspect 26   6.8 720 220 .17  0      false(unreach-call) 1 wit inspect 15    8.7  550 0     0      error (7) 0 --- inspect 71     49     740   .71  0      unknown 0 --- inspect 7.5  4.1  290 0      0     error (2) 0 --- inspect 1.4    1.5    27    1.2  .20   - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i error 0 wit inspect 32   8.2 1100 270 .078 0      timeout 0 wit inspect 95    83    1600 0     0      timeout 0 --- inspect 96     54     2100   .75  0      unknown 0 --- inspect 1.4  .83 65 0      0     error (1) 0 --- inspect .22   .22   27    0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900   600   8500 9000 0     0      error (invalid witness file) 0 --- inspect .75 .46 40 0     0      error (2) 0 --- inspect .021 .022 5.6 0     0      error (invalid witness file) 0 --- inspect .94 .60 48 0      0     error (invalid witness file) 0 --- inspect .0050 .0062 .54 0    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 100   44   3600 910 .057 0      false(unreach-call) 1 wit inspect 41    33    720 0     0      unknown 0 --- inspect 8.9   5.2   330   .66  0      unknown 0 --- inspect 11    5.9  340 0      0     error (2) 0 --- inspect 2.8    2.8    41    3.6  .074  - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900   620   8200 11000 0     0      error (invalid witness file) 0 --- inspect .60 .38 41 0     0      error (2) 0 --- inspect .021 .021 5.6 0     0      error (invalid witness file) 0 --- inspect .92 .58 48 0      0     error (invalid witness file) 0 --- inspect .0018 .0033 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900   810   4500 11000 0     0      error (invalid witness file) 0 --- inspect .70 .43 40 0     0      error (2) 0 --- inspect .024 .024 5.6 0     0      error (invalid witness file) 0 --- inspect .93 .63 48 0      0     error (invalid witness file) 0 --- inspect .0060 .0092 .52 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   220   11000 5300 0     0      error (invalid witness file) 0 --- inspect .60 .37 43 0     0      error (2) 0 --- inspect .021 .023 5.7 0     0      error (invalid witness file) 0 --- inspect .93 .60 47 0      0     error (invalid witness file) 0 --- inspect .0056 .0072 .52 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 39   14   1100 340 .033 0      timeout 0 wit inspect 96    83    1000 0     0      timeout 0 --- inspect 97     69     3700   .82  .36   unknown 0 --- inspect 14    7.6  480 0      0     error (2) 0 --- inspect 4.9    4.9    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 timeout 0 wit inspect 900   690   7600 11000 0     0      unknown 0 wit inspect 19    11    570 .066 .057  timeout 0 --- inspect 97     66     1400   1.5   0      unknown 0 --- inspect 1.3  .81 63 0      0     error (1) 0 --- inspect .15   .15   20    0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900   330   11000 7200 0     0      error (invalid witness file) 0 --- inspect .74 .45 40 0     0      error (2) 0 --- inspect .021 .022 5.6 0     0      error (invalid witness file) 0 --- inspect .91 .58 47 0      0     error (invalid witness file) 0 --- inspect .0054 .0069 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900   720   7500 9900 0     0      error (invalid witness file) 0 --- inspect .71 .43 40 0     0      error (2) 0 --- inspect .020 .021 5.6 0     0      error (invalid witness file) 0 --- inspect .94 .62 47 0      0     error (invalid witness file) 0 --- inspect .0018 .0022 .53 0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 910   480   11000 7800 0     0      error (invalid witness file) 0 --- inspect .74 .45 40 0     0      error (2) 0 --- inspect .021 .021 5.6 0     0      error (invalid witness file) 0 --- inspect .91 .59 47 0      0     error (invalid witness file) 0 --- inspect .0016 .0020 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 910   400   11000 7400 0     0      error (invalid witness file) 0 --- inspect .72 .44 40 0     0      error (2) 0 --- inspect .036 .036 5.5 0     0      error (invalid witness file) 0 --- inspect .92 .61 47 0      0     error (invalid witness file) 0 --- inspect .0046 .0056 .52 0    0      - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i true 2 wit inspect 18   4.5 510 140 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    870    3800 0   0      true 2 --- inspect 33     19     900   .62 0     
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i true 1 wit inspect 27   7.0 880 240 0     0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 45    25    1300 0   0      error (7) 0 --- inspect 64     37     960   .66 0     
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i true 2 wit inspect 12   3.5 470 95 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    860    2800 0   0      true 2 --- inspect 25     15     680   .62 0     
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i true 2 wit inspect 12   3.2 460 100 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    850    6400 0   0      true 2 --- inspect 31     18     1100   .66 0     
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i true 2 wit inspect 19   5.0 640 150 0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 --- inspect 7.0  3.7  300 0   0      true 2 --- inspect 67     53     3700   .62 0     
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i true 1 wit inspect 37   9.9 1500 320 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    690    6500 0   0      timeout 0 --- inspect 960     910     5600   1.6  0     
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i true 2 wit inspect 8.3 2.7 330 73 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    610    6000 0   0      true 2 --- inspect 17     9.2   440   .66 0     
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i true 2 wit inspect 15   4.0 510 130 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 670    590    7000 0   0      true 2 --- inspect 43     28     2200   .61 0     
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i true 2 wit inspect 11   3.1 460 83 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 690    680    7000 0   0      true 2 --- inspect 21     12     550   .66 0     
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i true 2 wit inspect 15   4.1 500 130 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    640    6000 0   0      true 2 --- inspect 28     15     720   .66 0     
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i true 2 wit inspect 25   6.3 820 200 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    710    6400 0   0      true 2 --- inspect 40     25     1400   .66 0     
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i true 2 wit inspect 13   3.5 360 110 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    830    5800 0   0      true 2 --- inspect 120     110     3400   .62 0     
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i true 2 wit inspect 12   3.4 480 110 0     0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 15    9.4  570 0   0      true 2 --- inspect 55     31     900   .62 0     
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i true 1 wit inspect 12   3.3 470 95 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    590    5800 0   0      unknown 0 --- inspect 8.3   4.7   300   .66 0     
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i true 2 wit inspect 18   4.6 520 140 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    720    6500 0   0      true 2 --- inspect 44     27     1600   .66 0     
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i true 2 wit inspect 8.9 2.9 390 82 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 660    550    7000 0   0      true 2 --- inspect 22     12     550   .66 0     
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i true 2 wit inspect 13   3.7 490 110 0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 --- inspect 7.5  4.0  310 0   0      true 2 --- inspect 23     13     650   .66 0     
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i true 1 wit inspect 19   4.9 650 170 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    740    6800 0   0      error (7) 0 --- inspect 16     9.1   310   .75 0     
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i true 2 wit inspect 52   23   2600 500 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5600 0   0      true 2 --- inspect 58     35     900   .62 0     
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i true 2 wit inspect 22   5.7 680 180 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    840    4300 0   0      true 2 --- inspect 85     54     1700   .62 0     
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i true 1 wit inspect 18   4.9 580 160 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3000 0   0      timeout 0 --- inspect 960     930     5400   .71 0     
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i true 2 wit inspect 17   4.5 540 150 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    610    6100 0   0      true 2 --- inspect 38     23     1200   .66 0     
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i true 2 wit inspect 13   3.6 470 100 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    610    6100 0   0      true 2 --- inspect 32     18     1100   .66 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) 1 wit inspect 37   10   1500 330 .074 0      false(unreach-call) 1 wit inspect 54    40    1400 0     0      timeout 0 --- inspect 97     72     3100   .99  0      unknown 0 --- inspect 16    8.8  650 0      0     error (2) 0 --- inspect 8.4    8.4    93    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 error 0 wit inspect 31   9.9 1100 280 0     0      unknown 0 wit inspect 27    17    910 0     0      error (7) 0 --- inspect 86     48     2100   .71  0      unknown 0 --- inspect 1.2  .75 52 0      0     error (1) 0 --- inspect .10   .10   13    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 0 wit inspect 58   15   1900 440 0     0      unknown 0 wit inspect 53    40    1100 .078 0      timeout 0 --- inspect 98     62     1200   .70  0      unknown 0 --- inspect 1.3  .78 57 0      0     error (1) 0 --- inspect .14   .14   17    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 18   5.7 660 140 .033 0      false(unreach-call) 1 wit inspect 77    71    680 0     0      unknown 0 --- inspect 9.3   5.2   310   .62  0      exception 0 --- inspect 8.3  4.6  340 0      .32  error (2) 0 --- inspect 3.0    3.0    33    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 23   6.3 840 180 .025 0      timeout 0 wit inspect 95    84    2700 0     0      unknown 0 --- inspect 8.1   4.7   430   .61  0      unknown 0 --- inspect 12    6.3  500 0      0     error (2) 0 --- inspect 5.7    5.7    62    8.0  0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 wit inspect 35   8.6 930 280 .070 0      timeout 0 --- inspect 93    58    3400 0     0      timeout 0 --- inspect 96     78     3400   1.7   0      unknown 0 --- inspect 1.5  .90 68 0      0     error (1) 0 --- inspect .24   .24   30    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 false(unreach-call) 1 wit inspect 14   3.7 510 120 .049 0      false(unreach-call) 1 wit inspect 15    8.4  480 0     0      timeout 0 --- inspect 97     86     3400   1.0   0      unknown 0 --- inspect 7.0  3.8  290 0      0     error (2) 0 --- inspect 1.7    1.7    27    1.6  .29   - --- 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 0 wit inspect 31   8.1 1000 240 0     0      timeout 0 wit inspect 94    86    1900 0     0      timeout 0 --- inspect 97     82     2500   .64  3.8    unknown 0 --- inspect 1.2  .75 58 0      0     error (1) 0 --- inspect .17   .16   18    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 false(unreach-call) 1 wit inspect 13   3.7 530 110 .025 0      false(unreach-call) 1 wit inspect 13    8.2  360 0     0      timeout 0 --- inspect 97     71     910   .72  0      exception 0 --- inspect 8.0  4.4  320 0      .32  error (2) 0 --- inspect 2.5    2.5    32    2.6  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 20   5.0 620 160 .045 0      false(unreach-call) 1 wit inspect 14    7.6  500 0     0      timeout 0 --- inspect 96     76     1100   .63  0      unknown 0 --- inspect 7.3  4.1  290 0      0     error (2) 0 --- inspect 1.9    1.9    28    1.6  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 14   3.9 520 120 .041 0      false(unreach-call) 1 wit inspect 16    8.9  460 0     0      timeout 0 --- inspect 97     61     1400   1.1   0      unknown 0 --- inspect 7.4  4.0  310 0      0     error (2) 0 --- inspect 1.9    1.9    29    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 error 0 wit inspect 42   12   1400 370 .082 0      timeout (error (invalid witness file)) 0 --- inspect 93    59    3400 0     0      timeout 0 --- inspect 97     67     2000   .89  0      unknown 0 --- inspect 2.0  1.1  96 0      0     error (1) 0 --- inspect .64   .64   72    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 19   5.5 570 140 .020 0      timeout 0 wit inspect 95    86    1000 0     0      timeout 0 --- inspect 98     75     1900   .82  0      unknown 0 --- inspect 11    5.8  340 0      0     error (2) 0 --- inspect 3.5    3.5    42    4.6  0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(unreach-call) 1 wit inspect 9.8 3.0 510 83 .020 0      false(unreach-call) 1 wit inspect 11    6.6  310 0     0      unknown 0 --- inspect 57     37     810   .71  0      unknown 0 --- inspect 6.3  3.6  280 0      .48  error (2) 0 --- inspect 1.4    1.4    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 17   4.4 570 140 .025 .0041 false(unreach-call) 1 wit inspect 61    54    1200 0     0      timeout 0 --- inspect 97     82     4000   1.6   0      exception 0 --- inspect 9.9  5.4  330 0      .16  error (2) 0 --- inspect 3.2    3.2    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 20   5.2 610 160 .037 0      false(unreach-call) 1 wit inspect 19    11    560 0     0      timeout 0 --- inspect 97     65     1500   1.5   0      unknown 0 --- inspect 9.7  5.3  330 0      0     error (2) 0 --- inspect 3.1    3.1    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 timeout 0 --- inspect 900   700   6200 11000 0     0      error (invalid witness file) 0 --- inspect .61 .37 41 0     0      error (2) 0 --- inspect .021 .022 5.6 0     0      error (invalid witness file) 0 --- inspect .94 .60 48 0      0     error (invalid witness file) 0 --- inspect .0043 .0056 .53 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 (parsing failed) 0 --- inspect 9.7 2.8 720 83 0     0      error (invalid witness file) 0 --- inspect .58 .36 40 0     0      error (2) 0 --- inspect .026 .026 5.6 0     0      error (invalid witness file) 0 --- inspect .90 .58 46 0      0     error (invalid witness file) 0 --- inspect .0055 .0061 .39 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i error 0 wit inspect 44   11   2300 410 .041 0      timeout 0 wit inspect 95    73    2400 0     0      error (7) 0 --- inspect 19     11     620   .70  0      unknown 0 --- inspect 1.6  .94 78 0      0     error (1) 0 --- inspect .39   .39   47    0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.i error 0 wit inspect 51   14   2800 400 0     0      timeout 0 --- inspect 93    60    3000 0     0      error (7) 0 --- inspect 24     13     650   .70  0      unknown 0 --- inspect 2.0  1.1  90 0      0     error (1) 0 --- inspect .59   .59   65    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 0 wit inspect 42   11   2000 330 .033 0      timeout 0 wit inspect 94    71    2300 0     0      error (7) 0 --- inspect 18     9.9   600   .66  0      unknown 0 --- inspect 1.8  1.0  79 0      0     error (1) 0 --- inspect .41   .41   48    0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.i false(unreach-call) 0 wit inspect 36   9.3 2200 300 .012 0      timeout 0 wit inspect 94    80    2100 0     0      error (7) 0 --- inspect 16     8.8   470   .30  0      timeout 0 --- inspect 7.6  130    440 .85   0     error (1) 0 --- inspect .82   .82   23    1.4  0      - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.i false(unreach-call) 1 wit inspect 30   8.0 1600 240 .016 0      false(unreach-call) 1 wit inspect 84    70    1700 0     0      error (7) 0 --- inspect 15     8.6   490   .73  0      timeout 0 --- inspect 7.8  130    440 0      0     error (1) 0 --- inspect .82   .83   23    1.6  0      - --- inspect - --- inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--misc--sgi-xp--xpc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i error 0 wit inspect 49   12   1200 360 .12  0      timeout 0 --- inspect 97    59    3900 0     0      timeout 0 --- inspect 97     78     1700   1.6   0      unknown 0 --- inspect 1.5  .92 70 0      0     error (1) 0 --- inspect .28   .28   33    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 false(unreach-call) 1 wit inspect 32   7.7 1000 250 .066 0      false(unreach-call) 1 wit inspect 11    5.7  360 0     0      error (7) 0 --- inspect 77     53     1000   .68  0      unknown 0 --- inspect 7.8  4.3  310 0      0     error (2) 0 --- inspect 2.0    2.1    30    2.5  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   630   8200 11000 0     0      error (invalid witness file) 0 --- inspect .75 .45 40 0     0      error (2) 0 --- inspect .026 .027 5.6 0     0      error (invalid witness file) 0 --- inspect .93 .61 48 0      0     error (invalid witness file) 0 --- inspect .0032 .0045 .54 0    0      - --- inspect - --- inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(unreach-call) 1 wit inspect 31   10   830 270 .14  0      false(unreach-call) 1 wit inspect 13    7.3  530 0     0      error (7) 0 --- inspect 71     53     730   .68  0      unknown 0 --- inspect 7.0  3.9  290 0      0     error (2) 0 --- inspect 1.5    1.5    26    1.2  0      - --- inspect - --- inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--usb--gadget--mv_udc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i error 0 wit inspect 32   7.9 960 270 .10  0      timeout 0 wit inspect 94    58    3200 0     0      timeout 0 --- inspect 97     64     1200   1.3   .0082 unknown 0 --- inspect 1.4  .86 64 0      0     error (1) 0 --- inspect .20   .20   23    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 false(unreach-call) 1 wit inspect 27   6.5 860 210 .057 0      false(unreach-call) 1 wit inspect 14    7.4  410 0     0      true -32 --- inspect 51     36     910   .62  0      unknown 0 --- inspect 8.5  4.7  320 0      0     error (2) 0 --- inspect 2.4    2.4    31    2.4  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 6.0 2.1 300 50 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 700    690    7000 0   0      true 2 --- inspect 23     14     990   .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 6.3 2.2 300 57 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 870    830    7000 0   0      true 2 --- inspect 13     7.3   400   .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 6.2 2.2 300 58 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 680    660    7000 0   0      true 2 --- inspect 18     11     730   .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 6.6 2.2 310 61 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    880    5700 0   0      true 2 --- inspect 12     7.2   430   .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 6.2 2.1 320 54 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6900 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 6.5 2.3 290 56 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    850    5700 0   0      true 2 --- inspect 14     7.6   460   .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 6.1 2.2 300 56 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 810    800    7000 0   0      true 2 --- inspect 22     14     1600   .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 5.0 1.9 290 50 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 650    630    7000 0   0      true 2 --- inspect 13     7.4   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 8.3 2.6 350 71 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 490    460    7000 0   0      true 2 --- inspect 19     11     490   .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 15   4.1 490 130 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 880    840    7000 0   0      true 2 --- inspect 32     19     730   .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 11   3.2 460 84 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 550    470    7000 0   0      true 2 --- inspect 21     13     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 12   3.4 470 97 0     .0041 - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 630    550    7000 0   0      true 2 --- inspect 26     15     550   .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 13   3.7 470 110 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 750    670    7000 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--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect 11   3.3 470 96 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    620    6700 0   0      true 2 --- inspect 21     13     540   .66 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 7.1 2.4 310 66 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5800 0   0      true 2 --- inspect 14     8.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--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect 9.8 2.9 410 84 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 650    620    7000 0   0      true 2 --- inspect 22     13     480   .66 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 16   4.2 490 130 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 720    630    7000 0   0      true 2 --- inspect 25     15     660   .66 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 15   4.0 480 120 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 600    500    7000 0   0      true 2 --- inspect 30     18     560   .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 15   3.9 480 120 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    670    6800 0   0      true 2 --- inspect 27     16     570   .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 7.8 2.5 330 59 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 700    670    7000 0   0      true 2 --- inspect 15     8.5   430   .62 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 14   3.8 500 110 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 650    630    7000 0   0      true 2 --- inspect 24     14     560   .66 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 24   7.0 730 200 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5700 0   0      true 2 --- inspect 39     23     840   .62 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 5.4 2.0 290 55 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3800 0   0      true 2 --- inspect 11     6.4   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 7.6 2.4 320 64 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4600 0   0      true 2 --- inspect 28     19     740   .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 5.7 2.1 290 54 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 520    500    7000 0   0      true 2 --- inspect 17     10     530   .66 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 7.5 2.5 340 61 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6200 0   0      true 2 --- inspect 15     8.2   470   .62 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 5.1 2.0 290 45 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    4900 0   0      true 2 --- inspect 11     5.9   360   .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 4.4 1.7 280 36 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 530    520    7000 0   0      true 2 --- inspect 9.2   5.3   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 9.4 2.8 400 83 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 800    780    7000 0   0      true 2 --- inspect 28     18     690   .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 5.9 2.1 290 53 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5600 0   0      true 2 --- inspect 18     12     440   .62 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 5.4 2.0 290 53 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5900 0   0      true 2 --- inspect 19     12     420   .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 6.2 2.2 290 54 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5200 0   0      true 2 --- inspect 20     13     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 5.5 2.0 290 47 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 370    350    7000 0   0      true 2 --- inspect 14     8.5   430   .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 6.4 2.2 290 57 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    880    6100 0   0      true 2 --- inspect 19     11     510   .62 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 8.5 2.7 350 82 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5000 0   0      true 2 --- inspect 18     11     560   .66 0     
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect 5.2 2.0 290 47 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 420    400    7000 0   0      true 2 --- inspect 11     6.4   430   .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 5.3 2.0 290 43 0     0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 490    480    7000 0   0      true 2 --- inspect 10     5.8   330   .66 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 5.5 2.0 290 46 0     0      - ---