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.2002
Test setintegration-predicateAnalysis
branch-r5671
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2213543.842586.022318.6941930.745
correct results1611071.28704.03652.965385.126
false negatives00000
false positives1937.2320.0115.2332.585
score (221 files, max score: 357)211
pthread/fib_bench_BUG.cil.cunknown1.921.180.821s0.038s
pthread/fib_bench_longer_BUG.cil.cunknown1.811.030.723s0.026s
pthread/queue_BUG.cil.cunknown2.161.230.940s0.134s
pthread/reorder_5_BUG.cil.cunknown2.221.230.859s0.136s
pthread/twostage_3_BUG.cil.cunknown2.421.471.154s0.167s
pthread/fib_bench.cil.cunknown1.821.030.757s0.025s
pthread/fib_bench_longer.cil.cunknown1.600.890.625s0.023s
pthread/queue_ok.cil.cunknown2.061.120.846s0.094s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.203.933.631s2.216s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.922.321.992s0.876s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.482.592.317s1.126s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.431.791.516s0.584s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.583.363.038s2.070s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.322.732.428s1.637s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.291.751.482s0.759s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.322.332.037s1.059s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.541.311.021s0.360s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.071.541.236s0.487s
ntdrivers/cdaudio.BUG.i.cil.cunsafe9.855.565.223s2.817s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.734.123.788s2.153s
ntdrivers/floppy.BUG.i.cil.cunsafe11.286.676.249s4.097s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe4.762.612.311s0.998s
ntdrivers/parport.BUG.i.cil.cunknown84.4763.2362.637s61.156s
ntdrivers/cdaudio.i.cil.csafe9.575.164.805s2.947s
ntdrivers/diskperf.i.cil.csafe5.503.403.124s2.000s
ntdrivers/floppy.i.cil.csafe26.2319.9719.545s15.039s
ntdrivers/parport.i.cil.cunknown87.2968.8863.331s61.693s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.672.141.858s0.870s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.192.502.196s1.094s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe4.122.231.944s0.860s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.262.452.154s0.995s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.581.351.073s0.296s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe6.223.393.065s1.622s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.627.547.250s5.465s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.101.621.354s0.497s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.521.831.566s0.684s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.361.741.465s0.607s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.141.120.851s0.067s
ssh-simplified/s3_clnt_1.cil.csafe8.115.144.782s2.881s
ssh-simplified/s3_clnt_2.cil.csafe8.885.865.490s3.593s
ssh-simplified/s3_clnt_3.cil.csafe9.456.315.975s3.134s
ssh-simplified/s3_clnt_4.cil.csafe9.086.005.680s3.298s
ssh-simplified/s3_srvr_1a.cil.csafe3.712.161.840s1.114s
ssh-simplified/s3_srvr_1b.cil.csafe1.660.970.738s0.128s
ssh-simplified/s3_srvr_1.cil.csafe34.4630.0329.519s22.109s
ssh-simplified/s3_srvr_3.cil.csafe24.6920.3119.801s13.185s
ssh-simplified/s3_srvr_4.cil.csafe13.949.849.370s7.635s
ssh-simplified/s3_srvr_6.cil.csafe16.6112.3111.845s9.837s
ssh-simplified/s3_srvr_7.cil.csafe22.8518.7918.346s16.473s
ssh-simplified/s3_srvr_8.cil.csafe12.999.028.594s5.828s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe4.952.742.466s1.152s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.322.322.041s0.931s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.422.412.134s1.008s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe4.292.271.994s0.936s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.462.352.058s0.927s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.092.131.791s0.751s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.092.121.822s0.743s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe3.902.061.764s0.688s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe4.792.522.212s0.956s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.024.093.797s2.419s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe7.114.223.914s2.271s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.173.863.554s1.783s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.612.962.666s1.550s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.612.832.547s1.252s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.267.387.067s5.695s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.082.852.572s1.311s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.704.394.083s2.171s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.922.652.370s1.146s
ssh/s3_clnt.blast.01.i.cil.csafe9.706.356.030s4.152s
ssh/s3_clnt.blast.03.i.cil.csafe8.585.274.940s3.473s
ssh/s3_clnt.blast.04.i.cil.csafe11.668.007.636s5.529s
ssh/s3_srvr.blast.01.i.cil.csafe12.848.528.084s5.301s
ssh/s3_srvr.blast.06.i.cil.csafe16.0711.5111.011s9.252s
ssh/s3_srvr.blast.07.i.cil.csafe15.0310.419.889s8.222s
ssh/s3_srvr.blast.08.i.cil.cout of memory91.8587.63--
ssh/s3_srvr.blast.09.i.cil.csafe12.548.518.088s5.927s
ssh/s3_srvr.blast.10.i.cil.csafe53.0647.8047.288s15.475s
ssh/s3_srvr.blast.12.i.cil.csafe41.5136.3635.803s17.140s
ssh/s3_srvr.blast.13.i.cil.csafe24.3519.4118.835s15.903s
ssh/s3_srvr.blast.14.i.cil.csafe34.0428.7528.200s22.017s
ssh/s3_srvr.blast.15.i.cil.csafe13.728.808.272s5.897s
ssh/s3_srvr.blast.16.i.cil.csafe15.7910.9210.413s7.269s
locks/test_locks_14.BUG.cunsafe1.821.070.814s0.108s
locks/test_locks_15.BUG.cunsafe1.751.040.780s0.116s
locks/test_locks_11.csafe1.510.840.606s0.079s
locks/test_locks_12.csafe1.680.900.653s0.090s
locks/test_locks_13.csafe1.740.930.679s0.097s
locks/test_locks_14.csafe1.801.000.745s0.115s
locks/test_locks_15.csafe1.871.060.774s0.124s
locks/test_locks_5.csafe1.680.960.685s0.045s
locks/test_locks_6.csafe1.660.860.608s0.050s
locks/test_locks_7.csafe1.640.930.685s0.058s
locks/test_locks_8.csafe1.700.970.651s0.060s
locks/test_locks_9.csafe1.560.890.643s0.069s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.241.210.945s0.208s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.780.920.682s0.097s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.111.220.941s0.173s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown66.8464.3564.044s60.157s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.581.351.068s0.219s
heap-manipulation/dll_of_dll.cil.cunknown1.891.070.818s0.109s
heap-manipulation/merge_sort.cil.csafe1.780.950.708s0.079s
heap-manipulation/sll_to_dll_rev.cil.cunknown62.7960.9260.642s54.160s
list-properties/alternating_list.cil.csafe2.071.070.797s0.168s
list-properties/list.cil.csafe2.111.150.894s0.217s
list-properties/list_flag.cil.csafe2.020.980.743s0.161s
list-properties/simple.cil.cunsafe1.941.000.738s0.146s
list-properties/simple_built_from_end.cil.cunsafe1.800.940.698s0.109s
list-properties/splice.cil.cunsafe3.322.001.746s0.866s
systemc/token_ring.01.BUG.cil.cunsafe2.941.581.315s0.580s
systemc/token_ring.02.BUG.cil.cunsafe4.732.482.152s1.273s
systemc/token_ring.03.BUG.cil.cunsafe7.783.953.594s2.529s
systemc/transmitter.01.BUG.cil.cunsafe2.241.240.945s0.279s
systemc/transmitter.02.BUG.cil.cunsafe2.911.541.278s0.545s
systemc/transmitter.03.BUG.cil.cunsafe4.882.442.134s1.250s
systemc/transmitter.04.BUG.cil.cunsafe8.964.584.232s3.126s
systemc/bist_cell.cil.csafe2.431.311.034s0.385s
systemc/kundu.cil.csafe16.9612.2911.708s10.175s
systemc/mem_slave_tlm.1.cil.cout of memory55.7451.13--
systemc/mem_slave_tlm.2.cil.cout of memory53.9349.45--
systemc/pc_sfifo_1.cil.csafe4.642.282.009s1.217s
systemc/pc_sfifo_2.cil.csafe5.152.532.234s1.421s
systemc/pc_sfifo_3.cil.csafe2.221.180.927s0.296s
systemc/token_ring.01.cil.csafe4.482.111.797s1.064s
systemc/token_ring.04.cil.cunknown72.4761.5060.576s54.961s
systemc/toy.cil.cunknown66.2061.1060.676s57.833s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.690.870.622s0.026s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.640.930.667s0.046s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.560.800.557s0.014s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.700.900.654s0.045s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.590.870.625s0.017s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.700.870.623s0.021s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.841.020.736s0.051s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.630.890.644s0.030s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.121.180.909s0.104s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.111.090.838s0.229s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.610.830.592s0.039s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.620.890.631s0.035s
ldv-regression/alias_of_return.c-safe.cil.csafe1.530.790.546s0.018s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.620.870.625s0.020s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.690.890.632s0.025s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.620.820.572s0.018s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.401.230.979s0.322s
ldv-regression/just_assert.c-safe.cil.csafe1.510.770.526s0.010s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.530.790.557s0.018s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.580.900.633s0.016s
ldv-regression/nested_structure-safe.cil.cunsafe1.840.910.665s0.057s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.580.800.566s0.020s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.550.820.584s0.018s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.530.800.549s0.015s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.730.970.731s0.120s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.460.810.562s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.500.820.578s0.021s
ldv-regression/oomInt.c-safe_1.cil.csafe1.510.780.541s0.017s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.620.880.639s0.050s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.600.820.580s0.023s
ldv-regression/rule60_list2.c-safe.cil.csafe1.810.980.737s0.116s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.450.780.540s0.017s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.600.920.678s0.021s
ldv-regression/test_address.c-safe.cil.cunsafe1.500.870.609s0.018s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.430.810.549s0.017s
ldv-regression/test_malloc-1-safe.cil.csafe1.520.820.579s0.034s
ldv-regression/test_malloc-2-safe.cil.csafe1.600.840.597s0.029s
ldv-regression/test_overflow.c-safe.cil.csafe1.680.840.575s0.023s
ldv-regression/test_union.c-safe.cil.csafe1.540.810.564s0.017s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.470.840.574s0.015s
ldv-regression/test_union_cast-1-safe.cil.csafe1.600.840.597s0.021s
ldv-regression/test_union_cast-2-safe.cil.csafe1.580.840.584s0.032s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.680.870.619s0.024s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.550.790.546s0.016s
ldv-regression/volatile_alias.c-safe.cil.csafe1.560.870.616s0.018s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.650.980.737s0.029s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.412.241.972s0.645s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.042.011.751s0.573s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.022.001.748s0.560s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.891.821.549s0.500s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.981.841.549s0.501s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.971.911.641s0.571s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.322.201.881s0.643s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.392.131.822s0.580s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe4.121.991.717s0.553s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.831.941.650s0.599s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.532.462.086s0.639s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.362.131.858s0.617s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.931.891.634s0.500s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.225.254.965s0.483s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe17.5410.219.829s7.007s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown92.1364.3263.786s62.030s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe15.325.825.506s0.717s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown79.0763.9463.452s39.666s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe18.1214.5113.820s10.543s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown87.1362.2061.759s59.386s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.023.022.752s0.250s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe11.684.434.163s0.389s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe11.387.316.977s4.837s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown85.9562.3961.877s52.677s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe5.202.482.218s0.493s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe40.2530.2229.678s21.156s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe4.972.362.087s0.915s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown93.4663.9963.489s61.862s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown89.3066.8166.253s62.240s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown88.7663.6462.966s61.649s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe8.354.884.513s3.137s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown5.692.782.485s1.009s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown94.2168.2867.785s62.051s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.102.141.824s0.795s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown87.9963.4662.985s61.055s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown89.6564.5564.077s62.404s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe2.664.152.837s1.230s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown79.8864.0962.468s59.761s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown87.8764.2563.783s61.732s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown84.8463.2162.717s60.599s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe6.924.043.740s2.399s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown82.6762.9962.306s61.234s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown82.0062.2461.657s60.260s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown90.3963.1462.613s61.469s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown90.8064.7064.175s61.450s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.201.621.351s0.353s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown100.6762.2861.771s56.678s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe2.801.491.240s0.166s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown86.0663.6463.081s60.920s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown91.4563.5863.056s61.298s