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-17.0954
Test setintegration-predicateAnalysis-abm
branch-r5639
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2222904.182158.821627.9771191.142
correct results1791927.541275.801212.238812.920
false negatives00000
false positives1941.6923.7518.4902.850
score (222 files, max score: 360)245
pthread/fib_bench_BUG.cil.cunknown1.600.900.625s0.028s
pthread/fib_bench_longer_BUG.cil.cunknown1.700.960.679s0.026s
pthread/queue_BUG.cil.cunknown1.901.090.823s0.124s
pthread/reorder_5_BUG.cil.cunknown2.071.110.825s0.127s
pthread/twostage_3_BUG.cil.cunknown2.071.170.883s0.136s
pthread/fib_bench.cil.cunknown1.860.960.699s0.028s
pthread/fib_bench_longer.cil.cunknown1.650.920.641s0.027s
pthread/queue_ok.cil.cunknown1.881.070.786s0.104s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe16.5110.159.766s6.849s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe8.744.594.226s2.215s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe9.434.814.459s2.332s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.222.542.196s1.028s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe12.687.186.830s4.341s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.745.745.428s3.574s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.325.154.840s3.049s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.966.405.996s3.821s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.421.961.556s0.508s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe5.192.752.373s0.987s
ntdrivers/cdaudio.BUG.i.cil.cunsafe15.418.057.676s4.386s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.585.965.588s2.998s
ntdrivers/floppy.BUG.i.cil.cunsafe12.736.656.233s2.971s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.263.573.239s1.389s
ntdrivers/parport.BUG.i.cil.cunsafe20.5012.7212.284s6.403s
ntdrivers/cdaudio.i.cil.csafe18.5911.1810.724s6.626s
ntdrivers/diskperf.i.cil.csafe12.146.346.016s3.504s
ntdrivers/floppy.i.cil.csafe15.018.748.378s4.454s
ntdrivers/parport.i.cil.csafe28.2418.9918.494s11.495s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.953.443.102s1.842s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.843.292.894s1.509s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.763.112.740s1.424s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.192.221.943s0.914s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe20.3315.6715.300s11.633s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe62.4157.8557.375s52.045s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.55119.58--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.0213.2812.899s10.160s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.302.392.096s0.987s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.892.662.381s1.218s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.151.230.958s0.050s
ssh-simplified/s3_clnt_1.cil.csafe10.467.236.891s4.747s
ssh-simplified/s3_clnt_2.cil.csafe9.445.955.653s3.643s
ssh-simplified/s3_clnt_3.cil.csafe7.924.724.301s2.625s
ssh-simplified/s3_clnt_4.cil.csafe11.798.117.771s5.018s
ssh-simplified/s3_srvr_1a.cil.csafe4.662.482.142s1.302s
ssh-simplified/s3_srvr_1b.cil.csafe2.041.160.909s0.237s
ssh-simplified/s3_srvr_1.cil.cout of memory73.3868.89--
ssh-simplified/s3_srvr_3.cil.csafe25.7120.2419.785s14.512s
ssh-simplified/s3_srvr_4.cil.csafe10.616.336.005s4.583s
ssh-simplified/s3_srvr_6.cil.ctimeout119.69115.76--
ssh-simplified/s3_srvr_7.cil.cunknown68.0365.3165.018s63.962s
ssh-simplified/s3_srvr_8.cil.csafe16.1311.8211.445s8.416s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.603.533.208s1.628s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.802.632.347s1.060s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.992.472.201s1.036s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.832.712.424s1.186s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.792.692.396s1.195s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe5.002.402.141s1.072s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe5.012.462.198s1.107s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.662.392.118s0.961s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe6.202.992.724s1.392s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown66.3562.2561.948s60.594s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe26.2720.6820.254s18.205s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.9831.0230.623s27.736s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.082.762.477s1.205s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe12.247.897.579s5.924s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe29.3224.1223.706s21.316s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.903.623.311s1.976s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe18.6414.0413.656s11.619s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.133.202.923s1.634s
ssh/s3_clnt.blast.01.i.cil.csafe9.045.084.795s3.151s
ssh/s3_clnt.blast.03.i.cil.csafe12.929.058.756s6.033s
ssh/s3_clnt.blast.04.i.cil.csafe11.397.427.111s4.068s
ssh/s3_srvr.blast.01.i.cil.csafe32.5127.9427.544s23.334s
ssh/s3_srvr.blast.06.i.cil.csafe25.3020.0219.609s14.755s
ssh/s3_srvr.blast.07.i.cil.cunknown67.1663.8263.527s61.960s
ssh/s3_srvr.blast.08.i.cil.csafe23.6518.1317.741s14.111s
ssh/s3_srvr.blast.09.i.cil.cunknown65.9661.6861.366s59.272s
ssh/s3_srvr.blast.10.i.cil.csafe11.877.076.724s5.008s
ssh/s3_srvr.blast.12.i.cil.csafe13.448.948.545s6.817s
ssh/s3_srvr.blast.13.i.cil.cunknown65.6761.4761.170s59.212s
ssh/s3_srvr.blast.14.i.cil.csafe36.4731.1930.778s24.735s
ssh/s3_srvr.blast.15.i.cil.csafe15.8611.1710.808s5.770s
ssh/s3_srvr.blast.16.i.cil.csafe40.5135.2034.765s24.516s
locks/test_locks_14.BUG.cunsafe2.451.441.171s0.430s
locks/test_locks_15.BUG.cunsafe2.591.491.201s0.479s
locks/test_locks_10.csafe2.011.130.892s0.245s
locks/test_locks_11.csafe2.151.210.958s0.282s
locks/test_locks_12.csafe2.221.271.002s0.367s
locks/test_locks_13.csafe2.381.341.092s0.387s
locks/test_locks_14.csafe2.381.421.156s0.440s
locks/test_locks_15.csafe2.641.491.242s0.479s
locks/test_locks_5.csafe1.740.970.711s0.098s
locks/test_locks_6.csafe1.821.020.785s0.128s
locks/test_locks_7.csafe1.731.010.774s0.147s
locks/test_locks_8.csafe1.921.110.860s0.193s
locks/test_locks_9.csafe1.941.110.875s0.213s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.351.311.024s0.168s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.860.960.719s0.085s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.021.070.833s0.151s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.481.331.083s0.213s
heap-manipulation/dll_of_dll.cil.cunknown2.031.100.846s0.099s
heap-manipulation/merge_sort.cil.csafe2.081.130.836s0.072s
heap-manipulation/sll_to_dll_rev.cil.cunknown14.3512.3712.091s9.436s
list-properties/alternating_list.cil.csafe2.021.120.839s0.170s
list-properties/list.cil.csafe2.051.070.826s0.249s
list-properties/list_flag.cil.csafe2.001.060.820s0.165s
list-properties/simple.cil.cunsafe2.011.150.871s0.172s
list-properties/simple_built_from_end.cil.cunsafe1.931.120.875s0.164s
list-properties/splice.cil.cunsafe3.612.312.048s0.778s
systemc/token_ring.01.BUG.cil.cunsafe3.361.911.634s0.542s
systemc/token_ring.02.BUG.cil.cunsafe5.542.682.396s1.178s
systemc/token_ring.03.BUG.cil.cunsafe7.263.933.663s1.938s
systemc/transmitter.01.BUG.cil.cunsafe2.621.411.150s0.338s
systemc/transmitter.02.BUG.cil.cunsafe3.512.071.797s0.707s
systemc/transmitter.03.BUG.cil.cunsafe4.602.282.021s0.796s
systemc/transmitter.04.BUG.cil.cunsafe5.612.772.497s1.078s
systemc/bist_cell.cil.csafe19.3115.4615.171s13.151s
systemc/kundu.cil.csafe67.9360.9860.632s56.993s
systemc/mem_slave_tlm.1.cil.cexception44.1338.40--
systemc/mem_slave_tlm.2.cil.csafe66.4661.4861.128s58.885s
systemc/mem_slave_tlm.4.cil.ctimeout119.69113.30--
systemc/pc_sfifo_1.cil.csafe5.863.012.762s1.502s
systemc/pc_sfifo_2.cil.csafe9.565.295.019s3.109s
systemc/pc_sfifo_3.cil.csafe8.444.614.315s2.519s
systemc/token_ring.01.cil.csafe9.625.525.248s3.065s
systemc/token_ring.04.cil.csafe66.5161.2760.931s58.173s
systemc/toy.cil.csafe66.7661.1760.841s58.367s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.473.211.578s0.032s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.704.061.622s0.061s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.413.182.132s0.016s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.380.82--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.841.280.951s0.024s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.700.910.629s0.017s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.630.930.671s0.042s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.760.970.699s0.037s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.561.401.127s0.253s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.861.711.380s0.533s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.720.960.688s0.044s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.600.960.686s0.040s
ldv-regression/alias_of_return.c-safe.cil.csafe1.680.960.673s0.040s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.730.950.648s0.025s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.680.970.683s0.036s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.720.970.689s0.018s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.371.441.168s0.301s
ldv-regression/just_assert.c-safe.cil.csafe1.540.840.587s0.015s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.560.870.624s0.017s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.641.020.764s0.024s
ldv-regression/nested_structure-safe.cil.cunsafe1.720.990.721s0.046s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.670.960.672s0.022s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.550.910.627s0.020s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.801.080.766s0.030s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe2.141.361.021s0.107s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.841.110.787s0.029s
ldv-regression/oomInt.c-safe.cil.csafe1.610.930.653s0.034s
ldv-regression/oomInt.c-safe_1.cil.csafe1.731.040.754s0.032s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.680.990.697s0.054s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.780.950.709s0.032s
ldv-regression/rule60_list2.c-safe.cil.csafe2.321.321.062s0.257s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.660.940.681s0.033s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.720.940.666s0.024s
ldv-regression/test_address.c-safe.cil.cunsafe1.600.970.648s0.022s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.660.910.648s0.025s
ldv-regression/test_malloc-1-safe.cil.csafe1.811.000.683s0.031s
ldv-regression/test_malloc-2-safe.cil.csafe1.540.800.570s0.027s
ldv-regression/test_overflow.c-safe.cil.csafe1.720.970.723s0.030s
ldv-regression/test_union.c-safe.cil.csafe1.780.990.711s0.046s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.480.820.558s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.740.980.697s0.020s
ldv-regression/test_union_cast-2-safe.cil.csafe1.680.910.658s0.024s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.770.960.704s0.021s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.580.950.678s0.019s
ldv-regression/volatile_alias.c-safe.cil.csafe1.590.860.615s0.023s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.710.890.606s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.552.482.160s0.441s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.522.352.058s0.428s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.622.452.151s0.458s
ddv-machzwd/ddv_machzwd_inb.cil.csafe4.132.141.788s0.493s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.952.021.701s0.434s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.082.041.748s0.475s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.112.021.752s0.451s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.932.071.740s0.429s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe4.182.041.752s0.456s
ddv-machzwd/ddv_machzwd_outl.cil.csafe4.092.001.727s0.456s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.901.991.689s0.402s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.012.031.701s0.433s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.001.981.680s0.437s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe16.977.757.386s0.575s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe13.076.616.200s2.214s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe16.097.807.450s3.142s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe15.795.845.538s0.686s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe20.8510.9510.564s3.571s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe11.104.814.463s1.565s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe20.4111.3810.927s4.800s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe9.193.953.674s0.234s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe24.199.158.812s1.172s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.897.056.673s2.949s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe44.2028.1127.750s11.506s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe7.883.573.224s0.622s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe19.3912.1411.772s4.990s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe6.973.413.022s1.079s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe19.779.979.489s6.630s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe18.678.688.339s1.394s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe38.3821.9521.495s12.273s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe12.186.516.140s3.763s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe14.107.827.356s4.373s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe21.1810.269.914s1.229s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.522.171.890s0.643s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe7.843.593.279s1.284s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe20.9410.709.082s5.915s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe5.382.672.405s0.822s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe16.057.497.094s4.548s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown86.4763.2162.713s59.509s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe20.769.989.555s6.117s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe10.084.884.560s2.149s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe6.342.942.623s1.014s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe9.754.153.785s1.647s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe5.162.582.261s0.876s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe20.458.858.500s3.880s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.732.352.075s0.536s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe24.9015.3414.985s4.935s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.962.111.799s0.272s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe14.026.415.422s2.582s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe7.343.092.821s1.141s