Tool DIVINE 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-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 01:45:35 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-divine-smt.sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-divine-smt.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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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 0 2.3 2.3 230 29 0      0     0 .86 .51 40 0   0   0 .028 .029 5.6 0   0   0 1.2  .77 47 0   0   0 .0016 .0020 .53 0   0   - -
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i 0 1.7 1.7 210 21 0      0     0 .77 .47 40 0   0   0 .023 .024 5.6 0   0   0 1.1  .69 47 0   0   0 .0055 .0068 .53 0   0   - -
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i 0 1.7 1.7 210 22 0      0     0 .69 .43 41 0   0   0 .024 .025 5.6 0   0   0 .96 .61 47 0   0   0 .0051 .0065 .53 0   0   - -
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i 0 1.8 1.8 210 27 0      0     0 .63 .39 41 0   0   0 .023 .024 5.6 0   0   0 1.0  .63 49 0   0   0 .0016 .0019 .41 0   0   - -
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i 0 1.8 1.8 210 24 0      0     0 .77 .47 40 0   0   0 .026 .027 5.6 0   0   0 .97 .62 46 0   0   0 .0050 .0062 .52 0   0   - -
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i 0 1.7 1.7 210 23 0      0     0 .70 .45 41 0   0   0 .030 .031 5.6 0   0   0 1.2  .75 48 0   0   0 .0017 .0021 .52 0   0   - -
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i 0 1.6 1.7 210 25 0      0     0 .75 .45 40 0   0   0 .021 .022 5.7 0   0   0 1.1  .67 47 0   0   0 .0023 .0030 .53 0   0   - -
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i 0 1.7 1.8 210 26 0      0     0 .75 .46 41 0   0   0 .022 .023 5.8 0   0   0 1.2  .80 48 0   0   0 .0044 .0058 .52 0   0   - -
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i 0 2.0 2.0 220 24 0      0     0 .60 .36 40 0   0   0 .026 .027 5.6 0   0   0 .94 .62 47 0   0   0 .0059 .0076 .53 0   0   - -
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i 0 1.7 1.7 210 21 0      0     0 .74 .46 40 0   0   0 .027 .029 5.6 0   0   0 1.0  .63 49 0   0   0 .0048 .0059 .54 0   0   - -
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i 0 1.6 1.6 200 21 0      0     0 .73 .45 40 0   0   0 .025 .026 5.6 0   0   0 .94 .61 47 0   0   0 .0048 .0054 .40 0   0   - -
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i 0 1.6 1.6 200 20 0      0     0 .73 .45 42 0   0   0 .027 .028 5.6 0   0   0 .99 .66 47 0   0   0 .0058 .0073 .52 0   0   - -
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i 0 1.6 1.7 200 20 0      0     0 .74 .45 40 0   0   0 .021 .023 5.6 0   0   0 1.1  .71 46 0   0   0 .0048 .0076 .53 0   0   - -
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i 0 1.6 1.6 200 20 0      0     0 .80 .49 41 0   0   0 .025 .026 5.6 0   0   0 1.1  .68 47 0   0   0 .0048 .0061 .53 0   0   - -
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i 0 1.7 1.8 210 22 0      0     - - - - 0 .59 .37 40 0   0   0 .023 .023 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i 0 2.3 2.3 230 27 0      0     - - - - 0 .68 .42 40 0   0   0 .021 .021 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 23 0      0     - - - - 0 .62 .40 40 0   0   0 .023 .024 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i 0 1.6 1.7 210 24 0      0     - - - - 0 .79 .48 42 0   0   0 .026 .027 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 20 0      0     - - - - 0 .73 .43 40 0   0   0 .022 .022 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i 0 2.6 2.6 250 35 0      0     - - - - 0 .62 .38 40 0   0   0 .022 .023 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 22 0      0     - - - - 0 .75 .46 41 0   0   0 .020 .028 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i 0 1.7 1.7 210 24 0      0     - - - - 0 .71 .45 41 0   0   0 .025 .027 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 20 0      0     - - - - 0 .59 .36 40 0   0   0 .028 .036 5.5 0   0  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i 0 1.7 1.7 210 23 0      0     - - - - 0 .68 .41 41 0   0   0 .027 .028 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i 0 1.8 1.8 210 23 0      0     - - - - 0 .62 .39 41 0   0   0 .023 .025 5.6 0   0  
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i 0 1.7 1.7 200 21 0      0     - - - - 0 .62 .38 41 0   0   0 .021 .022 5.8 0   0  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 20 0      0     - - - - 0 .62 .39 41 0   0   0 .022 .023 5.6 0   0  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i 0 1.6 1.7 200 20 0      0     - - - - 0 .60 .38 40 0   0   0 .023 .024 5.8 0   0  
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i 0 1.6 1.7 210 21 0      0     - - - - 0 .62 .39 41 0   0   0 .020 .022 5.6 0   0  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 22 0      0     - - - - 0 .70 .43 40 0   0   0 .026 .027 5.8 0   0  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 21 0      0     - - - - 0 .76 .48 41 0   0   0 .021 .022 5.6 0   0  
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i 0 1.7 1.7 210 20 0      0     - - - - 0 .62 .39 40 0   0   0 .027 .028 5.8 0   0  
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 24 0      0     - - - - 0 .74 .45 41 0   0   0 .025 .025 5.6 0   0  
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i 0 1.6 1.7 200 19 0      0     - - - - 0 .59 .36 41 0   0   0 .023 .024 5.7 0   0  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i 0 1.6 1.6 200 25 0      0     - - - - 0 .75 .47 41 0   0   0 .026 .027 5.6 0   0  
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i 0 1.7 1.7 200 23 0      0     - - - - 0 .61 .37 40 0   0   0 .027 .027 5.6 0   0  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i 0 1.6 1.6 210 23 0      0     - - - - 0 .59 .36 40 0   0   0 .023 .024 5.6 0   0  
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i 0 2.3 2.3 250 29 0      0     0 .72 .43 40 0   0   0 .026 .027 5.6 0   0   0 1.2  .77 46 0   0   0 .0055 .0069 .54 0   0   - -
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 0 1.6 1.6 200 19 0      0     0 .67 .40 40 0   0   0 .026 .028 5.6 0   0   0 .95 .61 47 0   0   0 .0022 .0030 .54 0   0   - -
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 0 1.6 1.7 210 19 0      0     0 .67 .40 40 0   0   0 .026 .027 5.6 0   0   0 1.2  .74 48 0   0   0 .0070 .012  .53 0   0   - -
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 0 1.7 1.7 210 24 0      0     0 .73 .45 40 0   0   0 .025 .026 5.8 0   0   0 .96 .61 47 0   0   0 .0047 .0058 .52 0   0   - -
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 0 1.9 1.9 220 24 0      0     0 .70 .43 41 0   0   0 .025 .026 5.6 0   0   0 .99 .64 47 0   0   0 .0016 .0026 .53 0   0   - -
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 0 1.8 1.8 220 29 0      0     0 .62 .38 40 0   0   0 .022 .023 5.6 0   0   0 1.1  .75 46 0   0   0 .0048 .0062 .41 0   0   - -
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 0 1.7 1.7 210 22 0      0     0 .76 .47 41 0   0   0 .021 .023 5.6 0   0   0 1.0  .66 48 0   0   0 .0017 .0022 .54 0   0   - -
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 0 1.7 1.7 210 26 0      0     0 .74 .46 43 0   0   0 .025 .026 5.7 0   0   0 1.2  .77 47 0   0   0 .0023 .0036 .41 0   0   - -
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 0 1.7 1.8 210 21 0      0     0 .62 .38 41 0   0   0 .024 .024 5.6 0   0   0 1.1  .71 47 0   0   0 .0017 .0028 .53 0   0   - -
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 0 1.7 1.7 210 25 0      0     0 .75 .47 41 0   0   0 .023 .024 5.6 0   0   0 1.2  .78 48 0   0   0 .0025 .0040 .54 0   0   - -
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 0 1.7 1.7 210 22 0      0     0 .83 .53 40 0   0   0 .021 .022 5.6 0   0   0 .92 .61 46 0   0   0 .0059 .0077 .52 0   0   - -
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 0 2.3 2.3 250 31 0      0     0 .69 .42 41 0   0   0 .026 .026 5.6 0   0   0 1.2  .78 48 0   0   0 .0039 .0050 .54 0   0   - -
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 0 1.8 1.8 220 27 0      0     0 .74 .46 41 0   0   0 .023 .024 5.6 0   0   0 1.2  .76 49 0   0   0 .0067 .0086 .53 0   0   - -
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 0 1.6 1.6 200 23 0      0     0 .73 .45 40 0   0   0 .027 .028 5.6 0   0   0 1.1  .70 47 0   0   0 .0028 .0037 .40 0   0   - -
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 0 1.8 1.8 220 25 0      0     0 .76 .46 40 0   0   0 .027 .027 5.6 0   0   0 1.1  .74 48 0   0   0 .0018 .0023 .53 0   0   - -
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 0 1.8 1.9 220 22 0      0     0 .75 .45 42 0   0   0 .021 .023 5.6 0   0   0 1.2  .78 48 0   0   0 .0016 .0021 .54 0   0   - -
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 0 1.8 1.8 220 22 0      0     0 .77 .47 42 0   0   0 .021 .022 5.7 0   0   0 1.1  .73 47 0   0   0 .0020 .0026 .52 0   0   - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.i 0 1.8 1.8 210 26 0      0     0 .74 .46 40 0   0   0 .020 .022 5.6 0   0   0 1.0  .66 47 0   0   0 .0017 .0022 .54 0   0   - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i 0 1.9 1.9 210 24 0      0     0 .64 .39 40 0   0   0 .027 .027 5.6 0   0   0 1.0  .65 48 0   0   0 .0039 .0044 .40 0   0   - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.i 0 2.0 2.0 210 25 0      0     0 .77 .48 41 0   0   0 .023 .023 5.6 0   0   0 1.2  .79 48 0   0   0 .0019 .0023 .53 0   0   - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.i 0 1.9 1.9 210 23 0      0     0 .72 .43 44 0   0   0 .033 .035 5.6 0   0   0 1.0  .65 47 0   0   0 .0067 .0084 .53 0   0   - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.i 0 1.8 1.8 210 22 0      0     0 .70 .43 42 0   0   0 .025 .026 5.8 0   0   0 .94 .62 47 0   0   0 .0052 .0064 .53 0   0   - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.i 0 1.9 1.9 210 24 0      0     0 .77 .47 41 0   0   0 .027 .030 5.7 0   0   0 1.1  .73 47 0   0   0 .0020 .0027 .52 0   0   - -
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 0 1.8 1.8 220 21 0      0     0 .94 .58 40 0   0   0 .021 .021 5.6 0   0   0 1.1  .68 47 0   0   0 .0025 .0033 .42 0   0   - -
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 0 1.7 1.7 210 24 0      .99  0 .66 .40 41 0   0   0 .023 .025 5.7 0   0   0 1.1  .74 47 0   0   0 .0046 .0059 .53 0   0   - -
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 0 1.8 1.8 220 22 0      0     0 .60 .38 41 0   0   0 .023 .024 5.6 0   0   0 1.2  .77 47 0   0   0 .0026 .0034 .53 0   0   - -
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 0 1.6 1.7 210 18 0      0     0 .58 .37 41 0   0   0 .028 .029 5.7 0   0   0 1.1  .68 48 0   0   0 .0036 .0057 .54 0   0   - -
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 0 1.7 1.7 210 21 0      0     0 .77 .48 42 0   0   0 .021 .021 5.6 0   0   0 1.2  .79 47 0   0   0 .0050 .0069 .42 0   0   - -
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 0 1.8 1.8 210 24 0      0     0 .64 .39 42 0   0   0 .026 .027 5.8 0   0   0 1.3  .80 47 0   0   0 .0058 .0078 .54 0   0   - -
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 0 10   9.2 430 120 0      0     - - - - 0 .59 .37 40 0   0   0 .021 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--ec_sys.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 22 0      0     - - - - 0 .74 .45 40 0   0   0 .027 .028 5.5 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 23 0      0     - - - - 0 .63 .40 42 0   0   0 .023 .024 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_marvell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.8 200 24 0      0     - - - - 0 .71 .43 41 0   0   0 .026 .026 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--ata--pata_netcell.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.9 1.9 200 25 0      0     - - - - 0 .61 .36 40 0   0   0 .020 .021 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--cfag12864b.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 21 0      0     - - - - 0 .61 .39 41 0   0   0 .027 .028 5.6 0   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 0 1.6 1.6 200 21 0      0     - - - - 0 .75 .45 40 0   0   0 .022 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--auxdisplay--ks0108.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 23 0      0     - - - - 0 .78 .48 41 0   0   0 .034 .035 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--aten.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 21   14   440 250 0      0     - - - - 0 .63 .39 40 0   0   0 .022 .023 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--bpck.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 31   18   450 370 0      0     - - - - 0 .74 .46 41 0   0   0 .021 .022 5.7 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--comm.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 21   14   440 230 0      0     - - - - 0 .75 .46 40 0   0   0 .021 .022 5.7 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--dstr.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 21   14   440 240 0      0     - - - - 0 .78 .49 41 0   0   0 .021 .022 5.7 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epat.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 25   15   440 300 0      0     - - - - 0 .57 .36 40 0   0   0 .020 .020 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--epia.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 24   15   440 240 0      0     - - - - 0 .61 .37 40 0   0   0 .021 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 20   13   440 220 0      0     - - - - 0 .74 .46 40 0   0   0 .021 .021 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--fit3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 21   13   440 220 0      0     - - - - 0 .75 .44 41 0   0   0 .027 .027 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--friq.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 27   16   450 320 0      0     - - - - 0 .64 .40 41 0   0   0 .021 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--frpw.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 24   15   440 270 0      0     - - - - 0 .68 .42 40 0   0   0 .021 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--kbic.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 66   32   440 660 0      0     - - - - 0 .61 .37 41 0   0   0 .022 .023 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--ktti.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 20   13   440 240 0      0     - - - - 0 .69 .43 41 0   0   0 .026 .027 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on20.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 21   14   440 230 0      0     - - - - 0 .63 .37 40 0   0   0 .023 .023 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--block--paride--on26.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 26   16   460 290 0      0     - - - - 0 .59 .36 40 0   0   0 .028 .030 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--hw_random--virtio-rng.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 19 0      0     - - - - 0 .77 .47 40 0   0   0 .027 .029 5.7 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ipmi--ipmi_poweroff.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 22 0      0     - - - - 0 .66 .42 40 0   0   0 .025 .027 5.8 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--ramoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 22 0      0     - - - - 0 .62 .37 40 0   0   0 .027 .028 5.6 0   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 0 1.6 1.6 200 26 0      .082 - - - - 0 .76 .46 41 0   0   0 .021 .022 5.8 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.6 1.7 200 21 0      0     - - - - 0 .58 .35 40 0   0   0 .021 .023 5.7 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--cpufreq--cpufreq_powersave.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 9.4 8.9 430 130 0      0     - - - - 0 .59 .37 41 0   0   0 .026 .027 5.6 0   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 0 1.6 1.7 200 21 0      0     - - - - 0 .77 .47 41 0   0   0 .021 .023 5.7 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-74x164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.6 1.6 200 19 0      0     - - - - 0 .74 .45 41 0   0   0 .022 .023 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-max7301.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 21 0      0     - - - - 0 .62 .37 42 0   0   0 .026 .027 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-mc33880.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.6 1.6 200 18 0      0     - - - - 0 .77 .48 41 0   0   0 .021 .022 5.7 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-tps65912.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.7 1.7 200 19 0      0     - - - - 0 .61 .37 42 0   0   0 .021 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpio--gpio-wm831x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 1.6 1.6 200 20 0      0     - - - - 0 .73 .45 41 0   0   0 .025 .026 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--i2c--sil164.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 900   230   380 8400 .0041 0     - - - - 0 .65 .40 40 0   0   0 .026 .027 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--drm--tdfx--tdfx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 8.8 8.5 430 110 0      0     - - - - 0 .60 .37 40 0   0   0 .021 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--gpu--stub--poulsbo.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 13   11   430 170 0      0     - - - - 0 .77 .48 41 0   0   0 .023 .024 5.7 0   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 0 10   9.2 430 120 0      0     - - - - 0 .59 .37 40 0   0   0 .026 .027 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-chicony.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 9.5 9.0 430 120 0      0     - - - - 0 .75 .46 41 0   0   0 .021 .021 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-elecom.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 9.5 9.0 430 110 0      0     - - - - 0 .73 .45 40 0   0   0 .022 .022 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ezkey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 10   9.1 430 120 0      0     - - - - 0 .65 .40 40 0   0   0 .023 .023 5.6 0   0  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-gyration.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i 0 10   9.1 430 120 0      0     - - -