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-19.0041
Test setintegration-predicateAnalysis-abm
branch-r5662
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202664.021959.771558.6111142.553
correct results1781811.831205.071150.550768.620
false negatives00000
false positives1937.1920.2615.5652.481
score (220 files, max score: 356)242
pthread/fib_bench_BUG.cil.cunknown1.401.350.788s0.112s
pthread/fib_bench_longer_BUG.cil.cunknown1.490.860.589s0.029s
pthread/queue_BUG.cil.cunknown1.891.010.758s0.092s
pthread/reorder_5_BUG.cil.cunknown1.891.060.802s0.113s
pthread/twostage_3_BUG.cil.cunknown1.830.960.721s0.129s
pthread/fib_bench.cil.cunknown1.290.750.515s0.027s
pthread/fib_bench_longer.cil.cunknown1.660.910.654s0.030s
pthread/queue_ok.cil.cunknown2.021.090.812s0.123s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe16.0110.079.653s6.388s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.743.813.473s1.780s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe8.944.504.163s2.195s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.474.964.583s1.127s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.029.419.037s4.586s
ntdrivers-simplified/diskperf_simpl1.cil.csafe9.857.347.014s3.171s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.296.205.817s3.181s
ntdrivers-simplified/floppy_simpl4.cil.csafe12.246.666.312s4.083s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.041.691.417s0.525s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.562.432.133s0.971s
ntdrivers/cdaudio.BUG.i.cil.cunsafe14.817.827.479s4.211s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.475.875.505s2.886s
ntdrivers/floppy.BUG.i.cil.cunsafe12.526.926.560s3.305s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.763.803.473s1.475s
ntdrivers/parport.BUG.i.cil.cunsafe21.9213.8613.330s6.905s
ntdrivers/cdaudio.i.cil.csafe18.9711.3510.878s6.902s
ntdrivers/diskperf.i.cil.csafe12.786.836.463s3.794s
ntdrivers/floppy.i.cil.csafe15.339.198.764s4.637s
ntdrivers/parport.i.cil.csafe28.5519.0818.649s10.811s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.523.172.904s1.726s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.062.822.556s1.417s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.082.912.623s1.303s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.282.221.964s0.928s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe17.8313.3613.017s10.161s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe64.5857.9857.457s51.394s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.68114.95--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe19.0313.7613.364s10.542s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.882.141.841s0.790s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.872.642.358s1.241s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.171.070.807s0.078s
ssh-simplified/s3_clnt_1.cil.csafe10.137.046.753s4.625s
ssh-simplified/s3_clnt_2.cil.csafe8.875.555.236s3.109s
ssh-simplified/s3_clnt_3.cil.csafe8.054.454.155s2.704s
ssh-simplified/s3_clnt_4.cil.csafe12.268.638.319s5.445s
ssh-simplified/s3_srvr_1a.cil.csafe4.902.572.249s1.459s
ssh-simplified/s3_srvr_1b.cil.csafe1.951.120.864s0.244s
ssh-simplified/s3_srvr_1.cil.cout of memory65.6761.56--
ssh-simplified/s3_srvr_3.cil.csafe25.2719.5919.176s13.775s
ssh-simplified/s3_srvr_4.cil.csafe10.406.356.024s4.497s
ssh-simplified/s3_srvr_6.cil.ctimeout119.64115.10--
ssh-simplified/s3_srvr_7.cil.cunknown64.5761.4761.183s60.053s
ssh-simplified/s3_srvr_8.cil.csafe15.5411.4011.083s8.199s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.543.082.809s1.523s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.932.632.375s1.152s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.802.502.223s1.024s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.722.892.578s1.260s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.452.742.478s1.312s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.732.492.226s1.121s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.662.402.139s0.982s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.692.482.218s1.032s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe6.163.082.806s1.368s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown65.4261.3460.980s59.307s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.8120.4420.036s17.991s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.6531.1830.736s28.006s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.902.722.430s1.188s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe10.876.916.614s5.179s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe28.7723.4023.011s20.921s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.753.623.346s1.972s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.2914.2113.847s11.875s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.943.242.970s1.703s
ssh/s3_clnt.blast.01.i.cil.csafe8.255.114.810s3.161s
ssh/s3_clnt.blast.03.i.cil.csafe12.408.908.562s6.015s
ssh/s3_clnt.blast.04.i.cil.csafe11.387.156.871s3.973s
ssh/s3_srvr.blast.01.i.cil.csafe33.2128.2127.828s23.067s
ssh/s3_srvr.blast.06.i.cil.csafe25.4820.0519.623s14.759s
ssh/s3_srvr.blast.07.i.cil.cunknown66.6463.3863.094s61.553s
ssh/s3_srvr.blast.08.i.cil.csafe23.6318.5618.163s14.609s
ssh/s3_srvr.blast.09.i.cil.cunknown66.4861.6361.310s59.417s
ssh/s3_srvr.blast.10.i.cil.csafe11.567.286.931s5.097s
ssh/s3_srvr.blast.12.i.cil.csafe14.789.909.506s7.703s
ssh/s3_srvr.blast.13.i.cil.cunknown67.9463.2362.914s61.118s
ssh/s3_srvr.blast.14.i.cil.csafe38.6133.4433.032s26.506s
ssh/s3_srvr.blast.15.i.cil.csafe18.0312.8012.431s6.993s
ssh/s3_srvr.blast.16.i.cil.csafe47.5841.6541.188s29.240s
locks/test_locks_14.BUG.cunsafe2.891.771.488s0.506s
locks/test_locks_15.BUG.cunsafe2.711.631.332s0.537s
locks/test_locks_11.csafe2.371.371.103s0.296s
locks/test_locks_12.csafe2.421.411.118s0.363s
locks/test_locks_13.csafe2.581.571.261s0.481s
locks/test_locks_14.csafe2.601.521.205s0.431s
locks/test_locks_15.csafe2.831.601.335s0.610s
locks/test_locks_5.csafe1.941.090.820s0.111s
locks/test_locks_6.csafe1.761.080.759s0.142s
locks/test_locks_7.csafe1.891.160.868s0.171s
locks/test_locks_8.csafe2.031.240.955s0.230s
locks/test_locks_9.csafe2.151.250.971s0.239s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.541.471.076s0.202s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.081.090.780s0.137s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.351.481.043s0.162s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.601.331.074s0.203s
heap-manipulation/dll_of_dll.cil.cunknown2.081.090.839s0.130s
heap-manipulation/merge_sort.cil.csafe1.961.100.863s0.102s
heap-manipulation/sll_to_dll_rev.cil.cunknown13.8611.8811.627s8.897s
list-properties/alternating_list.cil.csafe1.941.040.800s0.156s
list-properties/list.cil.csafe2.291.120.866s0.213s
list-properties/list_flag.cil.csafe2.081.060.773s0.164s
list-properties/simple.cil.cunsafe2.121.050.805s0.159s
list-properties/simple_built_from_end.cil.cunsafe1.971.010.762s0.141s
list-properties/splice.cil.cunsafe3.482.121.859s0.737s
systemc/token_ring.01.BUG.cil.cunsafe3.121.751.489s0.580s
systemc/token_ring.02.BUG.cil.cunsafe5.472.632.354s1.175s
systemc/token_ring.03.BUG.cil.cunsafe6.773.593.329s1.836s
systemc/transmitter.01.BUG.cil.cunsafe2.561.381.130s0.357s
systemc/transmitter.02.BUG.cil.cunsafe3.682.051.765s0.754s
systemc/transmitter.03.BUG.cil.cunsafe5.322.862.573s1.161s
systemc/transmitter.04.BUG.cil.cunsafe6.533.393.039s1.216s
systemc/bist_cell.cil.csafe20.8917.2516.851s14.412s
systemc/kundu.cil.cexception7.193.82--
systemc/mem_slave_tlm.1.cil.cexception45.7641.07--
systemc/mem_slave_tlm.2.cil.csafe65.7262.9162.609s58.598s
systemc/pc_sfifo_1.cil.csafe5.262.822.565s1.371s
systemc/pc_sfifo_2.cil.csafe7.914.824.556s2.782s
systemc/pc_sfifo_3.cil.csafe7.574.223.953s2.260s
systemc/token_ring.01.cil.csafe8.404.964.690s2.672s
systemc/token_ring.04.cil.csafe69.2864.0063.691s61.105s
systemc/toy.cil.csafe69.1662.3262.000s60.118s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.460.870.619s0.028s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.530.940.684s0.053s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.691.040.751s0.020s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.530.930.645s0.047s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.460.850.590s0.018s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.630.930.660s0.026s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.590.870.619s0.065s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.570.950.723s0.034s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.421.441.123s0.265s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.381.511.271s0.598s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.721.070.776s0.044s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.671.080.745s0.039s
ldv-regression/alias_of_return.c-safe.cil.csafe1.370.810.555s0.030s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.510.940.681s0.030s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.410.820.558s0.037s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.390.810.558s0.019s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe1.941.110.872s0.220s
ldv-regression/just_assert.c-safe.cil.csafe1.360.770.530s0.011s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.350.780.531s0.018s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.350.790.538s0.018s
ldv-regression/nested_structure-safe.cil.cunsafe1.540.860.629s0.058s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.340.770.535s0.020s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.450.820.564s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.380.800.560s0.021s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.600.940.676s0.100s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.370.790.547s0.023s
ldv-regression/oomInt.c-safe.cil.csafe1.430.820.584s0.037s
ldv-regression/oomInt.c-safe_1.cil.csafe1.340.790.559s0.032s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.520.910.616s0.053s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.440.820.584s0.024s
ldv-regression/rule60_list2.c-safe.cil.csafe1.911.130.866s0.224s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.380.790.561s0.026s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.350.780.527s0.017s
ldv-regression/test_address.c-safe.cil.cunsafe1.440.860.621s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.370.780.548s0.023s
ldv-regression/test_malloc-1-safe.cil.csafe1.470.840.601s0.033s
ldv-regression/test_malloc-2-safe.cil.csafe1.400.790.557s0.029s
ldv-regression/test_overflow.c-safe.cil.csafe1.390.810.576s0.034s
ldv-regression/test_union.c-safe.cil.csafe1.340.770.530s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.490.780.547s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.380.780.548s0.017s
ldv-regression/test_union_cast-2-safe.cil.csafe1.360.780.535s0.026s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.590.890.664s0.022s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.390.810.567s0.021s
ldv-regression/volatile_alias.c-safe.cil.csafe1.420.830.592s0.022s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.360.790.543s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.561.921.676s0.355s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.581.911.665s0.383s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.581.921.665s0.380s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.241.651.386s0.358s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.261.671.423s0.354s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.601.731.461s0.382s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.981.921.625s0.422s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.751.891.606s0.433s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.351.751.500s0.445s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.541.761.488s0.370s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.351.711.448s0.400s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.731.861.612s0.407s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.481.781.503s0.351s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.506.696.380s0.538s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe11.506.115.806s2.246s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.937.637.289s3.657s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe12.534.724.456s0.524s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe17.359.278.958s2.987s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe9.134.143.846s1.555s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe19.6911.4911.153s5.155s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe10.284.013.745s0.217s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe15.546.486.174s1.271s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.046.686.344s2.897s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe45.7029.4929.108s10.222s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.473.162.884s0.610s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.2310.6410.329s3.470s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.472.742.473s0.907s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe21.0711.0710.649s7.778s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe15.797.086.735s1.005s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe42.6922.8122.401s13.660s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.115.725.353s3.510s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe12.887.106.760s3.758s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe17.678.287.965s1.075s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown3.861.911.662s0.637s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe6.693.282.975s1.375s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe19.9310.309.951s6.850s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.902.312.008s0.711s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe16.158.047.671s5.197s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown90.6662.9362.468s59.548s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe24.4011.9211.545s8.336s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe8.364.374.083s1.991s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.192.652.388s0.989s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.123.683.393s1.643s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.272.181.916s0.725s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe18.098.438.095s4.664s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.262.021.770s0.452s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe19.9311.6811.345s4.806s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.441.651.408s0.179s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe12.545.955.581s3.333s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe6.753.212.884s1.144s