Tool ULTIMATE Automizer 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 01:06:24 CET 2017-12-03 03:07:09 CET 2017-12-03 03:49:57 CET 2017-12-03 03:57:59 CET 2017-12-03 04:29:07 CET 2017-12-02 23:12:02 CET 2017-12-03 03:11:19 CET
Run set uautomizer.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_DeviceDriversLinux64_ReachSafety cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.Systems_DeviceDriversLinux64_ReachSafety
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.pp.i 0 7.7 480 61 0 .50 43 0 .019 4.9 0 .79 49 0 .0012 .26 - -
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i 0 900   3300 6700 0 .71 44 0 .023 4.9 0 .97 47 0 .0016 .27 - -
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i 0 900   5300 8400 0 .54 42 0 .028 4.9 0 .92 49 0 .0016 .28 - -
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i.pp.i 0 640   2100 5300 0 .63 44 0 .018 5.0 0 .86 48 0 .0011 .31 - -
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i.pp.i 0 6.2 340 53 0 .56 41 0 .019 4.9 0 1.0  49 0 .0014 .26 - -
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i 0 600   1500 7800 0 .71 41 0 .019 4.8 0 .96 49 0 .0016 .27 - -
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i.pp.i 0 900   3500 6200 0 .46 44 0 .023 4.9 0 .86 47 0 .0017 .27 - -
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i.pp.i 0 130   2100 1100 0 .72 42 0 .018 4.8 0 .83 48 0 .0016 .30 - -
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i.pp.i 0 900   6800 8300 0 .66 42 0 .019 4.9 0 .87 48 0 .0015 .26 - -
ldv-linux-3.0/usb_urb-drivers-hid-usbhid-usbmouse.ko_false-unreach-call.cil.out.i.pp.i 0 21   710 170 0 .65 43 0 .021 4.9 0 1.1  49 0 .0014 .26 - -
ldv-linux-3.0/usb_urb-drivers-input-misc-keyspan_remote.ko_false-unreach-call.cil.out.i.pp.i 0 900   4500 6000 0 .53 41 0 .026 4.8 0 1.0  49 0 .0011 .26 - -
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i.pp.i 0 87   2100 670 0 .58 44 0 .019 4.9 0 1.1  49 0 .0017 .26 - -
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i.pp.i 0 58   1900 420 0 .66 41 0 .020 4.9 0 1.1  49 0 .0016 .29 - -
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i 0 800   3300 8900 0 .62 41 0 .021 4.8 0 1.0  48 0 .0014 .29 - -
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i.pp.i 0 900   3700 11000 0 .63 43 0 .018 4.8 0 .89 48 0 .0012 .32 - -
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i.pp.i 0 89   2700 820 0 .70 43 0 .044 4.9 0 .83 49 0 .0016 .26 - -
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i 2 28   900 220 - - - - 0 900    3700 2 41     730  
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i 2 120   2900 1300 - - - - 0 350    1900 2 120     3000  
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i.pp.i 2 41   2000 310 - - - - 0 900    2700 2 49     1900  
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i.pp.i 2 15   560 110 - - - - 0 790    7000 2 18     510  
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i 2 130   5800 970 - - - - 0 10    350 2 170     6100  
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i.pp.i 0 910   10000 11000 - - - - 0 .68 43 0 .018 4.9
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i.pp.i 2 12   490 96 - - - - 0 910    5900 2 14     470  
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i.pp.i 2 49   3400 460 - - - - 0 910    6700 2 60     3100  
ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i 2 33   930 270 - - - - 0 920    5800 2 49     810  
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i.pp.i 2 14   580 110 - - - - 0 810    7000 2 16     520  
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i 2 25   860 190 - - - - 0 920    5900 2 29     640  
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i.pp.i 2 35   1100 270 - - - - 0 900    6300 2 37     870  
ldv-linux-3.0/module_get_put-drivers-staging-et131x-et131x.ko_true-unreach-call.cil.out.i.pp.i 2 33   1500 300 - - - - 0 910    6000 2 41     1300  
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i.pp.i 2 28   850 220 - - - - 0 940    5500 2 31     790  
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i.pp.i 2 48   1500 350 - - - - 0 900    5500 2 49     1200  
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i 2 20   750 160 - - - - 0 910    5800 2 24     550  
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i.pp.i 2 28   880 230 - - - - 0 910    6000 2 27     820  
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i.pp.i 2 20   740 150 - - - - 0 900    2600 2 14     650  
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i.pp.i 2 20   730 140 - - - - 0 8.9  280 2 15     540  
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i.pp.i 0 10   290 79 - - - - 0 .53 43 0 .023 4.9
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i.pp.i 2 72   2800 610 - - - - 0 900    5700 2 60     2200  
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i.pp.i 1 49   1600 370 - - - - 0 910    5900 0 34     1100  
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i.pp.i 0 680   950 7900 - - - - 0 .67 44 0 .019 4.9
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i.pp.i 2 34   1100 250 - - - - 0 920    6100 2 35     970  
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i.pp.i 2 34   1300 250 - - - - 0 900    6000 2 34     1100  
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.c 0 820   15000 8300 0 .75 46 0 .038 4.8 0 .87 49 0 .0020 .27 - -
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.c 0 900   1900 7300 0 .56 43 0 .018 4.9 0 .87 48 0 .0011 .32 - -
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.c 0 900   4800 9300 0 .68 41 0 .020 4.9 0 .85 49 0 .0018 .27 - -
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.c 0 5.8 360 45 0 .53 41 0 .019 4.8 0 .88 50 0 .0011 .26 - -
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.c 0 900   5200 10000 0 .55 41 0 .018 4.8 0 1.1  49 0 .0016 .26 - -
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.c 0 900   5900 9700 0 .56 43 0 .019 4.8 0 .86 48 0 .0015 .26 - -
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.c 0 12   310 94 0 .66 41 0 .018 4.8 0 .88 51 0 .0016 .30 - -
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.c 0 900   5300 13000 0 .53 43 0 .018 4.9 0 .89 49 0 .0016 .28 - -
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.c 0 200   1100 1600 0 .92 43 0 .019 4.8 0 1.1  52 0 .0017 .27 - -
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.c 0 900   5100 7500 0 .53 42 0 .018 4.9 0 .89 50 0 .0012 .34 - -
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.c 0 160   1100 1300 0 .53 41 0 .018 4.9 0 1.1  50 0 .0017 .27 - -
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.c 0 800   3700 7900 0 .62 44 0 .020 4.8 0 1.1  49 0 .0017 .28 - -
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.c 0 900   4700 9300 0 .58 42 0 .025 4.9 0 .86 47 0 .0015 .27 - -
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.c 0 28   580 220 0 .69 43 0 .019 4.8 0 .96 50 0 .0020 .27 - -
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.c 0 900   5500 8100 0 .65 43 0 .025 4.8 0 .85 50 0 .0017 .28 - -
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.c 0 900   4000 8600 0 .52 45 0 .019 4.9 0 .94 49 0 .0017 .28 - -
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.c 0 900   9900 8000 0 .59 43 0 .018 4.8 0 1.1  50 0 .0017 .28 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-media-video-vivi.cil.out.c 0 12   530 94 0 .53 43 0 .019 4.9 0 .84 49 0 .0013 .27 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.c 0 11   480 87 0 .52 41 0 .018 5.0 0 .97 47 0 .0020 .29 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.c 0 13   600 110 0 .66 41 0 .018 4.9 0 .80 47 0 .0018 .30 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.c 0 14   650 100 0 .65 42 0 .019 4.9 0 1.0  49 0 .0016 .29 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-p54-p54usb.cil.out.c 0 13   610 110 0 .43 43 0 .018 4.9 0 1.0  49 0 .0017 .27 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-staging-media-dt3155v4l-dt3155v4l.cil.out.c 0 12   590 100 0 .52 41 0 .026 4.9 0 .85 49 0 .0017 .27 - -
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-usb-image-microtek.cil.out.c 0 12   590 120 0 .57 44 0 .018 4.9 0 .93 47 0 .0016 .29 - -
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.c 0 900   3200 11000 0 .67 45 0 .023 5.0 0 .92 50 0 .0012 .26 - -
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.c 0 170   1100 1300 0 94    2600 0 96     810   0 8.1  310 0 2.1    30    - -
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.c 0 900   7000 8200 0 .53 43 0 .024 4.9 0 .99 48 0 .0015 .29 - -
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.c 0 900   5900 9400 0 .67 43 0 .019 4.8 0 .84 47 0 .0014 .27 - -
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.c 0 110   1200 920 0 .58 42 0 .049 4.9 0 .95 47 0 .0019 .26 - -
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.c 0 90   1500 660 0 .53 41 0 .024 4.9 0 .88 49 0 .0018 .28 - -
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.c 2 12   530 88 - - - - 0 680    7000 2 17     500  
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.c 2 7.9 380 69 - - - - 0 900    6700 2 8.5   340  
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.c 2 13   520 97 - - - - 0 450    7000 2 14     460  
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.c 1 13   530 110 - - - - 0 900    6600 0 57     640  
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.c 2 11   470 95 - - - - 0 810    7000 2 11     410  
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.c 2 11   570 97 - - - - 0 580    7000 2 11     500  
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.c 2 9.9 440 73 - - - - 0 900    3200 2 10     370  
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.c 2 6.4 300 55 - - - - 0 910    7000 2 6.4   280  
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.c 2 12   540 98 - - - - 0 880    7000 2 15     490  
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.c 2 23   850 170 - - - - 0 760    7000 2 24     700  
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.c 2 16   560 130 - - - - 0 920    6800 2 17     520  
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.c 2 17   650 130 - - - - 0 610    7000 2 29     580  
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.c 2 22   700 160 - - - - 0 790    7000 2 22     600  
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.c 2 16   570 120 - - - - 0 910    6700 2 19     520  
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.c 2 11   510 80 - - - - 0 620    7000 2 8.6   480  
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.c 2 13   540 110 - - - - 0 780    7000 2 18     510  
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.c 2 23   720 170 - - - - 0 600    7000 2 27     630  
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.c 2 21   640 160 - - - - 0 920    7000 2 25     610  
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.c 2 19   680 160 - - - - 0 920    6800 2 24     620  
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.c 2 12   530 90 - - - - 0 680    7000 2 15     480  
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.c 2 19   650 150 - - - - 0 770    7000 2 23     600  
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.c 2 33   1100 250 - - - - 0 850    7000 2 33     910  
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.c 2 8.6 370 67 - - - - 0 900    3500 2 9.9   340  
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.c 2 22   1100 180 - - - - 0 900    6000 2 31     1000  
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.c 2 7.0 320 61 - - - - 0 700    7000 2 7.1   300  
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.c 2 10   500 84 - - - - 0 900    6000 2 12     470  
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.c 2 7.1 340 65 - - - - 0 900    5000 2 7.9   320  
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.c 2 6.2 320 46 - - - - 0 430    7000 2 7.0   290  
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.c 2 13   550 110 - - - - 0 700    7000 2 15     490  
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.c 2 9.7 430 74 - - - - 0 750    7000 2 9.1   380  
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.c 2 8.5 400 64 - - - - 0 900    5800 2 9.2   360  
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.c 2 8.9 410 67 - - - - 0 900    5000 2 9.1   360  
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.c 2 7.5 360 56 - - - - 0 400    7000 2 7.3   330  
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.c 2 9.1 430 75 - - - - 0 640    7000 2 11     390  
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.c 2 13   510 110 - - - - 0 900    4700 2 16     490  
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.c 2 11   480 81 - - - - 0 570    7000 2 11     380  
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.c 2 7.5 360 59 - - - - 0 490    7000 2 9.7   320  
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.c 2 8.0 380 56 - - - - 0 340    7000 2 8.1   330  
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.c 2 8.3 370 68 - - - - 0 510    7000 2 9.3   350  
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.c 2 7.0 350 56 - - - - 0 330    7000 2 7.4   320  
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.c 2 7.9 360 60 - - - - 0 410    7000 2 8.7   340  
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.c 2 9.2 410 73 - - - - 0 910    6800 2 9.2   350  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-kensington.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 2 7.8 360 66 - - - - 0 310    7000 2 8.4   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-keytouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 2 8.5 370 74 - - - - 0 340    7000 2 9.3   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-lcpower.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 2 8.1 360 70 - - - - 0 860    7000 2 8.6   330  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-monterey.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 2 7.6 370 61 - - - - 0 320    7000 2 8.7   340  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-ortek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 2 7.6 350 64 - - - - 0 320    7000 2 8.8   310  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-petalynx.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 2 8.7 410 65 - - - - 0 380    7000 2 9.1   370  
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hid--hid-primax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c 2