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.1711
Test setintegration-predicateAnalysis-abm
branch-r5680
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202710.742020.711621.4921203.790
correct results1791860.301262.731207.303824.630
false negatives00000
false positives1938.6221.4216.6112.711
score (220 files, max score: 356)244
pthread/fib_bench_BUG.cil.cunknown1.260.760.507s0.030s
pthread/fib_bench_longer_BUG.cil.cunknown1.310.760.520s0.023s
pthread/queue_BUG.cil.cunknown1.560.890.633s0.094s
pthread/reorder_5_BUG.cil.cunknown1.680.900.658s0.104s
pthread/twostage_3_BUG.cil.cunknown1.911.040.785s0.145s
pthread/fib_bench.cil.cunknown1.740.950.699s0.027s
pthread/fib_bench_longer.cil.cunknown1.650.900.647s0.027s
pthread/queue_ok.cil.cunknown1.800.940.689s0.090s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe14.788.838.475s5.906s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe8.184.263.892s1.966s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe9.414.574.236s2.327s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.182.542.227s1.023s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.958.347.963s4.898s
ntdrivers-simplified/diskperf_simpl1.cil.csafe9.507.425.904s3.206s
ntdrivers-simplified/floppy_simpl3.cil.csafe9.519.048.707s3.338s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.067.737.374s3.783s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.341.821.503s0.580s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.712.522.235s0.985s
ntdrivers/cdaudio.BUG.i.cil.cunsafe15.058.197.869s4.451s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.265.855.464s2.800s
ntdrivers/floppy.BUG.i.cil.cunsafe12.726.676.219s3.058s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.663.713.388s1.467s
ntdrivers/parport.BUG.i.cil.cunsafe21.0512.8512.449s7.103s
ntdrivers/cdaudio.i.cil.csafe18.1110.9110.531s6.534s
ntdrivers/diskperf.i.cil.csafe12.777.417.059s4.253s
ntdrivers/floppy.i.cil.csafe15.379.519.122s4.780s
ntdrivers/parport.i.cil.csafe28.4119.5119.063s11.618s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.463.212.914s1.799s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.962.752.479s1.386s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.923.062.802s1.505s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.452.462.179s1.016s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.5313.9113.546s10.466s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe63.9357.4456.896s51.581s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.68115.54--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe17.9713.3713.007s10.082s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.712.011.751s0.824s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.632.482.217s1.177s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.111.040.791s0.059s
ssh-simplified/s3_clnt_1.cil.csafe10.466.636.348s4.393s
ssh-simplified/s3_clnt_2.cil.csafe9.175.715.415s3.363s
ssh-simplified/s3_clnt_3.cil.csafe7.854.494.211s2.718s
ssh-simplified/s3_clnt_4.cil.csafe11.908.538.223s5.306s
ssh-simplified/s3_srvr_1a.cil.csafe4.492.372.089s1.353s
ssh-simplified/s3_srvr_1b.cil.csafe1.981.060.809s0.227s
ssh-simplified/s3_srvr_1.cil.cout of memory66.8862.69--
ssh-simplified/s3_srvr_3.cil.csafe25.1219.7219.282s14.070s
ssh-simplified/s3_srvr_4.cil.csafe10.466.526.185s4.669s
ssh-simplified/s3_srvr_6.cil.ctimeout119.63114.88--
ssh-simplified/s3_srvr_7.cil.cunknown66.6863.1462.850s61.650s
ssh-simplified/s3_srvr_8.cil.csafe16.1911.5611.217s8.129s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.423.343.036s1.639s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe5.162.772.496s1.198s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.372.272.006s0.916s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.562.832.556s1.266s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.582.722.427s1.247s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.552.532.267s1.096s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.702.462.199s1.052s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.802.572.294s1.088s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.533.062.787s1.356s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown68.1264.3063.976s62.398s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.5320.5120.098s18.037s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.0630.2229.758s26.833s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.812.662.387s1.141s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.087.236.905s5.401s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe28.8923.0422.644s20.692s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.943.863.581s2.094s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.6114.9514.576s12.530s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.183.323.051s1.789s
ssh/s3_clnt.blast.01.i.cil.csafe8.304.904.615s3.077s
ssh/s3_clnt.blast.03.i.cil.csafe12.578.748.448s5.861s
ssh/s3_clnt.blast.04.i.cil.csafe11.417.417.121s4.127s
ssh/s3_srvr.blast.01.i.cil.csafe31.8826.6726.303s22.459s
ssh/s3_srvr.blast.06.i.cil.csafe27.7222.0321.574s16.366s
ssh/s3_srvr.blast.07.i.cil.cunknown65.4961.8961.537s59.922s
ssh/s3_srvr.blast.08.i.cil.csafe25.4320.0319.523s15.418s
ssh/s3_srvr.blast.09.i.cil.cunknown66.4461.8961.546s59.538s
ssh/s3_srvr.blast.10.i.cil.csafe11.656.786.421s4.785s
ssh/s3_srvr.blast.12.i.cil.csafe13.809.519.039s7.263s
ssh/s3_srvr.blast.13.i.cil.cunknown67.4863.3863.078s61.028s
ssh/s3_srvr.blast.14.i.cil.csafe39.1733.0832.630s26.716s
ssh/s3_srvr.blast.15.i.cil.csafe17.4612.3811.990s6.496s
ssh/s3_srvr.blast.16.i.cil.csafe46.5941.1540.584s28.498s
locks/test_locks_14.BUG.cunsafe2.541.481.199s0.392s
locks/test_locks_15.BUG.cunsafe2.621.481.219s0.450s
locks/test_locks_11.csafe2.341.291.024s0.320s
locks/test_locks_12.csafe2.581.501.201s0.367s
locks/test_locks_13.csafe2.561.511.229s0.486s
locks/test_locks_14.csafe2.851.691.429s0.558s
locks/test_locks_15.csafe2.951.611.342s0.498s
locks/test_locks_5.csafe1.760.960.713s0.119s
locks/test_locks_6.csafe1.871.070.818s0.133s
locks/test_locks_7.csafe2.031.230.930s0.227s
locks/test_locks_8.csafe1.981.090.826s0.181s
locks/test_locks_9.csafe2.151.361.091s0.282s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.561.441.177s0.225s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.961.010.747s0.112s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.201.270.963s0.203s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.491.301.037s0.197s
heap-manipulation/dll_of_dll.cil.cunknown1.981.070.793s0.125s
heap-manipulation/merge_sort.cil.csafe2.271.260.976s0.107s
heap-manipulation/sll_to_dll_rev.cil.cunknown14.3712.4212.147s9.353s
list-properties/alternating_list.cil.csafe1.991.170.886s0.194s
list-properties/list.cil.csafe2.321.381.059s0.293s
list-properties/list_flag.cil.csafe2.101.160.893s0.191s
list-properties/simple.cil.cunsafe1.901.140.884s0.200s
list-properties/simple_built_from_end.cil.cunsafe2.141.240.972s0.180s
list-properties/splice.cil.cunsafe3.532.322.027s0.765s
systemc/token_ring.01.BUG.cil.cunsafe3.221.941.643s0.589s
systemc/token_ring.02.BUG.cil.cunsafe5.863.292.975s1.361s
systemc/token_ring.03.BUG.cil.cunsafe7.644.514.146s2.120s
systemc/transmitter.01.BUG.cil.cunsafe3.091.741.381s0.395s
systemc/transmitter.02.BUG.cil.cunsafe3.942.111.832s0.700s
systemc/transmitter.03.BUG.cil.cunsafe5.122.882.562s1.117s
systemc/transmitter.04.BUG.cil.cunsafe6.453.383.030s1.231s
systemc/bist_cell.cil.csafe19.9716.4516.151s13.956s
systemc/kundu.cil.csafe66.5160.9560.615s56.641s
systemc/mem_slave_tlm.1.cil.cexception45.5940.77--
systemc/mem_slave_tlm.2.cil.csafe69.3564.1463.791s61.326s
systemc/pc_sfifo_1.cil.csafe5.412.992.726s1.432s
systemc/pc_sfifo_2.cil.csafe8.325.224.973s3.029s
systemc/pc_sfifo_3.cil.csafe6.803.633.353s1.891s
systemc/token_ring.01.cil.csafe8.545.255.006s2.790s
systemc/token_ring.04.cil.csafe65.7561.3261.024s58.249s
systemc/toy.cil.csafe67.2061.7261.418s59.117s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.400.800.555s0.029s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.560.890.661s0.054s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.450.860.618s0.019s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.460.830.595s0.049s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.400.810.551s0.018s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.370.790.552s0.018s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.390.810.574s0.042s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.440.850.598s0.034s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.161.200.969s0.241s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.291.351.114s0.429s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.380.820.579s0.044s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.450.840.593s0.038s
ldv-regression/alias_of_return.c-safe.cil.csafe1.360.800.545s0.030s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.350.780.544s0.019s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.420.840.592s0.041s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.330.770.525s0.018s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.041.180.933s0.226s
ldv-regression/just_assert.c-safe.cil.csafe1.370.770.520s0.010s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.380.780.540s0.018s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.430.820.574s0.018s
ldv-regression/nested_structure-safe.cil.cunsafe1.780.870.640s0.053s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.710.910.649s0.026s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.620.830.575s0.016s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.570.910.643s0.025s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.921.040.746s0.103s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.390.800.554s0.023s
ldv-regression/oomInt.c-safe.cil.csafe1.410.810.576s0.032s
ldv-regression/oomInt.c-safe_1.cil.csafe1.560.890.660s0.036s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.670.980.750s0.057s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.390.810.575s0.024s
ldv-regression/rule60_list2.c-safe.cil.csafe2.201.351.071s0.319s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.390.790.564s0.034s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.360.790.548s0.017s
ldv-regression/test_address.c-safe.cil.cunsafe1.510.830.595s0.029s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.540.840.611s0.020s
ldv-regression/test_malloc-1-safe.cil.csafe1.400.850.577s0.033s
ldv-regression/test_malloc-2-safe.cil.csafe1.551.010.735s0.029s
ldv-regression/test_overflow.c-safe.cil.csafe1.400.800.568s0.029s
ldv-regression/test_union.c-safe.cil.csafe1.470.850.619s0.021s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.410.850.581s0.026s
ldv-regression/test_union_cast-1-safe.cil.csafe1.400.900.677s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.380.810.554s0.031s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.310.780.540s0.022s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.400.830.596s0.025s
ldv-regression/volatile_alias.c-safe.cil.csafe1.440.820.565s0.029s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.580.940.678s0.028s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.762.131.869s0.378s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.702.111.865s0.484s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.831.961.685s0.366s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.251.641.394s0.355s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.521.841.586s0.360s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.281.631.364s0.354s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.481.811.555s0.438s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.221.631.386s0.376s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.251.671.430s0.360s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.371.701.458s0.360s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.631.871.627s0.428s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.261.661.417s0.370s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.281.671.410s0.372s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.335.945.676s0.475s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe10.786.025.730s2.238s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.007.146.819s3.337s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe13.075.094.841s0.671s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe18.7510.109.764s3.735s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe9.764.674.355s1.833s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe20.6012.2511.892s4.919s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.403.072.806s0.210s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe17.126.586.296s1.075s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe11.036.446.106s2.835s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe43.6928.2627.889s9.547s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.953.453.130s0.693s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.4311.0110.646s3.686s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.342.762.469s0.880s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe18.6910.4710.138s7.421s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe14.796.536.237s0.958s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe37.4921.0020.600s12.359s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe10.525.495.166s3.408s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe13.076.796.438s3.826s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe19.819.509.118s1.120s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.322.262.012s0.676s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe7.533.693.397s1.631s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe21.3611.6611.326s7.241s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.222.171.923s0.685s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe14.727.507.154s4.948s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown90.2964.1863.754s61.107s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe21.7710.7910.454s7.589s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe8.504.374.085s1.960s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.112.612.341s0.939s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.103.683.374s1.599s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.732.412.125s0.816s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe19.759.198.841s5.098s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.682.292.024s0.535s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe20.3612.5812.151s5.977s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.581.691.442s0.192s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe11.815.755.412s3.190s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe6.102.922.646s1.065s