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-20.2001
Test setintegration-predicateAnalysis-abm
branch-r5671
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202654.151951.411554.3461148.467
correct results1781802.551196.461142.106770.101
false negatives00000
false positives1937.0920.7415.9762.724
score (220 files, max score: 356)242
pthread/fib_bench_BUG.cil.cunknown1.310.760.525s0.024s
pthread/fib_bench_longer_BUG.cil.cunknown1.350.770.526s0.024s
pthread/queue_BUG.cil.cunknown1.871.030.786s0.107s
pthread/reorder_5_BUG.cil.cunknown1.891.090.839s0.139s
pthread/twostage_3_BUG.cil.cunknown2.181.100.830s0.138s
pthread/fib_bench.cil.cunknown1.650.860.609s0.032s
pthread/fib_bench_longer.cil.cunknown1.440.780.556s0.024s
pthread/queue_ok.cil.cunknown1.540.870.645s0.107s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe18.4412.4311.941s8.603s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.783.953.493s1.790s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe9.294.654.336s2.448s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.532.722.362s1.116s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe14.758.678.234s5.399s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.795.895.526s3.560s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.435.485.122s3.072s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.956.255.877s3.676s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.321.961.676s0.673s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.742.372.075s0.948s
ntdrivers/cdaudio.BUG.i.cil.cunsafe15.728.378.029s4.575s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.496.165.822s3.064s
ntdrivers/floppy.BUG.i.cil.cunsafe12.606.916.499s3.146s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.714.113.722s1.624s
ntdrivers/parport.BUG.i.cil.cunsafe20.4912.5212.150s6.731s
ntdrivers/cdaudio.i.cil.csafe17.8110.159.784s6.003s
ntdrivers/diskperf.i.cil.csafe12.667.106.771s3.940s
ntdrivers/floppy.i.cil.csafe15.859.318.967s4.721s
ntdrivers/parport.i.cil.csafe29.5320.0219.573s12.335s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.243.172.908s1.672s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.072.822.534s1.386s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.023.162.841s1.429s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.262.362.097s0.897s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe19.2714.8014.429s11.326s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe62.7556.6156.108s50.619s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.58115.00--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.0213.4313.102s10.432s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.892.221.914s0.868s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.522.382.112s1.182s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.051.010.775s0.058s
ssh-simplified/s3_clnt_1.cil.csafe9.946.626.336s4.378s
ssh-simplified/s3_clnt_2.cil.csafe8.925.655.352s3.369s
ssh-simplified/s3_clnt_3.cil.csafe7.594.554.243s2.709s
ssh-simplified/s3_clnt_4.cil.csafe12.298.488.194s5.340s
ssh-simplified/s3_srvr_1a.cil.csafe4.722.502.185s1.404s
ssh-simplified/s3_srvr_1b.cil.csafe2.291.280.992s0.266s
ssh-simplified/s3_srvr_1.cil.cout of memory62.9758.68--
ssh-simplified/s3_srvr_3.cil.csafe24.4319.4919.063s14.054s
ssh-simplified/s3_srvr_4.cil.csafe9.826.295.961s4.527s
ssh-simplified/s3_srvr_6.cil.ctimeout119.62115.09--
ssh-simplified/s3_srvr_7.cil.cunknown65.3662.1061.811s60.709s
ssh-simplified/s3_srvr_8.cil.csafe15.7911.2410.909s8.167s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.593.463.190s1.622s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe5.002.802.519s1.193s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.692.572.236s1.038s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.402.612.355s1.181s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.422.722.407s1.250s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.612.502.239s1.054s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.722.462.165s0.979s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.732.512.252s1.036s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe6.013.282.961s1.418s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown68.9664.9464.574s63.119s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe24.9919.7019.277s17.221s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe35.7230.3429.927s27.070s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.822.632.362s1.129s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe10.866.946.642s5.239s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe29.1923.6923.284s21.170s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.683.633.321s1.988s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.3514.1413.775s11.816s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.963.473.193s1.796s
ssh/s3_clnt.blast.01.i.cil.csafe8.695.054.765s3.092s
ssh/s3_clnt.blast.03.i.cil.csafe12.778.668.380s5.831s
ssh/s3_clnt.blast.04.i.cil.csafe11.477.337.045s4.150s
ssh/s3_srvr.blast.01.i.cil.csafe33.3428.6728.290s23.977s
ssh/s3_srvr.blast.06.i.cil.csafe26.1820.6920.232s14.914s
ssh/s3_srvr.blast.07.i.cil.cunknown68.4864.8464.536s62.899s
ssh/s3_srvr.blast.08.i.cil.csafe25.4219.8119.405s16.018s
ssh/s3_srvr.blast.09.i.cil.cunknown65.8261.2660.941s59.073s
ssh/s3_srvr.blast.10.i.cil.csafe11.437.126.788s5.117s
ssh/s3_srvr.blast.12.i.cil.csafe14.939.759.368s7.592s
ssh/s3_srvr.blast.13.i.cil.cunknown65.6261.1060.785s59.094s
ssh/s3_srvr.blast.14.i.cil.csafe39.7534.0533.607s27.076s
ssh/s3_srvr.blast.15.i.cil.csafe18.1512.8412.414s6.798s
ssh/s3_srvr.blast.16.i.cil.csafe45.2439.7139.249s27.374s
locks/test_locks_14.BUG.cunsafe2.581.561.282s0.445s
locks/test_locks_15.BUG.cunsafe2.771.601.316s0.464s
locks/test_locks_11.csafe2.221.301.026s0.304s
locks/test_locks_12.csafe2.481.451.181s0.339s
locks/test_locks_13.csafe2.601.521.241s0.456s
locks/test_locks_14.csafe2.661.591.300s0.532s
locks/test_locks_15.csafe2.751.631.329s0.504s
locks/test_locks_5.csafe1.911.130.836s0.121s
locks/test_locks_6.csafe2.011.120.800s0.148s
locks/test_locks_7.csafe1.891.200.868s0.169s
locks/test_locks_8.csafe2.011.270.983s0.206s
locks/test_locks_9.csafe2.061.361.127s0.265s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.441.471.140s0.218s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.081.140.889s0.124s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.371.371.092s0.228s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.481.391.119s0.229s
heap-manipulation/dll_of_dll.cil.cunknown1.961.030.783s0.120s
heap-manipulation/merge_sort.cil.csafe1.901.040.788s0.089s
heap-manipulation/sll_to_dll_rev.cil.cunknown13.3811.6611.382s8.713s
list-properties/alternating_list.cil.csafe1.991.090.824s0.158s
list-properties/list.cil.csafe2.061.100.842s0.220s
list-properties/list_flag.cil.csafe2.041.020.774s0.172s
list-properties/simple.cil.cunsafe2.041.070.795s0.167s
list-properties/simple_built_from_end.cil.cunsafe1.981.010.756s0.142s
list-properties/splice.cil.cunsafe3.532.302.017s0.837s
systemc/token_ring.01.BUG.cil.cunsafe3.131.771.509s0.576s
systemc/token_ring.02.BUG.cil.cunsafe5.422.692.408s1.178s
systemc/token_ring.03.BUG.cil.cunsafe7.714.153.856s2.146s
systemc/transmitter.01.BUG.cil.cunsafe2.681.531.221s0.396s
systemc/transmitter.02.BUG.cil.cunsafe3.952.051.738s0.735s
systemc/transmitter.03.BUG.cil.cunsafe5.503.132.801s1.142s
systemc/transmitter.04.BUG.cil.cunsafe6.773.573.199s1.395s
systemc/bist_cell.cil.csafe20.7016.9316.523s14.154s
systemc/kundu.cil.cexception6.963.82--
systemc/mem_slave_tlm.1.cil.cexception45.2540.31--
systemc/mem_slave_tlm.2.cil.csafe66.2862.5562.212s59.500s
systemc/pc_sfifo_1.cil.csafe5.132.822.575s1.374s
systemc/pc_sfifo_2.cil.csafe8.064.744.467s2.730s
systemc/pc_sfifo_3.cil.csafe6.983.903.631s2.104s
systemc/token_ring.01.cil.csafe8.264.644.378s2.487s
systemc/token_ring.04.cil.csafe67.0660.9560.655s57.061s
systemc/toy.cil.csafe68.9762.8962.441s60.317s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.400.870.577s0.031s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.500.920.684s0.053s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.440.880.601s0.016s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.590.960.699s0.048s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.340.810.532s0.018s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.500.890.639s0.021s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.700.930.660s0.045s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.600.950.722s0.036s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.381.401.141s0.303s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.421.431.194s0.437s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.691.000.747s0.060s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.651.080.778s0.048s
ldv-regression/alias_of_return.c-safe.cil.csafe1.570.860.570s0.031s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.380.800.548s0.018s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.520.910.673s0.036s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.500.910.608s0.023s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe1.961.180.940s0.261s
ldv-regression/just_assert.c-safe.cil.csafe1.320.750.521s0.014s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.370.780.538s0.017s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.470.870.624s0.018s
ldv-regression/nested_structure-safe.cil.cunsafe1.490.860.634s0.051s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.350.780.548s0.025s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.360.770.524s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.380.810.570s0.027s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.600.930.681s0.100s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.400.810.560s0.023s
ldv-regression/oomInt.c-safe.cil.csafe1.360.800.564s0.032s
ldv-regression/oomInt.c-safe_1.cil.csafe1.360.790.560s0.038s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.510.880.622s0.051s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.360.790.562s0.024s
ldv-regression/rule60_list2.c-safe.cil.csafe2.271.220.969s0.242s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.350.760.534s0.024s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.440.860.605s0.017s
ldv-regression/test_address.c-safe.cil.cunsafe1.410.820.565s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.560.880.640s0.023s
ldv-regression/test_malloc-1-safe.cil.csafe1.530.890.645s0.037s
ldv-regression/test_malloc-2-safe.cil.csafe1.420.800.567s0.029s
ldv-regression/test_overflow.c-safe.cil.csafe1.330.770.545s0.031s
ldv-regression/test_union.c-safe.cil.csafe1.340.770.531s0.017s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.410.800.565s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.320.750.525s0.016s
ldv-regression/test_union_cast-2-safe.cil.csafe1.480.870.628s0.027s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.430.810.572s0.022s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.440.870.628s0.018s
ldv-regression/volatile_alias.c-safe.cil.csafe1.330.760.521s0.018s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.420.820.570s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.631.951.702s0.352s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.621.921.645s0.371s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.762.011.759s0.407s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.201.681.421s0.371s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.271.651.409s0.354s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.421.751.486s0.453s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.851.831.577s0.379s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.981.871.623s0.406s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.771.851.586s0.403s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.601.851.589s0.448s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.541.811.562s0.426s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.311.701.449s0.391s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.471.681.442s0.357s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.326.215.930s0.489s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe11.586.335.965s2.202s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.267.206.868s3.387s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe12.324.634.359s0.547s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe17.579.589.274s3.541s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe9.644.424.116s1.678s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe18.7210.7110.380s4.549s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.242.992.730s0.206s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe14.465.835.551s1.160s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.016.616.275s2.889s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe45.5330.4530.109s10.678s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.903.343.065s0.644s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.3210.5410.222s3.502s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.612.862.594s1.029s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe17.649.559.212s7.044s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe14.876.796.479s1.336s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe40.3522.5422.103s13.116s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe12.246.295.907s3.670s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe12.836.956.587s3.723s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe17.688.428.096s1.126s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown3.851.961.698s0.651s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe7.033.403.102s1.454s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe20.7010.339.998s7.061s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.522.201.928s0.690s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe14.907.547.168s4.993s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown91.3964.0263.549s60.545s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe23.3512.1411.802s8.832s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.775.074.791s2.286s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.512.862.588s1.047s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.564.003.663s1.564s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.322.181.901s0.694s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe18.548.538.190s4.695s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.482.101.837s0.517s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe19.5811.7711.440s5.149s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.381.701.436s0.186s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe12.065.785.468s3.165s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe6.242.852.555s1.009s