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-21.1712
Test setintegration-predicateAnalysis
branch-r5680
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2213550.512594.762257.4251864.499
correct results1611065.15695.78644.279378.009
false negatives00000
false positives1938.7921.0416.0992.769
score (221 files, max score: 357)211
pthread/fib_bench_BUG.cil.cunknown1.831.030.722s0.041s
pthread/fib_bench_longer_BUG.cil.cunknown1.804.063.631s0.028s
pthread/queue_BUG.cil.cunknown1.952.982.645s0.116s
pthread/reorder_5_BUG.cil.cunknown2.073.201.802s0.125s
pthread/twostage_3_BUG.cil.cunknown2.205.022.063s0.126s
pthread/fib_bench.cil.cunknown1.632.322.043s0.029s
pthread/fib_bench_longer.cil.cunknown1.842.972.604s0.031s
pthread/queue_ok.cil.cunknown1.912.682.407s0.105s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.445.033.599s2.203s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.802.111.820s0.775s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.502.642.312s1.010s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.241.731.442s0.546s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.723.453.115s1.938s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.622.842.530s1.654s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.421.901.638s0.898s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.502.432.113s1.205s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.722.061.066s0.349s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.351.671.375s0.567s
ntdrivers/cdaudio.BUG.i.cil.cunsafe9.885.374.971s2.671s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.784.163.782s2.007s
ntdrivers/floppy.BUG.i.cil.cunsafe11.256.656.266s4.028s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe4.112.251.942s0.826s
ntdrivers/parport.BUG.i.cil.cunknown91.3073.5364.197s62.634s
ntdrivers/cdaudio.i.cil.csafe9.825.505.192s3.264s
ntdrivers/diskperf.i.cil.csafe6.153.523.229s2.040s
ntdrivers/floppy.i.cil.csafe25.3619.4519.058s14.549s
ntdrivers/parport.i.cil.cunknown92.3167.1563.474s61.973s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.501.891.620s0.683s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe3.902.271.991s0.894s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe3.832.061.761s0.865s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.222.382.102s1.002s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.471.291.042s0.304s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe5.883.232.942s1.509s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.037.146.842s5.190s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.261.741.449s0.514s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.361.761.500s0.653s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.161.641.389s0.584s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.021.030.805s0.054s
ssh-simplified/s3_clnt_1.cil.csafe7.805.134.837s2.977s
ssh-simplified/s3_clnt_2.cil.csafe7.805.064.769s3.202s
ssh-simplified/s3_clnt_3.cil.csafe9.286.135.832s3.010s
ssh-simplified/s3_clnt_4.cil.csafe8.865.835.504s3.393s
ssh-simplified/s3_srvr_1a.cil.csafe3.361.881.562s0.995s
ssh-simplified/s3_srvr_1b.cil.csafe1.761.020.780s0.128s
ssh-simplified/s3_srvr_1.cil.csafe35.0431.1330.652s22.765s
ssh-simplified/s3_srvr_3.cil.csafe25.7521.6121.129s14.134s
ssh-simplified/s3_srvr_4.cil.csafe14.7010.5210.066s8.119s
ssh-simplified/s3_srvr_6.cil.csafe16.2911.9811.479s9.580s
ssh-simplified/s3_srvr_7.cil.csafe22.6218.2617.817s15.930s
ssh-simplified/s3_srvr_8.cil.csafe12.418.828.415s5.668s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe4.672.522.242s1.064s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.382.442.144s0.998s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.302.251.971s0.891s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe3.942.201.911s0.849s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.152.191.924s0.910s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.132.211.935s0.839s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.192.071.776s0.718s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.112.081.796s0.809s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe4.762.582.250s0.993s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe6.743.993.712s2.390s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe7.484.384.070s2.374s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.183.843.528s1.756s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.613.022.741s1.589s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.883.042.755s1.288s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.247.357.050s5.648s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.182.902.601s1.306s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.154.103.787s1.910s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.942.622.333s1.084s
ssh/s3_clnt.blast.01.i.cil.csafe10.166.656.320s4.281s
ssh/s3_clnt.blast.03.i.cil.csafe9.065.785.414s3.757s
ssh/s3_clnt.blast.04.i.cil.csafe11.968.267.910s5.778s
ssh/s3_srvr.blast.01.i.cil.csafe13.798.688.198s5.362s
ssh/s3_srvr.blast.06.i.cil.csafe15.9311.3910.881s9.108s
ssh/s3_srvr.blast.07.i.cil.csafe14.549.949.476s7.907s
ssh/s3_srvr.blast.08.i.cil.cout of memory87.0182.66--
ssh/s3_srvr.blast.09.i.cil.csafe12.968.688.246s5.961s
ssh/s3_srvr.blast.10.i.cil.csafe52.3847.3346.803s15.636s
ssh/s3_srvr.blast.12.i.cil.csafe43.6438.2337.693s16.721s
ssh/s3_srvr.blast.13.i.cil.csafe22.0717.3716.832s14.444s
ssh/s3_srvr.blast.14.i.cil.csafe31.9326.8026.173s20.393s
ssh/s3_srvr.blast.15.i.cil.csafe13.148.457.916s5.507s
ssh/s3_srvr.blast.16.i.cil.csafe16.7611.9211.447s8.077s
locks/test_locks_14.BUG.cunsafe1.771.040.794s0.100s
locks/test_locks_15.BUG.cunsafe1.650.920.675s0.106s
locks/test_locks_11.csafe1.620.860.637s0.080s
locks/test_locks_12.csafe1.520.880.647s0.089s
locks/test_locks_13.csafe1.590.890.664s0.094s
locks/test_locks_14.csafe1.650.940.709s0.116s
locks/test_locks_15.csafe1.640.870.644s0.109s
locks/test_locks_5.csafe1.560.840.583s0.040s
locks/test_locks_6.csafe1.540.840.605s0.048s
locks/test_locks_7.csafe1.510.840.616s0.055s
locks/test_locks_8.csafe1.560.880.646s0.065s
locks/test_locks_9.csafe1.690.970.721s0.070s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.521.351.040s0.225s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.041.120.816s0.113s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.151.240.939s0.177s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown63.5761.1360.812s56.612s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.641.411.139s0.216s
heap-manipulation/dll_of_dll.cil.cunknown2.141.170.892s0.138s
heap-manipulation/merge_sort.cil.csafe1.961.030.747s0.085s
heap-manipulation/sll_to_dll_rev.cil.cunknown63.0861.0460.741s54.163s
list-properties/alternating_list.cil.csafe1.790.940.705s0.136s
list-properties/list.cil.csafe1.941.030.797s0.185s
list-properties/list_flag.cil.csafe1.861.020.791s0.189s
list-properties/simple.cil.cunsafe2.141.140.860s0.156s
list-properties/simple_built_from_end.cil.cunsafe1.841.050.756s0.128s
list-properties/splice.cil.cunsafe3.542.231.956s0.941s
systemc/token_ring.01.BUG.cil.cunsafe3.251.871.566s0.642s
systemc/token_ring.02.BUG.cil.cunsafe4.732.301.949s1.123s
systemc/token_ring.03.BUG.cil.cunsafe8.184.143.757s2.685s
systemc/transmitter.01.BUG.cil.cunsafe2.451.291.008s0.290s
systemc/transmitter.02.BUG.cil.cunsafe3.141.721.393s0.605s
systemc/transmitter.03.BUG.cil.cunsafe5.042.532.218s1.333s
systemc/transmitter.04.BUG.cil.cunsafe9.324.864.533s3.329s
systemc/bist_cell.cil.csafe2.701.461.163s0.414s
systemc/kundu.cil.csafe16.9512.6712.072s10.458s
systemc/mem_slave_tlm.1.cil.cout of memory58.4854.14--
systemc/mem_slave_tlm.2.cil.cout of memory54.9550.12--
systemc/pc_sfifo_1.cil.csafe4.622.281.894s1.210s
systemc/pc_sfifo_2.cil.csafe5.342.532.257s1.431s
systemc/pc_sfifo_3.cil.csafe2.201.180.913s0.292s
systemc/token_ring.01.cil.csafe4.702.271.919s1.174s
systemc/token_ring.04.cil.cunknown72.3861.2560.879s54.646s
systemc/toy.cil.cunknown67.2662.07--
ldv-regression/1_3.c-unsafe.cil.cunsafe1.500.890.627s0.028s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.590.930.652s0.054s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.520.800.558s0.013s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.710.880.639s0.048s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.580.840.559s0.016s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.460.790.551s0.016s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.610.840.597s0.035s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.821.030.758s0.032s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.801.010.769s0.126s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.181.120.856s0.232s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.710.980.690s0.046s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.780.950.612s0.032s
ldv-regression/alias_of_return.c-safe.cil.csafe1.610.870.612s0.018s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.530.790.549s0.016s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.510.810.570s0.023s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.510.780.541s0.016s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.391.251.005s0.365s
ldv-regression/just_assert.c-safe.cil.csafe1.540.770.534s0.009s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.770.950.687s0.017s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.590.830.564s0.015s
ldv-regression/nested_structure-safe.cil.cunsafe1.720.930.694s0.071s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.610.810.573s0.020s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.660.890.628s0.021s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.490.790.545s0.017s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.961.030.782s0.129s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.790.950.680s0.023s
ldv-regression/oomInt.c-safe.cil.csafe1.680.860.602s0.020s
ldv-regression/oomInt.c-safe_1.cil.csafe1.510.780.550s0.017s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.660.950.698s0.064s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.861.010.744s0.026s
ldv-regression/rule60_list2.c-safe.cil.csafe1.891.050.800s0.132s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.640.950.685s0.023s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.680.890.659s0.020s
ldv-regression/test_address.c-safe.cil.cunsafe1.680.890.658s0.018s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.540.780.547s0.016s
ldv-regression/test_malloc-1-safe.cil.csafe1.720.870.599s0.035s
ldv-regression/test_malloc-2-safe.cil.csafe1.760.930.636s0.034s
ldv-regression/test_overflow.c-safe.cil.csafe1.610.880.628s0.026s
ldv-regression/test_union.c-safe.cil.csafe1.540.800.562s0.015s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.460.750.513s0.014s
ldv-regression/test_union_cast-1-safe.cil.csafe1.660.970.613s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.680.950.677s0.040s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.410.850.542s0.025s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.710.920.691s0.020s
ldv-regression/volatile_alias.c-safe.cil.csafe1.651.030.743s0.022s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.710.870.620s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.452.372.101s0.621s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.352.171.900s0.604s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.432.341.991s0.637s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.741.841.526s0.490s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.721.761.507s0.466s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.681.881.633s0.582s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.671.761.512s0.524s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.841.961.683s0.574s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.891.921.655s0.584s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.801.851.568s0.475s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.222.081.799s0.596s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.941.951.666s0.518s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.931.801.508s0.491s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.705.515.218s0.509s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe17.2910.269.897s6.979s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown91.9064.9564.397s62.462s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe14.115.204.915s0.657s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown78.8863.7463.285s40.111s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe15.148.237.854s5.943s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown89.8963.7063.310s61.058s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe6.102.562.303s0.195s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe10.844.193.925s0.382s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe11.377.326.976s4.905s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown80.9061.5361.082s57.390s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe4.882.382.111s0.462s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe44.8032.1731.628s23.007s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe4.692.382.101s0.895s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown91.1063.5763.086s61.413s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown90.0166.6366.120s62.296s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown87.6062.8762.170s61.057s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe7.684.684.369s3.034s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown4.492.342.067s0.822s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown92.1467.5467.040s61.447s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.542.231.967s0.883s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown87.0462.5162.001s60.115s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown88.3762.6662.150s60.394s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.131.501.236s0.277s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown85.1364.0963.562s61.877s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown91.1264.5664.078s61.892s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown84.9564.0063.501s61.374s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe6.904.023.725s2.386s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown85.7562.5561.860s60.783s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown82.8962.5761.988s60.592s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown89.5762.7962.271s61.132s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown91.8964.8964.378s61.745s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.231.631.363s0.357s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown102.1863.4462.920s55.757s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe2.821.491.226s0.164s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown83.7062.7862.243s58.170s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown92.7862.3661.843s60.071s