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.1411
Test setintegration-predicateAnalysis
branch-r5668
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2213542.282592.652315.8961916.451
correct results1611086.49703.75653.094380.166
false negatives00000
false positives1938.7820.6615.8652.692
score (221 files, max score: 357)211
pthread/fib_bench_BUG.cil.cunknown1.861.050.730s0.033s
pthread/fib_bench_longer_BUG.cil.cunknown1.861.040.708s0.028s
pthread/queue_BUG.cil.cunknown2.201.260.977s0.129s
pthread/reorder_5_BUG.cil.cunknown2.091.120.836s0.124s
pthread/twostage_3_BUG.cil.cunknown2.121.220.860s0.138s
pthread/fib_bench.cil.cunknown1.620.870.631s0.028s
pthread/fib_bench_longer.cil.cunknown1.720.960.693s0.026s
pthread/queue_ok.cil.cunknown1.881.080.790s0.094s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.514.063.725s2.138s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe4.052.291.985s0.880s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.482.572.215s1.019s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.241.781.439s0.488s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.863.533.193s2.161s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.582.862.557s1.779s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.762.111.766s0.860s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.392.402.111s1.176s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.641.341.074s0.346s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.001.501.199s0.494s
ntdrivers/cdaudio.BUG.i.cil.cunsafe10.345.635.321s2.982s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.483.943.615s1.987s
ntdrivers/floppy.BUG.i.cil.cunsafe11.196.796.407s4.247s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe4.882.712.382s0.969s
ntdrivers/parport.BUG.i.cil.cunknown88.5166.9063.152s61.523s
ntdrivers/cdaudio.i.cil.csafe9.084.894.586s2.779s
ntdrivers/diskperf.i.cil.csafe5.483.192.898s1.806s
ntdrivers/floppy.i.cil.csafe12.938.568.199s5.793s
ntdrivers/parport.i.cil.cunknown81.2662.5761.972s60.534s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.561.991.716s0.775s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.062.231.962s0.850s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe3.771.941.682s0.745s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe3.892.171.919s0.918s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.621.341.095s0.303s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe6.003.272.984s1.524s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.537.697.375s5.586s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.071.571.286s0.451s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.872.021.758s0.758s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.511.821.560s0.682s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.141.090.832s0.066s
ssh-simplified/s3_clnt_1.cil.csafe8.515.465.131s3.056s
ssh-simplified/s3_clnt_2.cil.csafe8.465.595.257s3.395s
ssh-simplified/s3_clnt_3.cil.csafe9.706.546.213s3.188s
ssh-simplified/s3_clnt_4.cil.csafe8.985.985.662s3.463s
ssh-simplified/s3_srvr_1a.cil.csafe3.621.991.656s1.000s
ssh-simplified/s3_srvr_1b.cil.csafe1.941.040.797s0.144s
ssh-simplified/s3_srvr_1.cil.csafe34.6330.2129.713s21.782s
ssh-simplified/s3_srvr_3.cil.csafe23.8319.7119.232s12.902s
ssh-simplified/s3_srvr_4.cil.csafe13.569.669.219s7.581s
ssh-simplified/s3_srvr_6.cil.csafe16.0411.8611.413s9.671s
ssh-simplified/s3_srvr_7.cil.csafe22.3118.3517.906s16.222s
ssh-simplified/s3_srvr_8.cil.csafe13.689.619.182s6.206s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe4.662.592.298s1.105s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.402.382.098s0.956s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.552.422.120s0.950s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe3.942.161.822s0.817s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.422.392.097s0.964s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.282.241.928s0.821s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.242.161.850s0.801s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.122.191.887s0.783s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.022.652.348s1.067s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.074.073.788s2.458s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe8.124.844.491s2.619s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.234.003.684s1.756s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.863.202.891s1.618s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.302.652.358s1.076s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.317.387.091s5.707s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.122.932.648s1.330s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.344.233.923s1.973s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.282.812.523s1.174s
ssh/s3_clnt.blast.01.i.cil.csafe9.816.275.925s4.012s
ssh/s3_clnt.blast.03.i.cil.csafe8.465.385.059s3.602s
ssh/s3_clnt.blast.04.i.cil.csafe11.117.717.345s5.183s
ssh/s3_srvr.blast.01.i.cil.csafe13.478.688.221s5.426s
ssh/s3_srvr.blast.06.i.cil.csafe16.4311.4710.981s9.162s
ssh/s3_srvr.blast.07.i.cil.csafe14.249.949.473s8.023s
ssh/s3_srvr.blast.08.i.cil.cout of memory92.6588.12--
ssh/s3_srvr.blast.09.i.cil.csafe12.698.648.208s5.964s
ssh/s3_srvr.blast.10.i.cil.csafe52.5247.6047.028s15.836s
ssh/s3_srvr.blast.12.i.cil.csafe40.3735.0634.547s16.016s
ssh/s3_srvr.blast.13.i.cil.csafe23.4518.5818.027s15.627s
ssh/s3_srvr.blast.14.i.cil.csafe36.4531.2030.633s23.753s
ssh/s3_srvr.blast.15.i.cil.csafe13.658.798.277s5.849s
ssh/s3_srvr.blast.16.i.cil.csafe15.9411.1910.663s7.560s
locks/test_locks_14.BUG.cunsafe1.680.990.735s0.101s
locks/test_locks_15.BUG.cunsafe1.761.120.764s0.102s
locks/test_locks_11.csafe1.660.950.705s0.092s
locks/test_locks_12.csafe1.700.960.713s0.114s
locks/test_locks_13.csafe1.860.980.724s0.103s
locks/test_locks_14.csafe1.640.940.691s0.115s
locks/test_locks_15.csafe1.550.900.649s0.111s
locks/test_locks_5.csafe1.520.810.570s0.040s
locks/test_locks_6.csafe1.620.880.654s0.047s
locks/test_locks_7.csafe1.520.850.619s0.059s
locks/test_locks_8.csafe1.580.820.593s0.060s
locks/test_locks_9.csafe1.600.850.604s0.068s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.231.230.993s0.197s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.790.930.692s0.098s
heap-manipulation/merge_sort_BUG.cil.cunsafe1.981.080.832s0.178s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown63.2860.9560.667s57.443s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.351.210.943s0.190s
heap-manipulation/dll_of_dll.cil.cunknown1.890.950.712s0.093s
heap-manipulation/merge_sort.cil.csafe1.800.930.694s0.082s
heap-manipulation/sll_to_dll_rev.cil.cunknown62.7660.9560.678s54.346s
list-properties/alternating_list.cil.csafe1.940.980.722s0.140s
list-properties/list.cil.csafe2.211.200.944s0.217s
list-properties/list_flag.cil.csafe2.001.060.786s0.170s
list-properties/simple.cil.cunsafe1.901.070.809s0.158s
list-properties/simple_built_from_end.cil.cunsafe1.861.070.799s0.131s
list-properties/splice.cil.cunsafe3.141.951.694s0.804s
systemc/token_ring.01.BUG.cil.cunsafe3.271.851.572s0.676s
systemc/token_ring.02.BUG.cil.cunsafe4.532.261.978s1.171s
systemc/token_ring.03.BUG.cil.cunsafe7.994.003.632s2.582s
systemc/transmitter.01.BUG.cil.cunsafe2.421.301.023s0.263s
systemc/transmitter.02.BUG.cil.cunsafe3.061.601.314s0.564s
systemc/transmitter.03.BUG.cil.cunsafe5.122.502.219s1.327s
systemc/transmitter.04.BUG.cil.cunsafe9.445.194.801s3.580s
systemc/bist_cell.cil.csafe2.541.411.074s0.428s
systemc/kundu.cil.csafe16.6312.5011.935s10.313s
systemc/mem_slave_tlm.1.cil.cout of memory57.8153.03--
systemc/mem_slave_tlm.2.cil.csegmentation fault63.2158.10--
systemc/pc_sfifo_1.cil.csafe5.422.492.173s1.465s
systemc/pc_sfifo_2.cil.csafe5.692.952.648s1.692s
systemc/pc_sfifo_3.cil.csafe2.421.311.034s0.362s
systemc/token_ring.01.cil.csafe4.382.161.835s1.053s
systemc/token_ring.04.cil.cunknown74.0261.6760.722s54.364s
systemc/toy.cil.cunknown66.4061.2660.818s57.806s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.590.820.569s0.023s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.660.860.622s0.047s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.550.800.554s0.014s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.810.900.652s0.046s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.520.790.552s0.019s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.570.800.562s0.016s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.610.830.589s0.035s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.600.870.627s0.031s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.800.940.695s0.104s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.121.200.950s0.267s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.630.860.613s0.044s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.560.820.571s0.031s
ldv-regression/alias_of_return.c-safe.cil.csafe1.610.830.596s0.020s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.520.780.546s0.016s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.500.810.570s0.021s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.590.820.562s0.016s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.511.391.129s0.382s
ldv-regression/just_assert.c-safe.cil.csafe1.720.920.664s0.010s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.620.840.591s0.018s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.550.820.577s0.016s
ldv-regression/nested_structure-safe.cil.cunsafe1.870.990.750s0.053s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.530.850.597s0.020s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.590.810.575s0.016s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.540.880.618s0.021s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.900.970.721s0.112s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.550.820.572s0.025s
ldv-regression/oomInt.c-safe.cil.csafe1.530.800.543s0.020s
ldv-regression/oomInt.c-safe_1.cil.csafe1.480.850.605s0.017s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.690.950.699s0.053s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.530.850.603s0.023s
ldv-regression/rule60_list2.c-safe.cil.csafe1.710.890.635s0.096s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.500.780.548s0.018s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.550.870.630s0.025s
ldv-regression/test_address.c-safe.cil.cunsafe1.620.830.591s0.018s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.510.770.537s0.016s
ldv-regression/test_malloc-1-safe.cil.csafe1.550.860.629s0.038s
ldv-regression/test_malloc-2-safe.cil.csafe1.520.800.563s0.030s
ldv-regression/test_overflow.c-safe.cil.csafe1.600.820.576s0.023s
ldv-regression/test_union.c-safe.cil.csafe1.500.770.539s0.014s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.550.870.610s0.019s
ldv-regression/test_union_cast-1-safe.cil.csafe1.530.790.553s0.017s
ldv-regression/test_union_cast-2-safe.cil.csafe1.640.840.598s0.027s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.590.820.572s0.021s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.580.840.583s0.020s
ldv-regression/volatile_alias.c-safe.cil.csafe1.600.810.545s0.018s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.510.780.532s0.018s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.112.181.910s0.671s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.991.991.734s0.504s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.142.101.840s0.583s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.961.971.704s0.571s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.472.221.934s0.703s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.092.091.795s0.512s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.761.811.544s0.520s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.721.841.571s0.620s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe4.302.181.883s0.593s
ddv-machzwd/ddv_machzwd_outl.cil.csafe4.252.111.855s0.623s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.312.111.835s0.641s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.212.161.880s0.617s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.001.961.690s0.568s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.225.795.456s0.535s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe16.9410.159.715s6.785s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown92.4564.7664.218s62.487s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe15.265.885.535s0.685s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown79.3164.6364.167s40.845s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe18.0512.7511.392s7.839s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown80.1262.4161.950s58.425s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.793.152.874s0.210s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe21.797.867.572s0.509s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe14.299.248.869s6.254s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown84.0861.8261.223s52.599s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe5.682.652.357s0.537s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe47.7235.8735.254s24.891s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.982.912.601s1.122s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown90.7964.3263.737s61.723s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown88.7866.3865.850s61.203s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown83.5062.0761.321s59.981s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe9.875.955.599s3.775s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown5.662.792.490s1.003s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown94.1266.6866.114s60.233s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.642.201.900s0.784s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown86.0062.7662.271s60.131s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown85.3264.5764.032s62.085s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.541.841.531s0.371s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown84.8964.5663.863s62.037s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown90.6965.9265.394s62.472s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown79.6065.4663.973s60.734s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.425.124.807s3.126s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown85.8663.8163.055s61.618s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown82.1562.9662.360s60.679s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown86.4061.8061.279s59.941s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown91.2464.3663.839s60.086s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.821.741.478s0.416s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown97.1663.9363.421s57.941s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.651.751.500s0.208s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown85.6163.3062.707s59.960s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown89.7162.7262.135s59.819s