ToolCPAchecker 1.1-svn
Limitstimelimit: 120 s, memlimit: 3000 MB
Systemhost: pc-wehr-serv1
os: Linux 3.0.0-15-generic x86_64
cpu: Intel(R) Core(TM) i7-2600 CPU @ 3.40GHz
cores: 4, frequency: 3401 MHz, ram: 16408608 kB
Date of run12-02-16.0901
Test setintegration-predicateAnalysis-abm
branch-r5623
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2222856.112107.121709.8851276.956
correct results1802012.771357.741299.713903.905
false negatives00000
false positives1943.6823.9718.7662.921
score (222 files, max score: 360)247
pthread/fib_bench_BUG.cil.cunknown1.220.730.505s0.025s
pthread/fib_bench_longer_BUG.cil.cunknown1.240.730.505s0.030s
pthread/queue_BUG.cil.cunknown1.430.850.608s0.082s
pthread/reorder_5_BUG.cil.cunknown1.560.910.665s0.107s
pthread/twostage_3_BUG.cil.cunknown1.911.090.833s0.149s
pthread/fib_bench.cil.cunknown1.390.770.548s0.025s
pthread/fib_bench_longer.cil.cunknown1.530.910.644s0.030s
pthread/queue_ok.cil.cunknown1.971.050.799s0.092s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe15.739.969.622s6.669s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe8.264.243.947s2.101s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe10.075.434.962s2.614s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.092.532.176s0.976s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.928.037.605s4.957s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.455.845.525s3.598s
ntdrivers-simplified/floppy_simpl3.cil.csafe9.855.084.776s2.878s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.686.225.882s3.751s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.161.811.444s0.506s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.642.352.066s0.918s
ntdrivers/cdaudio.BUG.i.cil.cunsafe14.887.967.600s4.247s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.326.115.775s2.969s
ntdrivers/floppy.BUG.i.cil.cunsafe12.856.846.486s3.048s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.323.663.311s1.354s
ntdrivers/parport.BUG.i.cil.cunsafe20.5712.5512.030s6.665s
ntdrivers/cdaudio.i.cil.csafe17.4210.249.868s6.154s
ntdrivers/diskperf.i.cil.csafe11.716.466.132s3.679s
ntdrivers/floppy.i.cil.csafe14.448.598.245s4.405s
ntdrivers/parport.i.cil.csafe27.2618.1217.686s10.451s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.723.252.981s1.860s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.313.002.723s1.473s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.783.012.710s1.419s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.342.472.200s1.028s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe19.1414.7814.338s11.034s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe64.4057.6557.174s51.496s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.63115.14--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.4213.2112.853s10.080s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.182.241.960s0.940s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.922.582.309s1.258s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.161.120.863s0.052s
ssh-simplified/s3_clnt_1.cil.csafe10.887.256.964s4.843s
ssh-simplified/s3_clnt_2.cil.csafe9.125.625.316s3.323s
ssh-simplified/s3_clnt_3.cil.csafe7.924.444.151s2.617s
ssh-simplified/s3_clnt_4.cil.csafe12.188.428.121s5.254s
ssh-simplified/s3_srvr_1a.cil.csafe5.012.652.316s1.480s
ssh-simplified/s3_srvr_1b.cil.csafe2.051.170.893s0.246s
ssh-simplified/s3_srvr_1.cil.cout of memory64.6660.28--
ssh-simplified/s3_srvr_3.cil.csafe24.9719.2618.835s13.745s
ssh-simplified/s3_srvr_4.cil.csafe9.816.095.737s4.341s
ssh-simplified/s3_srvr_6.cil.ctimeout119.64114.78--
ssh-simplified/s3_srvr_7.cil.cunknown65.0361.6761.368s60.277s
ssh-simplified/s3_srvr_8.cil.csafe15.7511.1710.835s7.988s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.773.423.120s1.595s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.752.642.362s1.139s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.512.292.018s0.926s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.602.722.433s1.230s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.712.602.333s1.120s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.632.352.078s0.981s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.902.582.311s1.171s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.802.582.284s1.073s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe6.063.212.903s1.404s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown65.7361.5361.221s59.862s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe24.9419.7319.328s17.326s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.2529.9929.559s26.730s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.902.682.429s1.192s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.027.056.746s5.380s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe27.6822.2821.842s19.843s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.993.453.173s1.917s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe17.9913.2412.880s11.020s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.223.303.036s1.790s
ssh/s3_clnt.blast.01.i.cil.csafe8.014.844.557s2.928s
ssh/s3_clnt.blast.03.i.cil.csafe12.748.638.353s5.844s
ssh/s3_clnt.blast.04.i.cil.csafe11.167.056.781s3.922s
ssh/s3_srvr.blast.01.i.cil.csafe33.7328.5828.207s23.913s
ssh/s3_srvr.blast.06.i.cil.csafe24.8519.5119.072s14.258s
ssh/s3_srvr.blast.07.i.cil.cunknown64.5761.0260.735s59.343s
ssh/s3_srvr.blast.08.i.cil.csafe23.4117.9217.530s14.050s
ssh/s3_srvr.blast.09.i.cil.cunknown65.5161.1560.821s58.914s
ssh/s3_srvr.blast.10.i.cil.csafe12.137.687.333s5.257s
ssh/s3_srvr.blast.12.i.cil.csafe14.989.959.548s7.525s
ssh/s3_srvr.blast.13.i.cil.cunknown67.0662.8262.477s60.633s
ssh/s3_srvr.blast.14.i.cil.csafe36.4130.8730.440s24.801s
ssh/s3_srvr.blast.15.i.cil.csafe16.3310.7910.430s5.530s
ssh/s3_srvr.blast.16.i.cil.csafe42.0736.9236.480s26.233s
locks/test_locks_14.BUG.cunsafe2.681.551.286s0.437s
locks/test_locks_15.BUG.cunsafe2.861.671.367s0.532s
locks/test_locks_10.csafe2.221.291.011s0.270s
locks/test_locks_11.csafe2.411.411.104s0.338s
locks/test_locks_12.csafe2.611.511.145s0.376s
locks/test_locks_13.csafe2.561.491.231s0.383s
locks/test_locks_14.csafe2.481.441.190s0.424s
locks/test_locks_15.csafe2.461.391.140s0.473s
locks/test_locks_5.csafe1.841.020.743s0.105s
locks/test_locks_6.csafe1.841.030.798s0.136s
locks/test_locks_7.csafe1.951.140.887s0.188s
locks/test_locks_8.csafe2.081.240.942s0.193s
locks/test_locks_9.csafe2.201.321.053s0.257s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.641.501.249s0.244s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.031.100.765s0.141s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.331.461.135s0.202s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.721.481.188s0.196s
heap-manipulation/dll_of_dll.cil.cunknown2.121.230.873s0.113s
heap-manipulation/merge_sort.cil.csafe2.191.170.891s0.088s
heap-manipulation/sll_to_dll_rev.cil.cunknown14.0512.3312.071s9.015s
list-properties/alternating_list.cil.csafe2.151.150.871s0.184s
list-properties/list.cil.csafe2.441.361.073s0.249s
list-properties/list_flag.cil.csafe2.201.180.872s0.218s
list-properties/simple.cil.cunsafe2.261.230.962s0.172s
list-properties/simple_built_from_end.cil.cunsafe2.041.180.879s0.172s
list-properties/splice.cil.cunsafe3.902.622.352s0.946s
systemc/token_ring.01.BUG.cil.cunsafe3.411.931.644s0.579s
systemc/token_ring.02.BUG.cil.cunsafe5.342.852.589s1.279s
systemc/token_ring.03.BUG.cil.cunsafe7.284.043.761s2.147s
systemc/transmitter.01.BUG.cil.cunsafe2.591.411.155s0.341s
systemc/transmitter.02.BUG.cil.cunsafe3.521.961.693s0.694s
systemc/transmitter.03.BUG.cil.cunsafe4.912.692.362s0.994s
systemc/transmitter.04.BUG.cil.cunsafe6.293.323.052s1.285s
systemc/bist_cell.cil.csafe19.9816.8116.519s14.426s
systemc/kundu.cil.csafe68.3060.9560.636s57.309s
systemc/mem_slave_tlm.1.cil.cexception43.4837.94--
systemc/mem_slave_tlm.2.cil.csafe76.6472.1671.799s68.074s
systemc/mem_slave_tlm.4.cil.csafe96.1995.1293.777s87.155s
systemc/pc_sfifo_1.cil.csafe6.103.222.939s1.585s
systemc/pc_sfifo_2.cil.csafe9.815.695.391s3.341s
systemc/pc_sfifo_3.cil.csafe8.974.944.657s2.772s
systemc/token_ring.01.cil.csafe9.445.345.080s2.880s
systemc/token_ring.04.cil.csafe65.9860.9160.608s57.708s
systemc/toy.cil.csafe70.3462.7962.450s60.310s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.570.890.619s0.031s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.560.930.671s0.069s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.730.980.724s0.017s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.200.69--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.780.960.682s0.023s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.730.930.688s0.031s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.570.860.606s0.040s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.720.970.724s0.042s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.501.431.125s0.281s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.451.411.154s0.450s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.650.920.666s0.055s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.510.860.615s0.041s
ldv-regression/alias_of_return.c-safe.cil.csafe1.630.950.692s0.041s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.710.990.674s0.020s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.700.930.670s0.037s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.580.880.621s0.028s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.251.270.965s0.240s
ldv-regression/just_assert.c-safe.cil.csafe1.680.880.616s0.015s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.870.970.690s0.021s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.600.930.660s0.027s
ldv-regression/nested_structure-safe.cil.cunsafe1.731.040.741s0.049s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.820.990.724s0.026s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.780.960.701s0.016s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.760.960.684s0.020s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe2.001.140.862s0.109s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.650.900.660s0.028s
ldv-regression/oomInt.c-safe.cil.csafe1.560.920.653s0.041s
ldv-regression/oomInt.c-safe_1.cil.csafe1.640.940.610s0.034s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.650.980.720s0.056s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.680.930.665s0.028s
ldv-regression/rule60_list2.c-safe.cil.csafe2.201.260.986s0.229s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.610.860.587s0.029s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.820.960.686s0.020s
ldv-regression/test_address.c-safe.cil.cunsafe1.730.960.683s0.026s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.480.830.583s0.023s
ldv-regression/test_malloc-1-safe.cil.csafe1.650.890.649s0.033s
ldv-regression/test_malloc-2-safe.cil.csafe1.640.900.642s0.030s
ldv-regression/test_overflow.c-safe.cil.csafe1.670.900.656s0.031s
ldv-regression/test_union.c-safe.cil.csafe1.650.910.665s0.023s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.660.920.654s0.021s
ldv-regression/test_union_cast-1-safe.cil.csafe1.390.780.538s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.730.920.672s0.036s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.760.970.709s0.032s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.750.950.679s0.026s
ldv-regression/volatile_alias.c-safe.cil.csafe1.711.010.703s0.023s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.660.910.594s0.018s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.172.282.012s0.379s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.492.592.332s0.548s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.612.402.126s0.479s
ddv-machzwd/ddv_machzwd_inb.cil.csafe4.082.101.772s0.445s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.022.011.716s0.435s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.872.051.757s0.433s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.991.931.590s0.415s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.142.121.842s0.415s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.992.151.841s0.561s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.861.951.656s0.443s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.722.041.762s0.499s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.801.911.634s0.407s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.901.931.651s0.400s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe15.367.106.786s0.569s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe12.046.035.727s2.220s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.477.056.719s2.898s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe15.225.835.517s0.701s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe20.7310.5810.240s3.253s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe11.775.254.887s1.776s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe22.2313.1511.958s5.047s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe8.963.863.535s0.306s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe21.688.337.958s1.132s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe13.437.196.825s3.286s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe42.9927.6927.301s10.172s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe8.233.603.314s0.708s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe18.9511.4311.066s4.146s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe6.333.092.747s0.966s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe18.109.729.314s6.542s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe17.757.937.583s1.408s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe34.3818.9318.514s10.958s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.705.525.195s3.217s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe13.536.966.615s3.883s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe21.7310.079.715s1.257s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.472.372.067s0.866s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe7.323.583.245s1.391s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe19.739.759.342s6.049s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe5.262.592.301s0.795s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe15.777.527.133s4.351s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown88.2364.3263.901s60.426s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe23.6110.249.883s5.967s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.414.624.326s2.109s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.962.792.497s0.940s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.623.623.303s1.403s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.612.211.929s0.661s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe19.408.378.028s3.700s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe5.282.402.129s0.550s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe22.7013.2112.847s5.061s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.262.101.837s0.202s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe14.286.536.159s3.227s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe7.483.573.281s1.408s