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-abm
branch-r5668
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202811.832064.951660.4321230.019
correct results1791955.591303.241246.776852.252
false negatives00000
false positives1942.1322.6717.5462.915
score (220 files, max score: 356)244
pthread/fib_bench_BUG.cil.cunknown1.270.770.543s0.030s
pthread/fib_bench_longer_BUG.cil.cunknown1.310.770.528s0.030s
pthread/queue_BUG.cil.cunknown1.640.930.667s0.091s
pthread/reorder_5_BUG.cil.cunknown1.861.000.718s0.110s
pthread/twostage_3_BUG.cil.cunknown1.971.120.885s0.147s
pthread/fib_bench.cil.cunknown1.540.860.617s0.023s
pthread/fib_bench_longer.cil.cunknown1.330.770.520s0.025s
pthread/queue_ok.cil.cunknown1.951.030.784s0.113s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe18.4312.0611.641s8.251s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.483.623.316s1.737s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe9.484.704.390s2.435s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.602.742.385s1.123s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe14.048.267.896s5.209s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.395.875.561s3.647s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.035.234.881s2.983s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.726.335.948s3.818s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.051.701.424s0.501s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.582.312.001s0.936s
ntdrivers/cdaudio.BUG.i.cil.cunsafe15.088.027.704s4.560s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.436.275.917s3.029s
ntdrivers/floppy.BUG.i.cil.cunsafe12.686.816.362s3.296s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.864.063.753s1.633s
ntdrivers/parport.BUG.i.cil.cunsafe21.4213.2312.843s7.256s
ntdrivers/cdaudio.i.cil.csafe17.6110.069.677s5.899s
ntdrivers/diskperf.i.cil.csafe11.906.506.142s3.623s
ntdrivers/floppy.i.cil.csafe15.168.778.390s4.454s
ntdrivers/parport.i.cil.csafe28.2419.4218.964s11.745s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.383.062.792s1.603s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.892.652.375s1.272s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.943.152.859s1.471s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.672.762.477s1.120s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.7414.4714.063s10.951s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe63.1456.6556.157s50.653s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.60115.59--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe17.3612.7312.371s9.766s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.202.402.106s0.934s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.592.412.131s1.115s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.061.070.793s0.058s
ssh-simplified/s3_clnt_1.cil.csafe10.697.246.945s4.936s
ssh-simplified/s3_clnt_2.cil.csafe9.125.765.456s3.210s
ssh-simplified/s3_clnt_3.cil.csafe7.934.704.362s2.826s
ssh-simplified/s3_clnt_4.cil.csafe11.988.488.180s5.167s
ssh-simplified/s3_srvr_1a.cil.csafe4.772.482.158s1.389s
ssh-simplified/s3_srvr_1b.cil.csafe2.141.180.913s0.223s
ssh-simplified/s3_srvr_1.cil.cout of memory65.4361.11--
ssh-simplified/s3_srvr_3.cil.csafe24.2919.3318.922s13.583s
ssh-simplified/s3_srvr_4.cil.csafe10.116.195.839s4.463s
ssh-simplified/s3_srvr_6.cil.ctimeout119.58115.15--
ssh-simplified/s3_srvr_7.cil.cunknown65.2561.8061.499s60.419s
ssh-simplified/s3_srvr_8.cil.csafe15.4311.4411.123s8.289s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.773.713.449s1.865s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe5.292.892.579s1.199s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe5.202.762.483s1.099s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.672.622.362s1.183s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.422.632.365s1.287s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.902.512.244s1.108s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe5.042.472.199s1.054s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.802.502.235s1.006s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.743.042.767s1.377s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown66.4462.4462.125s60.601s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.3619.6319.248s17.331s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe37.0531.3130.892s28.005s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.792.452.193s1.068s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.377.236.920s5.507s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe29.4124.2123.722s21.780s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.823.633.334s1.974s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.2314.6314.273s12.099s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.113.263.000s1.638s
ssh/s3_clnt.blast.01.i.cil.csafe9.065.485.171s3.397s
ssh/s3_clnt.blast.03.i.cil.csafe13.449.669.321s6.425s
ssh/s3_clnt.blast.04.i.cil.csafe12.228.027.706s4.452s
ssh/s3_srvr.blast.01.i.cil.csafe33.3928.6228.192s23.917s
ssh/s3_srvr.blast.06.i.cil.csafe25.1019.5619.140s14.402s
ssh/s3_srvr.blast.07.i.cil.cunknown67.3863.6563.314s61.741s
ssh/s3_srvr.blast.08.i.cil.csafe23.9918.7318.293s14.815s
ssh/s3_srvr.blast.09.i.cil.cunknown66.6362.1761.800s59.800s
ssh/s3_srvr.blast.10.i.cil.csafe12.007.216.867s5.174s
ssh/s3_srvr.blast.12.i.cil.csafe14.289.489.061s7.241s
ssh/s3_srvr.blast.13.i.cil.cunknown66.7762.7862.453s60.689s
ssh/s3_srvr.blast.14.i.cil.csafe39.6333.8333.375s27.173s
ssh/s3_srvr.blast.15.i.cil.csafe18.7713.6913.278s7.239s
ssh/s3_srvr.blast.16.i.cil.csafe45.3139.9539.468s27.838s
locks/test_locks_14.BUG.cunsafe2.561.501.244s0.457s
locks/test_locks_15.BUG.cunsafe2.751.671.313s0.513s
locks/test_locks_11.csafe2.401.331.071s0.321s
locks/test_locks_12.csafe2.411.411.156s0.369s
locks/test_locks_13.csafe2.571.551.274s0.483s
locks/test_locks_14.csafe2.641.561.233s0.454s
locks/test_locks_15.csafe2.571.581.316s0.576s
locks/test_locks_5.csafe1.791.210.862s0.119s
locks/test_locks_6.csafe1.820.990.749s0.138s
locks/test_locks_7.csafe1.891.030.779s0.158s
locks/test_locks_8.csafe1.941.060.815s0.193s
locks/test_locks_9.csafe1.941.120.856s0.225s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.621.311.053s0.220s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.101.150.867s0.135s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.231.281.005s0.191s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.551.291.014s0.201s
heap-manipulation/dll_of_dll.cil.cunknown1.951.050.773s0.133s
heap-manipulation/merge_sort.cil.csafe1.971.030.761s0.085s
heap-manipulation/sll_to_dll_rev.cil.cunknown13.8511.8111.553s8.816s
list-properties/alternating_list.cil.csafe1.971.050.761s0.157s
list-properties/list.cil.csafe2.421.230.928s0.266s
list-properties/list_flag.cil.csafe2.271.180.915s0.190s
list-properties/simple.cil.cunsafe2.221.300.996s0.186s
list-properties/simple_built_from_end.cil.cunsafe2.001.020.759s0.146s
list-properties/splice.cil.cunsafe3.682.271.937s0.805s
systemc/token_ring.01.BUG.cil.cunsafe3.251.831.569s0.629s
systemc/token_ring.02.BUG.cil.cunsafe6.303.142.819s1.465s
systemc/token_ring.03.BUG.cil.cunsafe8.284.794.479s2.498s
systemc/transmitter.01.BUG.cil.cunsafe2.751.471.219s0.386s
systemc/transmitter.02.BUG.cil.cunsafe3.842.071.791s0.730s
systemc/transmitter.03.BUG.cil.cunsafe4.932.652.350s0.957s
systemc/transmitter.04.BUG.cil.cunsafe5.652.942.651s1.162s
systemc/bist_cell.cil.csafe19.4316.1615.878s13.827s
systemc/kundu.cil.csafe67.0060.9760.643s56.998s
systemc/mem_slave_tlm.1.cil.cexception49.3245.85--
systemc/mem_slave_tlm.2.cil.csafe71.5465.8265.468s62.959s
systemc/pc_sfifo_1.cil.csafe6.493.513.237s1.748s
systemc/pc_sfifo_2.cil.csafe9.515.605.314s3.243s
systemc/pc_sfifo_3.cil.csafe7.704.354.056s2.334s
systemc/token_ring.01.cil.csafe9.495.545.245s2.999s
systemc/token_ring.04.cil.csafe72.0667.5867.245s64.889s
systemc/toy.cil.csafe69.5662.1161.717s59.313s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.811.050.763s0.034s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.781.160.839s0.062s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.751.020.719s0.025s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.630.900.646s0.065s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.801.010.731s0.023s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.621.010.703s0.018s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.801.190.838s0.063s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.780.990.728s0.043s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.541.301.040s0.228s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.571.471.212s0.458s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.761.020.750s0.059s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.660.920.648s0.038s
ldv-regression/alias_of_return.c-safe.cil.csafe1.661.010.767s0.038s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.640.920.650s0.019s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.870.980.715s0.046s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.660.870.619s0.020s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.331.210.965s0.248s
ldv-regression/just_assert.c-safe.cil.csafe1.580.860.532s0.011s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.610.890.642s0.018s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.770.950.660s0.018s
ldv-regression/nested_structure-safe.cil.cunsafe1.710.940.700s0.072s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.570.890.622s0.025s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.570.830.581s0.017s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.590.890.644s0.029s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.941.110.845s0.124s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.590.940.643s0.026s
ldv-regression/oomInt.c-safe.cil.csafe1.670.910.634s0.031s
ldv-regression/oomInt.c-safe_1.cil.csafe1.750.920.683s0.036s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.800.980.720s0.062s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.610.850.611s0.025s
ldv-regression/rule60_list2.c-safe.cil.csafe2.111.230.980s0.257s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.500.800.567s0.025s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.650.950.682s0.021s
ldv-regression/test_address.c-safe.cil.cunsafe1.610.870.613s0.028s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.650.920.670s0.025s
ldv-regression/test_malloc-1-safe.cil.csafe1.660.860.625s0.046s
ldv-regression/test_malloc-2-safe.cil.csafe1.750.920.657s0.035s
ldv-regression/test_overflow.c-safe.cil.csafe1.560.830.591s0.035s
ldv-regression/test_union.c-safe.cil.csafe1.470.840.601s0.021s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.550.800.558s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.530.790.560s0.016s
ldv-regression/test_union_cast-2-safe.cil.csafe1.620.860.612s0.031s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.580.860.614s0.027s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.600.850.607s0.020s
ldv-regression/volatile_alias.c-safe.cil.csafe1.720.920.660s0.020s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.670.950.692s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.192.251.976s0.435s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.382.282.018s0.422s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.582.402.102s0.454s
ddv-machzwd/ddv_machzwd_inb.cil.csafe4.242.061.774s0.450s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.132.051.748s0.389s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.871.961.709s0.511s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.861.991.690s0.440s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.982.041.752s0.523s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe4.022.141.796s0.475s
ddv-machzwd/ddv_machzwd_outl.cil.csafe4.232.291.996s0.613s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.002.331.976s0.541s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.072.001.731s0.488s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.132.161.868s0.511s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe15.957.366.928s0.501s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe12.356.305.960s2.287s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe18.218.568.197s3.778s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe11.934.564.201s0.596s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe20.7910.8410.507s3.915s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe11.225.114.779s1.741s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe22.3013.1412.714s5.451s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe8.283.593.308s0.266s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe21.468.307.997s1.306s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.907.096.721s3.068s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe47.0831.0730.696s10.662s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe7.513.343.051s0.668s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe19.0511.6011.245s4.083s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe6.743.413.126s1.154s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe20.3811.0810.716s8.042s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe17.337.947.624s1.437s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe41.2523.4823.001s15.867s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.805.885.495s3.559s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe15.768.227.851s4.921s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe20.4410.009.626s1.237s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.552.201.919s0.784s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe8.264.273.963s1.595s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe23.7412.8912.521s7.899s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe5.422.532.240s0.851s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe17.698.408.001s5.581s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown92.3965.0464.545s61.165s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe22.1211.7211.310s8.035s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.875.044.756s2.319s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe6.302.942.628s1.046s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe9.684.183.860s1.839s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe5.652.972.675s0.981s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe19.899.459.038s5.250s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe5.342.552.245s0.636s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe22.4513.9113.509s5.970s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.022.001.720s0.231s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe15.097.136.760s3.806s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe7.383.553.246s1.309s