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.0841
Test setintegration-predicateAnalysis-abm
branch-r5630
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2222870.552116.671608.9691184.480
correct results1791913.291255.511198.402809.454
false negatives00000
false positives1941.6922.7917.5562.744
score (222 files, max score: 360)245
pthread/fib_bench_BUG.cil.cunknown1.250.720.506s0.025s
pthread/fib_bench_longer_BUG.cil.cunknown1.230.730.508s0.025s
pthread/queue_BUG.cil.cunknown1.740.990.725s0.098s
pthread/reorder_5_BUG.cil.cunknown1.861.020.755s0.109s
pthread/twostage_3_BUG.cil.cunknown1.900.990.746s0.114s
pthread/fib_bench.cil.cunknown1.330.790.556s0.034s
pthread/fib_bench_longer.cil.cunknown1.290.760.505s0.031s
pthread/queue_ok.cil.cunknown1.901.050.769s0.088s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe16.309.949.577s6.513s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.183.633.348s1.713s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe9.044.303.988s2.132s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.412.712.340s1.077s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.667.527.141s4.625s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.525.865.544s3.557s
ntdrivers-simplified/floppy_simpl3.cil.csafe9.985.244.922s3.054s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.616.075.737s3.625s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.901.641.376s0.490s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.732.482.163s0.933s
ntdrivers/cdaudio.BUG.i.cil.cunsafe14.947.837.463s4.204s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.385.955.579s2.913s
ntdrivers/floppy.BUG.i.cil.cunsafe12.916.896.419s2.917s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.663.983.576s1.451s
ntdrivers/parport.BUG.i.cil.cunsafe20.0711.6511.232s5.687s
ntdrivers/cdaudio.i.cil.csafe17.1910.059.697s5.928s
ntdrivers/diskperf.i.cil.csafe12.556.766.427s3.795s
ntdrivers/floppy.i.cil.csafe15.399.238.866s4.691s
ntdrivers/parport.i.cil.csafe27.7718.8418.398s11.692s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.423.102.804s1.691s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.932.832.517s1.302s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.632.872.564s1.370s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.282.352.058s0.930s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.7213.8313.477s10.201s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe64.5958.3357.850s51.657s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.58115.08--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe17.7913.2912.943s10.258s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.182.392.141s0.959s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.992.552.274s1.249s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.121.110.852s0.057s
ssh-simplified/s3_clnt_1.cil.csafe10.666.796.498s4.522s
ssh-simplified/s3_clnt_2.cil.csafe8.785.505.228s3.148s
ssh-simplified/s3_clnt_3.cil.csafe8.164.514.230s2.678s
ssh-simplified/s3_clnt_4.cil.csafe11.808.157.880s5.041s
ssh-simplified/s3_srvr_1a.cil.csafe4.522.332.021s1.298s
ssh-simplified/s3_srvr_1b.cil.csafe1.981.070.814s0.217s
ssh-simplified/s3_srvr_1.cil.cout of memory64.2159.69--
ssh-simplified/s3_srvr_3.cil.csafe24.8019.4418.995s13.854s
ssh-simplified/s3_srvr_4.cil.csafe10.136.285.906s4.398s
ssh-simplified/s3_srvr_6.cil.ctimeout119.56114.56--
ssh-simplified/s3_srvr_7.cil.cunknown64.6861.7161.414s60.337s
ssh-simplified/s3_srvr_8.cil.csafe14.8910.7210.375s7.659s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.232.972.692s1.403s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.742.412.148s0.996s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.802.492.213s1.073s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.662.672.393s1.172s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.912.872.603s1.273s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.772.472.164s0.957s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.652.261.995s0.963s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.732.271.998s0.927s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.743.122.840s1.431s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown66.5062.5662.217s60.830s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe26.0220.5420.129s18.110s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.1430.6430.219s27.421s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.852.722.456s1.208s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe10.777.196.876s5.327s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe28.4223.0522.666s20.777s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.863.583.308s1.985s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe17.9813.3312.978s11.091s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.323.373.106s1.774s
ssh/s3_clnt.blast.01.i.cil.csafe8.014.914.629s2.992s
ssh/s3_clnt.blast.03.i.cil.csafe12.078.438.138s5.654s
ssh/s3_clnt.blast.04.i.cil.csafe10.876.956.683s3.919s
ssh/s3_srvr.blast.01.i.cil.csafe32.6427.6927.334s23.168s
ssh/s3_srvr.blast.06.i.cil.csafe25.4219.9719.538s14.602s
ssh/s3_srvr.blast.07.i.cil.cunknown66.0962.1861.888s60.435s
ssh/s3_srvr.blast.08.i.cil.csafe23.4318.3717.978s14.386s
ssh/s3_srvr.blast.09.i.cil.cunknown66.8462.1261.797s59.816s
ssh/s3_srvr.blast.10.i.cil.csafe11.797.186.776s4.937s
ssh/s3_srvr.blast.12.i.cil.csafe14.689.709.335s7.378s
ssh/s3_srvr.blast.13.i.cil.cunknown66.7561.9161.582s59.855s
ssh/s3_srvr.blast.14.i.cil.csafe36.1230.9230.491s24.539s
ssh/s3_srvr.blast.15.i.cil.csafe15.1610.6810.297s5.523s
ssh/s3_srvr.blast.16.i.cil.csafe42.4037.0936.666s26.843s
locks/test_locks_14.BUG.cunsafe2.751.601.346s0.449s
locks/test_locks_15.BUG.cunsafe2.781.611.353s0.515s
locks/test_locks_10.csafe1.921.080.832s0.234s
locks/test_locks_11.csafe2.251.291.018s0.308s
locks/test_locks_12.csafe2.381.341.086s0.358s
locks/test_locks_13.csafe2.321.311.061s0.372s
locks/test_locks_14.csafe2.631.471.213s0.455s
locks/test_locks_15.csafe2.741.571.319s0.527s
locks/test_locks_5.csafe1.901.190.905s0.105s
locks/test_locks_6.csafe1.861.070.802s0.123s
locks/test_locks_7.csafe2.181.260.954s0.163s
locks/test_locks_8.csafe2.071.230.976s0.197s
locks/test_locks_9.csafe2.221.270.959s0.226s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.761.581.198s0.201s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.161.190.869s0.112s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.321.381.118s0.238s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.751.561.287s0.256s
heap-manipulation/dll_of_dll.cil.cunknown2.141.120.820s0.121s
heap-manipulation/merge_sort.cil.csafe1.971.080.818s0.078s
heap-manipulation/sll_to_dll_rev.cil.cunknown13.7412.1311.746s8.936s
list-properties/alternating_list.cil.csafe2.221.190.907s0.182s
list-properties/list.cil.csafe2.021.120.876s0.240s
list-properties/list_flag.cil.csafe2.171.250.988s0.208s
list-properties/simple.cil.cunsafe1.921.020.777s0.174s
list-properties/simple_built_from_end.cil.cunsafe2.021.110.845s0.143s
list-properties/splice.cil.cunsafe3.672.372.080s0.806s
systemc/token_ring.01.BUG.cil.cunsafe3.071.681.413s0.511s
systemc/token_ring.02.BUG.cil.cunsafe6.333.142.831s1.378s
systemc/token_ring.03.BUG.cil.cunsafe7.263.853.581s1.997s
systemc/transmitter.01.BUG.cil.cunsafe2.691.561.285s0.390s
systemc/transmitter.02.BUG.cil.cunsafe3.872.211.914s0.789s
systemc/transmitter.03.BUG.cil.cunsafe4.812.552.243s0.903s
systemc/transmitter.04.BUG.cil.cunsafe6.333.212.924s1.209s
systemc/bist_cell.cil.csafe20.3916.8816.583s14.482s
systemc/kundu.cil.csafe68.8261.0760.734s56.517s
systemc/mem_slave_tlm.1.cil.cexception37.4131.60--
systemc/mem_slave_tlm.2.cil.csafe68.0163.1962.765s60.251s
systemc/mem_slave_tlm.4.cil.ctimeout119.68118.34--
systemc/pc_sfifo_1.cil.csafe6.153.242.998s1.611s
systemc/pc_sfifo_2.cil.csafe9.325.645.350s3.293s
systemc/pc_sfifo_3.cil.csafe8.134.394.079s2.332s
systemc/token_ring.01.cil.csafe9.745.615.356s2.991s
systemc/token_ring.04.cil.csafe66.2460.9360.606s56.824s
systemc/toy.cil.csafe74.2966.4066.007s63.497s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.710.970.724s0.039s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.820.980.700s0.058s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.670.940.676s0.017s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.360.79--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.600.890.623s0.018s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.720.950.689s0.020s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.610.920.663s0.042s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.850.990.729s0.043s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.441.401.094s0.276s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.651.581.263s0.515s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.680.960.701s0.050s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.560.890.626s0.038s
ldv-regression/alias_of_return.c-safe.cil.csafe1.610.850.566s0.033s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.540.870.616s0.021s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.690.960.672s0.041s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.550.870.621s0.022s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.201.240.988s0.234s
ldv-regression/just_assert.c-safe.cil.csafe1.560.880.632s0.015s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.640.880.618s0.023s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.670.950.679s0.026s
ldv-regression/nested_structure-safe.cil.cunsafe1.560.840.601s0.044s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.640.910.644s0.021s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.700.850.612s0.017s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.530.860.595s0.025s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.901.030.742s0.094s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.911.080.791s0.031s
ldv-regression/oomInt.c-safe.cil.csafe1.650.930.672s0.033s
ldv-regression/oomInt.c-safe_1.cil.csafe1.700.930.660s0.039s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.560.950.657s0.049s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.620.980.683s0.029s
ldv-regression/rule60_list2.c-safe.cil.csafe2.221.331.001s0.261s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.680.890.622s0.030s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.710.970.691s0.022s
ldv-regression/test_address.c-safe.cil.cunsafe1.680.940.638s0.025s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.630.900.638s0.030s
ldv-regression/test_malloc-1-safe.cil.csafe1.620.830.584s0.030s
ldv-regression/test_malloc-2-safe.cil.csafe1.670.920.645s0.028s
ldv-regression/test_overflow.c-safe.cil.csafe1.520.900.627s0.030s
ldv-regression/test_union.c-safe.cil.csafe1.660.900.655s0.029s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.740.930.670s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.821.000.695s0.024s
ldv-regression/test_union_cast-2-safe.cil.csafe1.761.020.716s0.037s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.820.980.687s0.032s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.680.970.634s0.032s
ldv-regression/volatile_alias.c-safe.cil.csafe1.730.950.622s0.017s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.821.020.680s0.016s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.432.452.172s0.466s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.312.342.030s0.453s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.462.432.033s0.409s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.881.941.673s0.422s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.322.181.883s0.434s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.601.811.473s0.348s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.801.831.564s0.367s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.681.781.485s0.353s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.851.961.694s0.448s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.741.771.501s0.374s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.621.801.521s0.374s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.741.891.632s0.435s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.731.811.538s0.355s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe16.777.266.937s0.540s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe12.856.496.158s2.186s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe15.737.126.709s2.855s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe15.425.575.308s0.598s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe21.4710.9510.593s3.898s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe11.895.264.952s1.890s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe22.8113.6512.226s5.101s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe9.524.193.912s0.251s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe17.106.806.515s1.119s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.616.966.620s3.051s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe42.7527.3626.999s10.502s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe7.613.483.198s0.705s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.7210.5910.224s4.562s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe6.743.282.908s0.922s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe21.4810.139.745s6.170s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe18.568.107.782s1.209s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe35.1919.6319.190s11.133s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe12.115.825.456s3.340s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe12.896.295.957s3.582s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe21.029.449.068s1.157s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.732.402.095s0.771s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe7.913.823.519s1.287s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe20.5410.199.801s6.291s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe5.122.672.278s0.766s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe15.707.657.290s4.504s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown87.6463.9463.513s60.545s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe21.1410.339.970s6.813s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.894.694.388s2.224s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe6.022.752.466s0.863s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe9.563.793.471s1.496s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.862.422.145s0.722s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe19.488.247.857s3.543s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.782.131.865s0.502s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe26.7715.3514.961s5.518s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.901.921.613s0.217s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe14.226.355.954s3.007s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe7.383.513.126s1.016s