Tool VeriAbs 1.3.10 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-10 16:50:17 CET 2018-12-10 20:34:10 CET 2018-12-10 21:22:10 CET 2018-12-10 21:27:56 CET 2018-12-12 21:52:30 CET 2018-12-10 19:33:41 CET 2018-12-10 20:40:20 CET
Run set veriabs.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety
Options -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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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 28   870 580 8.7  .0041 false(unreach-call) 1 wit inspect 24    14    690 0   0    error (7) 0 --- inspect 62     36     1000   .73 0    timeout 0 --- inspect 7.9  130    380 .070  0      error (2) 0 --- inspect 6.3    6.3    90    9.9  0     - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900 880   1900 7700 1.9  0      error (invalid witness file) 0 --- inspect .82 .50 42 0   0    error (2) 0 --- inspect .022 .023 5.6 0    0    error (invalid witness file) 0 --- inspect .92 .60 48 0      0      error (invalid witness file) 0 --- inspect .0017 .0021 .53 0    0     - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900 880   1200 8100 2.4  0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0    error (2) 0 --- inspect .026 .027 5.5 0    0    error (invalid witness file) 0 --- inspect 1.1  .72 46 0      0      error (invalid witness file) 0 --- inspect .0048 .0058 .53 0    0     - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i unknown 0 --- inspect 86 50   1100 920 5.7  0      error (invalid witness file) 0 --- inspect .62 .37 41 0   0    error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .91 .61 47 0      0      error (invalid witness file) 0 --- inspect .0048 .0060 .52 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) 0 wit inspect 140 110   1200 1600 3.1  .0041 true -32 wit inspect 19    10    630 0   0    unknown 0 --- inspect 9.6   5.2   320   .66 0    unknown 0 --- inspect 11    6.1  390 0      .79   error (2) 0 --- inspect 2.4    2.4    35    .50 0     - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i false(unreach-call) 1 wit inspect 730 700   890 7300 2.8  .061  false(unreach-call) 1 wit inspect 12    6.5  410 0   0    timeout (error (7)) 0 --- inspect 92     65     1900   .68 0    unknown 0 --- inspect 8.9  4.8  290 0      .10   error (2) 0 --- inspect 1.8    1.8    28    2.0  0     - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i false(unreach-call) 1 wit inspect 270 210   3000 2600 2.1  0      false(unreach-call) 1 wit inspect 13    6.9  430 0   0    timeout 0 --- inspect 97     82     4100   1.6  0    unknown 0 --- inspect 8.5  4.6  290 0      0      error (2) 0 --- inspect 1.6    1.6    26    1.5  .23  - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i timeout 0 --- inspect 900 870   990 10000 3.3  0      error (invalid witness file) 0 --- inspect .72 .43 42 0   0    error (2) 0 --- inspect .021 .022 5.7 0    0    error (invalid witness file) 0 --- inspect 1.2  .78 48 0      0      error (invalid witness file) 0 --- inspect .0050 .0064 .53 0    0     - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i unknown 0 --- inspect 58 21   640 480 14    0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0    error (2) 0 --- inspect .026 .027 5.6 0    0    error (invalid witness file) 0 --- inspect .96 .62 46 0      0      error (invalid witness file) 0 --- inspect .0026 .0086 .52 0    0     - --- 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 73 41   750 780 2.4  0      false(unreach-call) 1 wit inspect 15    8.5  530 0   0    true -32 --- inspect 38     23     1100   .62 0    unknown 0 --- inspect 10    5.5  310 0      .34   error (2) 0 --- inspect 1.8    1.8    28    1.6  0     - --- 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 710 630   2200 8300 1.7  0      timeout 0 wit inspect 97    78    2000 0   0    timeout 0 --- inspect 97     87     3600   1.8  0    unknown 0 --- inspect 6.9  3.8  280 0      .50   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 170 140   1200 2100 1.7  0      timeout 0 wit inspect 97    78    1100 0   0    true -32 --- inspect 29     15     520   .66 0    unknown 0 --- inspect 6.7  3.7  280 0      .078  error (2) 0 --- inspect 1.4    1.4    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 690 650   4500 7300 1.4  0      timeout 0 wit inspect 97    70    2500 0   0    true -32 --- inspect 22     13     810   .62 0    unknown 0 --- inspect 6.2  3.4  280 0      .44   error (2) 0 --- inspect 1.2    1.2    22    .91 0     - --- 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 300 260   1000 3500 1.6  .51   true -32 wit inspect 16    8.4  540 0   0    error (7) 0 --- inspect 23     13     520   .75 0    unknown 0 --- inspect 7.5  4.1  290 0      1.1    error (2) 0 --- inspect 1.3    1.2    24    .19 0     - --- inspect - --- inspect
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i true 2 wit inspect 43 16   1000 340 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    860    3800 0   0      true 2 --- inspect 34     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 180 120   3000 1900 150    0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 wit inspect 370    340    1700 0   0      error (7) 0 --- inspect 70     40     1200   .73 0     
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i true 2 wit inspect 58 18   2000 510 140    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    860    2700 0   0      true 2 --- inspect 28     17     650   .66 0     
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i true 2 wit inspect 29 11   670 240 170    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    810    6000 0   .26   true 2 --- inspect 34     19     1000   .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 150 80   6000 1500 150    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 --- inspect 11    6.0  300 0   0      true 2 --- inspect 69     54     3400   .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 760 650   6200 9200 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    710    6500 0   0      timeout 0 --- inspect 960     900     5600   1.5  0     
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i true 2 wit inspect 22 8.9 620 180 140    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    640    6000 0   0      true 2 --- inspect 18     9.7   450   .62 0     
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i true 2 wit inspect 60 26   2900 530 140    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 740    650    7000 0   0      true 2 --- inspect 40     26     2200   .66 .23  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i unknown 0 --- inspect 17 7.3 260 150 1.4  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i true 2 wit inspect 40 15   970 350 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    620    6000 0   0      true 2 --- inspect 35     20     770   .66 0     
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i true 2 wit inspect 51 21   1100 410 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    700    6400 0   0      true 2 --- inspect 42     26     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 40 15   960 320 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 960    830    5700 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 unknown 0 --- inspect 30 14   440 320 1.2  .070  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i unknown 0 --- inspect 75 41   1100 820 1.9  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-media-video-msp3400.ko_true-unreach-call.cil.out.i true 2 wit inspect 42 15   950 340 200    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    710    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 31 11   760 280 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 680    560    7000 0   0      true 2 --- inspect 21     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 33 13   860 260 150    0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 --- inspect 9.7  5.3  340 0   0      true 2 --- inspect 23     13     570   .66 0     
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i true 1 wit inspect 23 11   450 200 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    770    6700 0   0      error (7) 0 --- inspect 12     7.1   310   .75 0     
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i unknown 0 --- inspect 27 12   450 250 1.3  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 42 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 true 1 wit inspect 82 27   2800 760 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    830    4200 0   0      error (7) 0 --- inspect 100     72     1400   .71 .045 
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i unknown 0 --- inspect 820 800   960 10000 1.6  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .47 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i unknown 0 --- inspect 160 110   1900 1900 3.4  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i true 2 wit inspect 49 17   1600 420 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    620    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 unknown 0 --- inspect 260 180   2800 2900 27    0      error (invalid witness file) 0 --- inspect .57 .36 40 0   0    error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect 1.1  .72 48 0      0      error (invalid witness file) 0 --- inspect .0018 .0042 .41 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 false(unreach-call) 1 wit inspect 98 71   1100 1000 1.6  0      false(unreach-call) 1 wit inspect 18    11    680 0   0    error (7) 0 --- inspect 71     39     2000   .71 0    unknown 0 --- inspect 8.3  4.5  320 0      .34   error (2) 0 --- inspect 2.6    2.6    28    .21 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 false(unreach-call) 0 wit inspect 71 41   880 710 2.1  0      true -32 wit inspect 11    5.5  500 0   0    error (7) 0 --- inspect 67     46     740   .68 .27 unknown 0 --- inspect 9.1  4.9  340 0      .95   error (1) 0 --- inspect 1.4    1.4    31    .27 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 94 67   760 1200 2.4  .86   false(unreach-call) 1 wit inspect 65    59    800 0   0    unknown 0 --- inspect 12     6.8   320   .66 0    exception 0 --- inspect 11    6.0  340 0      1.1    error (1) 0 --- inspect 2.5    2.5    33    .44 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 280 250   2600 3000 8.8  0      true -32 wit inspect 51    40    1900 0   0    unknown 0 --- inspect 8.6   4.8   450   .65 0    unknown 0 --- inspect 14    7.7  490 0      .43   error (2) 0 --- inspect 6.1    6.2    67    3.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 out of memory 0 --- inspect 100 77   15000 1100 4.5  0      error (invalid witness file) 0 --- inspect .57 .36 41 0   0    error (2) 0 --- inspect .025 .026 5.6 0    0    error (invalid witness file) 0 --- inspect 1.2  .76 47 0      0      error (invalid witness file) 0 --- inspect .0016 .0023 .54 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) 0 wit inspect 80 54   1100 970 2.0  0      true -32 wit inspect 9.1  4.8  370 0   0    timeout 0 --- inspect 97     85     3500   .73 0    unknown 0 --- inspect 8.6  4.7  290 0      .43   error (2) 0 --- inspect 1.6    1.6    27    1.6  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 false(unreach-call) 0 wit inspect 640 620   1300 4700 2.3  0      timeout 0 --- inspect 97    71    2500 0   0    timeout 0 --- inspect 97     84     4200   1.5  0    unknown 0 --- inspect 9.0  4.8  350 0      0      error (2) 0 --- inspect 2.0    2.0    29    2.1  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 timeout 0 --- inspect 900 890   320 12000 2.4  .090  error (invalid witness file) 0 --- inspect .73 .44 42 0   0    error (2) 0 --- inspect .023 .023 5.6 0    0    error (invalid witness file) 0 --- inspect .95 .61 47 0      0      error (invalid witness file) 0 --- inspect .0016 .0019 .40 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 56 31   1200 610 2.3  0      false(unreach-call) 1 wit inspect 16    8.9  550 0   0    timeout 0 --- inspect 97     72     1400   1.3  0    unknown 0 --- inspect 8.8  4.8  310 0      1.1    error (2) 0 --- inspect 2.0    2.0    29    .32 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 90 57   1100 1000 2.2  0      false(unreach-call) 1 wit inspect 13    7.5  560 0   0    timeout 0 --- inspect 96     63     1400   .75 0    unknown 0 --- inspect 9.0  4.9  310 0      .34   error (1) 0 --- inspect 1.7    1.7    30    .33 .33  - --- 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 890   2500 5200 10    0      error (invalid witness file) 0 --- inspect .77 .47 40 0   0    error (2) 0 --- inspect .021 .022 5.6 0    0    error (invalid witness file) 0 --- inspect .92 .60 47 0      0      error (invalid witness file) 0 --- inspect .0065 .0085 .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 unknown 0 --- inspect 39 15   450 350 8.8  0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0    error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect 1.2  .75 47 0      0      error (invalid witness file) 0 --- inspect .0053 .0070 .52 0    0     - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(unreach-call) 1 wit inspect 45 23   680 490 1.7  .0041 false(unreach-call) 1 wit inspect 10    6.1  350 0   0    unknown 0 --- inspect 59     38     810   .75 0    unknown 0 --- inspect 6.6  3.6  280 0      0      error (2) 0 --- inspect 1.4    1.4    24    1.3  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 unknown 0 --- inspect 42 16   500 340 7.0  0      error (invalid witness file) 0 --- inspect .59 .37 40 0   0    error (2) 0 --- inspect .025 .027 5.8 0    0    error (invalid witness file) 0 --- inspect .94 .61 47 0      0      error (invalid witness file) 0 --- inspect .0058 .0095 .52 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 unknown 0 --- inspect 190 140   1400 2300 8.1  0      error (invalid witness file) 0 --- inspect .79 .48 41 0   0    error (2) 0 --- inspect .021 .022 5.6 0    0    error (invalid witness file) 0 --- inspect .97 .62 47 0      0      error (invalid witness file) 0 --- inspect .0016 .0021 .54 0    0     - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unknown 0 --- inspect 330 310   6400 2300 4.1  0      error (invalid witness file) 0 --- inspect .67 .42 42 0   0    error (2) 0 --- inspect .026 .027 5.6 0    0    error (invalid witness file) 0 --- inspect 1.2  .79 47 0      0      error (invalid witness file) 0 --- inspect .0017 .0020 .39 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 45 14   380 400 9.7  0      error (invalid witness file) 0 --- inspect .63 .39 40 0   0    error (2) 0 --- inspect .022 .025 5.6 0    0    error (invalid witness file) 0 --- inspect .91 .59 47 0      0      error (invalid witness file) 0 --- inspect .0058 .0072 .53 0    0     - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i false(unreach-call) 1 wit inspect 180 140   2900 2000 5.3  0      false(unreach-call) 1 wit inspect 39    25    2100 0   0    error (7) 0 --- inspect 16     8.7   600   .73 0    timeout 0 --- inspect 8.7  130    450 .0041 0      error (1) 0 --- inspect .83   .83   23    1.8  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 140 71   1800 1200 22    0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0    error (2) 0 --- inspect .024 .024 5.6 0    0    error (invalid witness file) 0 --- inspect .90 .59 46 0      0      error (invalid witness file) 0 --- inspect .0018 .0024 .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 91 40   1300 810 21    0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0    error (2) 0 --- inspect .026 .027 5.5 0    0    error (invalid witness file) 0 --- inspect 1.1  .71 47 0      0      error (invalid witness file) 0 --- inspect .0017 .0021 .54 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 220 180   2700 2400 4.3  0      timeout 0 wit inspect 94    81    2100 0   0    error (7) 0 --- inspect 18     9.6   470   .66 0    timeout 0 --- inspect 8.9  130    450 .91   0      error (1) 0 --- inspect .78   .78   23    1.4  0     - --- inspect - --- inspect
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.i false(unreach-call) 1 wit inspect 190 150   2300 1900 4.2  .070  false(unreach-call) 1 wit inspect 87    70    1700 0   0    error (7) 0 --- inspect 16     8.5   500   .73 0    timeout 0 --- inspect 7.5  130    440 .0041 0      error (1) 0 --- inspect .80   .80   23    1.6  0     - --- inspect - --- inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--misc--sgi-xp--xpc.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i out of memory 0 --- inspect 710 680   15000 4500 4.1  0      error (invalid witness file) 0 --- inspect .58 .36 42 0   0    error (2) 0 --- inspect .020 .020 5.6 0    0    error (invalid witness file) 0 --- inspect 1.2  .74 47 0      0      error (invalid witness file) 0 --- inspect .0052 .0065 .54 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 880   2000 5800 3.1  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 .96 .62 49 0      0      error (invalid witness file) 0 --- inspect .0015 .0024 .54 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 860   1700 7800 5.1  0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0    error (2) 0 --- inspect .021 .021 5.6 0    0    error (invalid witness file) 0 --- inspect 1.1  .73 48 0      0      error (invalid witness file) 0 --- inspect .0015 .0017 .41 0    0     - --- inspect - --- inspect
ldv-linux-3.4-simple/43_1a_cilled_false-unreach-call_ok_linux-43_1a-drivers--scsi--megaraid--megaraid_mm_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i false(unreach-call) 0 wit inspect 190 160   1300 1700 1.9  0      true -32 wit inspect 12    6.3  470 0   0    error (7) 0 --- inspect 68     50     700   .68 0    unknown 0 --- inspect 8.5  4.6  330 0      0      error (1) 0 --- inspect 1.3    1.3    29    .21 .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 720 690   15000 6000 3.6  0      error (invalid witness file) 0 --- inspect .57 .34 41 0   0    error (2) 0 --- inspect .025 .027 5.8 0    0    error (invalid witness file) 0 --- inspect .89 .59 46 0      0      error (invalid witness file) 0 --- inspect .0043 .0054 .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 out of memory 0 --- inspect 100 78   15000 1200 3.1  0      error (invalid witness file) 0 --- inspect .61 .37 42 0   0    error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .94 .62 48 0      0      error (invalid witness file) 0 --- inspect .0017 .0030 .56 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 23 8.7 640 190 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 700    690    7000 0   0      true 2 --- inspect 22     14     940   .62 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 18 7.6 510 150 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 900    870    7000 0   .094  true 2 --- inspect 13     7.4   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 23 8.9 640 200 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 640    620    7000 0   0      true 2 --- inspect 18     11     710   .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 1 wit inspect 24 9.5 620 210 150    .15   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    6100 0   0      unknown 0 --- inspect 35     22     670   .75 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 22 9.1 570 170 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6800 0   0      true 2 --- inspect 11     6.5   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 21 8.3 680 180 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    850    6000 0   0      true 2 --- inspect 15     8.5   520   .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 true 2 wit inspect 20 8.2 540 170 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6800 0   0      true 2 --- inspect 26     17     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 14 6.3 470 110 140    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 620    600    7000 0   0      true 2 --- inspect 11     6.2   440   .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 20 8.2 620 180 140    .070  - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 550    520    7000 0   0      true 2 --- inspect 19     11     480   .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 33 12   870 320 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 800    760    7000 0   0      true 2 --- inspect 32     19     710   .62 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 25 9.6 660 210 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 590    490    7000 0   0      true 2 --- inspect 23     14     500   .62 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 28 10   770 230 170    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 580    500    7000 0   0      true 2 --- inspect 29     16     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 31 11   950 290 140    .070  - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 780    700    7000 0   0      true 2 --- inspect 28     16     580   .62 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 26 9.7 750 210 140    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    640    6700 0   0      true 2 --- inspect 21     13     560   .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 20 7.8 620 150 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5800 0   0      true 2 --- inspect 16     8.6   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 23 9.0 660 190 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 650    610    7000 0   0      true 2 --- inspect 20     13     530   .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 32 12   850 250 190    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 820    730    7000 0   0      true 2 --- inspect 27     16     620   .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 31 11   860 250 140    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 620    530    7000 0   0      true 2 --- inspect 26     16     560   .62 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 31 11   890 250 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 920    710    6800 0   0      true 2 --- inspect 26     15     570   .62 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 19 8.1 650 170 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 860    820    7000 0   0      true 2 --- inspect 15     8.1   460   .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 30 11   810 260 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 690    660    7000 0   0      true 2 --- inspect 27     15     590   .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 47 17   1300 410 140    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5600 0   0      true 2 --- inspect 41     23     850   .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 16 7.1 490 150 140    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    3600 0   .049  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--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i true 2 wit inspect 40 14   1700 350 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    4200 0   0      true 2 --- inspect 37     25     750   .62 .15  
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 14 6.7 490 120 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 520    500    7000 0   0      true 2 --- inspect 16     10     490   .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 22 10   630 200 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    6100 0   0      true 2 --- inspect 15     8.3   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 15 6.7 490 130 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    4800 0   0      true 2 --- inspect 10     5.8   350   .66 .025 
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 13 6.6 460 110 140    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 500    490    7000 0   0      true 2 --- inspect 9.1   5.5   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 23 9.1 690 190 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 880    850    7000 0   0      true 2 --- inspect 29     18     610   .66 .18  
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 18 7.7 510 150 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5600 0   0      true 2 --- inspect 17     11     430   .66 .090 
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 18 7.6 520 150 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 910    890    5900 0   0      true 2 --- inspect 14     10     410   .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 19 7.9 550 170 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    890    5200 0   0      true 2 --- inspect 17     12     420   .62 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 17 7.2 500 140 170    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 380    370    7000 0   0      true 2 --- inspect 13     8.3   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 18 7.8 560 160 150    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    6100 0   0      true 2 --- inspect 15     9.5   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 26 9.8 650 240 140    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 wit inspect 900    880    5200 0   0      true 2 --- inspect 20     12     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 17 7.4 560 140 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 460    450    7000 0   .12   true 2 --- inspect 11     6.6   440   .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 7.5 500 140 140    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 550    530    7000 0   0      true 2 --- inspect 9.9   6.0   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 17 7.5 500 140 150    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 500    480    7000 0   0      true 2 --- inspect 11     6.2   330   .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 18 7.5 510 130 150    0      - --- inspect - --- inspect - ---