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.1402
Test setintegration-predicateAnalysis-abm
branch-r5656
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202787.092051.221652.9141209.262
correct results1781930.691290.711233.046827.678
false negatives00000
false positives1942.3823.1918.1582.956
score (220 files, max score: 356)243
pthread/fib_bench_BUG.cil.cunknown1.881.670.755s0.033s
pthread/fib_bench_longer_BUG.cil.cunknown1.780.940.681s0.032s
pthread/queue_BUG.cil.cunknown2.171.140.870s0.116s
pthread/reorder_5_BUG.cil.cunknown2.211.260.895s0.135s
pthread/twostage_3_BUG.cil.cunknown2.231.120.862s0.126s
pthread/fib_bench.cil.cunknown1.460.820.579s0.029s
pthread/fib_bench_longer.cil.cunknown1.510.830.592s0.032s
pthread/queue_ok.cil.cunknown1.820.980.720s0.094s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe13.938.097.767s5.166s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe6.733.192.922s1.533s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe8.243.973.661s1.959s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe4.842.271.991s0.953s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe12.977.487.110s4.598s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.385.525.214s3.392s
ntdrivers-simplified/floppy_simpl3.cil.csafe9.544.724.389s2.716s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.236.005.657s3.702s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.091.751.475s0.547s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.212.111.835s0.869s
ntdrivers/cdaudio.BUG.i.cil.cunsafe13.866.886.561s3.745s
ntdrivers/diskperf.BUG.i.cil.cunsafe10.365.224.849s2.521s
ntdrivers/floppy.BUG.i.cil.cunsafe11.676.145.820s2.860s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.123.433.076s1.294s
ntdrivers/parport.BUG.i.cil.cunsafe21.6613.0712.652s7.095s
ntdrivers/cdaudio.i.cil.csafe18.5911.0510.649s6.770s
ntdrivers/diskperf.i.cil.csafe13.327.467.105s4.153s
ntdrivers/floppy.i.cil.csafe15.589.198.780s4.495s
ntdrivers/parport.i.cil.csafe31.0021.5821.096s13.327s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.823.423.073s1.856s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.722.682.389s1.298s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.022.932.674s1.450s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.192.271.994s0.914s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.2613.1512.796s9.806s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe57.6251.3150.863s45.858s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.58115.74--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.0713.4413.083s10.285s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.042.201.943s0.866s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.722.412.131s1.082s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.381.250.967s0.074s
ssh-simplified/s3_clnt_1.cil.csafe10.356.826.509s4.527s
ssh-simplified/s3_clnt_2.cil.csafe8.785.495.203s3.263s
ssh-simplified/s3_clnt_3.cil.csafe7.764.694.385s2.855s
ssh-simplified/s3_clnt_4.cil.csafe11.528.227.912s5.079s
ssh-simplified/s3_srvr_1a.cil.csafe4.962.532.224s1.441s
ssh-simplified/s3_srvr_1b.cil.csafe2.201.210.937s0.280s
ssh-simplified/s3_srvr_1.cil.cout of memory72.0167.11--
ssh-simplified/s3_srvr_3.cil.csafe27.2321.9021.442s15.575s
ssh-simplified/s3_srvr_4.cil.csafe10.826.496.145s4.598s
ssh-simplified/s3_srvr_6.cil.ctimeout119.60115.73--
ssh-simplified/s3_srvr_7.cil.cunknown71.6468.9468.584s67.421s
ssh-simplified/s3_srvr_8.cil.csafe16.7813.1712.768s8.945s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.667.225.726s1.591s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.313.893.481s0.904s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.813.593.273s1.084s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe6.334.223.913s1.599s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe6.273.853.513s1.394s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.944.193.912s2.088s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.955.455.183s1.165s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.334.384.035s1.991s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.334.694.354s1.177s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown65.5262.2961.968s59.914s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe26.9420.9820.556s18.522s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe37.9831.6431.213s28.359s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.112.792.515s1.254s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe12.047.807.460s5.839s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe27.2321.9221.485s19.286s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.855.614.269s1.925s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe18.3913.8213.466s11.546s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.673.192.931s1.636s
ssh/s3_clnt.blast.01.i.cil.csafe8.745.605.329s3.588s
ssh/s3_clnt.blast.03.i.cil.csafe13.8810.119.773s6.879s
ssh/s3_clnt.blast.04.i.cil.csafe12.118.077.761s4.196s
ssh/s3_srvr.blast.01.i.cil.csafe35.0529.8429.425s24.602s
ssh/s3_srvr.blast.06.i.cil.csafe27.3321.5821.145s15.980s
ssh/s3_srvr.blast.07.i.cil.cunknown67.2663.9963.640s61.840s
ssh/s3_srvr.blast.08.i.cil.csafe25.3320.1419.642s15.721s
ssh/s3_srvr.blast.09.i.cil.cunknown65.8661.4961.147s58.966s
ssh/s3_srvr.blast.10.i.cil.csafe12.087.156.777s5.057s
ssh/s3_srvr.blast.12.i.cil.csafe14.399.919.450s7.614s
ssh/s3_srvr.blast.13.i.cil.cunknown66.5461.9061.582s59.666s
ssh/s3_srvr.blast.14.i.cil.csafe37.5232.1531.695s25.621s
ssh/s3_srvr.blast.15.i.cil.csafe17.2912.2511.846s6.578s
ssh/s3_srvr.blast.16.i.cil.csafe42.1136.7036.256s25.785s
locks/test_locks_14.BUG.cunsafe2.521.481.234s0.460s
locks/test_locks_15.BUG.cunsafe2.681.491.253s0.507s
locks/test_locks_11.csafe2.491.401.104s0.330s
locks/test_locks_12.csafe2.441.501.246s0.432s
locks/test_locks_13.csafe2.631.451.192s0.427s
locks/test_locks_14.csafe2.641.491.212s0.442s
locks/test_locks_15.csafe2.831.531.248s0.501s
locks/test_locks_5.csafe1.761.040.783s0.133s
locks/test_locks_6.csafe1.861.040.755s0.132s
locks/test_locks_7.csafe2.001.130.885s0.201s
locks/test_locks_8.csafe1.971.150.891s0.237s
locks/test_locks_9.csafe2.051.140.850s0.220s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.641.301.018s0.195s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.841.000.750s0.113s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.181.110.847s0.153s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.881.611.345s0.271s
heap-manipulation/dll_of_dll.cil.cunknown2.201.170.898s0.129s
heap-manipulation/merge_sort.cil.csafe1.941.080.834s0.100s
heap-manipulation/sll_to_dll_rev.cil.cunknown13.9212.0811.835s9.255s
list-properties/alternating_list.cil.csafe2.091.130.868s0.175s
list-properties/list.cil.csafe2.071.090.815s0.202s
list-properties/list_flag.cil.csafe2.151.180.855s0.187s
list-properties/simple.cil.cunsafe2.031.110.866s0.187s
list-properties/simple_built_from_end.cil.cunsafe2.091.260.995s0.220s
list-properties/splice.cil.cunsafe3.672.251.987s0.778s
systemc/token_ring.01.BUG.cil.cunsafe3.282.021.733s0.651s
systemc/token_ring.02.BUG.cil.cunsafe5.262.632.358s1.178s
systemc/token_ring.03.BUG.cil.cunsafe7.043.723.442s1.870s
systemc/transmitter.01.BUG.cil.cunsafe2.391.311.067s0.318s
systemc/transmitter.02.BUG.cil.cunsafe3.652.071.810s0.795s
systemc/transmitter.03.BUG.cil.cunsafe4.642.442.174s0.890s
systemc/transmitter.04.BUG.cil.cunsafe5.702.872.617s1.104s
systemc/bist_cell.cil.csafe19.7016.2215.926s13.932s
systemc/kundu.cil.csafe68.1461.0960.697s56.594s
systemc/mem_slave_tlm.1.cil.cexception35.8130.29--
systemc/mem_slave_tlm.2.cil.csafe68.2563.3363.016s60.735s
systemc/pc_sfifo_1.cil.csafe5.863.222.968s1.568s
systemc/pc_sfifo_2.cil.csafe9.535.775.495s3.346s
systemc/pc_sfifo_3.cil.csafe8.164.173.883s2.232s
systemc/token_ring.01.cil.csafe9.525.565.273s3.025s
systemc/token_ring.04.cil.csafe65.8661.0060.696s57.940s
systemc/toy.cil.csafe68.0260.9260.611s56.040s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.620.940.646s0.029s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.560.910.631s0.058s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.710.870.612s0.017s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.300.71--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.660.940.677s0.017s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.570.920.666s0.019s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.710.940.674s0.050s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.490.850.608s0.034s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.301.220.965s0.223s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.621.461.175s0.459s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.640.930.673s0.045s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.610.930.632s0.042s
ldv-regression/alias_of_return.c-safe.cil.csafe1.510.840.598s0.030s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.580.890.606s0.018s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.500.850.572s0.036s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.670.880.637s0.020s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.391.271.016s0.257s
ldv-regression/just_assert.c-safe.cil.csafe1.550.830.594s0.009s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.620.920.656s0.022s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.710.970.666s0.023s
ldv-regression/nested_structure-safe.cil.cunsafe1.770.960.705s0.065s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.650.890.638s0.025s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.720.910.639s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.430.860.545s0.018s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.931.060.795s0.109s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.580.900.640s0.027s
ldv-regression/oomInt.c-safe.cil.csafe1.770.920.661s0.031s
ldv-regression/oomInt.c-safe_1.cil.csafe1.630.940.692s0.038s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.730.970.736s0.062s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.710.960.723s0.026s
ldv-regression/rule60_list2.c-safe.cil.csafe2.301.230.963s0.239s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.610.890.637s0.025s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.660.950.678s0.018s
ldv-regression/test_address.c-safe.cil.cunsafe1.740.980.677s0.025s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.730.910.635s0.024s
ldv-regression/test_malloc-1-safe.cil.csafe1.500.880.604s0.036s
ldv-regression/test_malloc-2-safe.cil.csafe1.540.870.626s0.032s
ldv-regression/test_overflow.c-safe.cil.csafe1.650.900.654s0.031s
ldv-regression/test_union.c-safe.cil.csafe1.480.820.579s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.660.900.624s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.530.830.601s0.016s
ldv-regression/test_union_cast-2-safe.cil.csafe1.550.810.574s0.028s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.680.930.672s0.021s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.700.910.638s0.020s
ldv-regression/volatile_alias.c-safe.cil.csafe1.640.900.656s0.032s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.580.820.563s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.292.231.980s0.432s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.212.161.908s0.405s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.172.211.941s0.460s
ddv-machzwd/ddv_machzwd_inb.cil.csafe4.081.981.677s0.479s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.122.081.784s0.438s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.152.091.795s0.393s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.092.021.740s0.453s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.941.911.633s0.376s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.961.971.688s0.406s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.991.991.714s0.469s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.001.901.627s0.418s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.252.151.851s0.480s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.101.981.710s0.410s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe16.016.566.261s0.490s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe12.106.165.855s2.217s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe17.098.768.339s4.148s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe14.265.335.053s0.618s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe20.3110.4510.099s3.372s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe10.984.914.619s1.871s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe20.3311.4811.078s4.823s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe9.283.863.583s0.262s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe23.238.978.669s1.299s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe13.707.607.237s3.263s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe46.4430.4830.091s10.558s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe7.343.443.154s0.705s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe18.4510.9510.621s4.792s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.972.782.504s0.886s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe19.5410.5110.115s7.736s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe17.778.087.728s1.432s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe41.2523.3722.824s14.396s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.826.336.007s3.823s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe14.838.297.857s4.807s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe21.759.649.298s1.188s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.542.211.946s0.762s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe8.323.733.431s1.431s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe23.3611.8211.437s8.016s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe5.542.672.370s0.796s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe16.628.017.638s5.164s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown91.3463.9163.406s59.965s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe24.6912.0311.673s8.144s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.344.704.416s2.143s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe6.272.892.618s1.079s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.683.753.450s1.584s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe5.312.802.524s0.880s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe19.949.028.658s4.830s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.862.312.048s0.578s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe25.7615.6215.267s6.219s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.021.991.691s0.226s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe15.037.176.776s3.904s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe7.903.783.428s1.477s