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.0918
Test setintegration-predicateAnalysis-abm
branch-r5631
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2222847.692098.341691.3971256.410
correct results1801989.901329.041269.172871.157
false negatives00000
false positives1938.5220.6216.0042.504
score (222 files, max score: 360)247
pthread/fib_bench_BUG.cil.cunknown1.722.200.738s0.040s
pthread/fib_bench_longer_BUG.cil.cunknown1.650.990.702s0.050s
pthread/queue_BUG.cil.cunknown1.931.120.868s0.086s
pthread/reorder_5_BUG.cil.cunknown2.011.140.850s0.120s
pthread/twostage_3_BUG.cil.cunknown1.981.090.829s0.141s
pthread/fib_bench.cil.cunknown1.570.920.622s0.028s
pthread/fib_bench_longer.cil.cunknown1.590.980.714s0.031s
pthread/queue_ok.cil.cunknown2.021.320.986s0.125s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe16.219.989.616s6.664s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.583.473.193s1.683s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe8.943.893.553s1.971s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.162.542.236s1.073s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.016.986.652s4.249s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.825.475.167s3.457s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.004.804.510s2.789s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.566.105.755s3.635s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.311.771.474s0.523s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.422.281.968s0.881s
ntdrivers/cdaudio.BUG.i.cil.cunsafe14.597.276.921s3.886s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.115.775.470s2.859s
ntdrivers/floppy.BUG.i.cil.cunsafe12.186.746.242s3.032s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.093.573.194s1.365s
ntdrivers/parport.BUG.i.cil.cunsafe20.5612.1111.685s6.080s
ntdrivers/cdaudio.i.cil.csafe18.0510.369.962s6.078s
ntdrivers/diskperf.i.cil.csafe12.666.846.466s3.841s
ntdrivers/floppy.i.cil.csafe16.319.489.129s4.657s
ntdrivers/parport.i.cil.csafe28.9619.8419.327s11.315s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.503.293.023s1.909s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.132.952.574s1.392s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.243.192.887s1.503s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.482.512.228s0.928s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.0513.3512.980s10.102s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe60.3253.4152.959s47.814s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.51115.46--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.5213.9513.573s10.768s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.072.261.979s0.960s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.562.472.209s1.159s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.341.290.976s0.092s
ssh-simplified/s3_clnt_1.cil.csafe10.867.757.356s5.189s
ssh-simplified/s3_clnt_2.cil.csafe9.926.085.775s3.574s
ssh-simplified/s3_clnt_3.cil.csafe8.184.854.540s2.856s
ssh-simplified/s3_clnt_4.cil.csafe12.128.618.338s5.327s
ssh-simplified/s3_srvr_1a.cil.csafe5.012.612.289s1.483s
ssh-simplified/s3_srvr_1b.cil.csafe2.061.220.916s0.257s
ssh-simplified/s3_srvr_1.cil.cout of memory69.4065.38--
ssh-simplified/s3_srvr_3.cil.csafe26.4420.6620.187s14.662s
ssh-simplified/s3_srvr_4.cil.csafe11.387.537.188s5.254s
ssh-simplified/s3_srvr_6.cil.ctimeout119.61114.73--
ssh-simplified/s3_srvr_7.cil.cunknown72.9770.4570.127s68.832s
ssh-simplified/s3_srvr_8.cil.csafe16.4711.3611.023s8.123s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe7.343.252.937s1.459s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe5.112.582.306s1.087s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe5.162.682.404s1.119s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe6.253.082.738s1.345s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.762.682.396s1.230s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe5.403.002.621s1.238s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe5.112.602.333s1.132s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.892.602.294s0.998s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe6.173.212.917s1.434s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown67.2062.9062.576s61.015s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe26.5620.8620.450s18.477s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe38.6132.6132.219s29.342s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.282.902.647s1.321s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe12.108.017.702s5.952s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe28.6923.3522.962s20.370s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe8.244.973.629s2.154s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe18.2514.2413.839s11.314s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.975.654.335s1.768s
ssh/s3_clnt.blast.01.i.cil.csafe8.147.567.058s4.259s
ssh/s3_clnt.blast.03.i.cil.csafe13.6512.4411.102s6.320s
ssh/s3_clnt.blast.04.i.cil.csafe11.707.627.319s4.272s
ssh/s3_srvr.blast.01.i.cil.csafe34.4629.9129.473s25.070s
ssh/s3_srvr.blast.06.i.cil.csafe26.1420.4119.968s14.989s
ssh/s3_srvr.blast.07.i.cil.cunknown69.8266.1165.805s64.277s
ssh/s3_srvr.blast.08.i.cil.csafe24.3919.1418.734s15.375s
ssh/s3_srvr.blast.09.i.cil.cunknown66.2861.8761.521s59.330s
ssh/s3_srvr.blast.10.i.cil.csafe11.827.226.882s4.921s
ssh/s3_srvr.blast.12.i.cil.csafe14.349.358.955s7.062s
ssh/s3_srvr.blast.13.i.cil.cunknown65.9261.5161.168s59.281s
ssh/s3_srvr.blast.14.i.cil.csafe37.5732.0631.625s25.829s
ssh/s3_srvr.blast.15.i.cil.csafe15.9911.3610.966s5.656s
ssh/s3_srvr.blast.16.i.cil.csafe41.3735.7035.277s25.025s
locks/test_locks_14.BUG.cunsafe2.451.401.155s0.384s
locks/test_locks_15.BUG.cunsafe2.621.511.255s0.481s
locks/test_locks_10.csafe2.111.200.946s0.257s
locks/test_locks_11.csafe2.081.170.915s0.277s
locks/test_locks_12.csafe2.321.271.019s0.354s
locks/test_locks_13.csafe2.531.441.180s0.401s
locks/test_locks_14.csafe2.851.761.452s0.561s
locks/test_locks_15.csafe2.701.581.255s0.480s
locks/test_locks_5.csafe1.690.920.672s0.099s
locks/test_locks_6.csafe1.761.030.791s0.138s
locks/test_locks_7.csafe1.861.080.808s0.155s
locks/test_locks_8.csafe1.851.050.807s0.178s
locks/test_locks_9.csafe2.151.240.996s0.229s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.601.391.089s0.170s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.201.170.911s0.107s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.291.250.965s0.173s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.641.451.181s0.194s
heap-manipulation/dll_of_dll.cil.cunknown1.910.980.745s0.103s
heap-manipulation/merge_sort.cil.csafe1.961.080.824s0.075s
heap-manipulation/sll_to_dll_rev.cil.cunknown13.0211.2510.959s8.353s
list-properties/alternating_list.cil.csafe1.870.980.744s0.151s
list-properties/list.cil.csafe1.881.090.783s0.198s
list-properties/list_flag.cil.csafe1.941.070.830s0.182s
list-properties/simple.cil.cunsafe1.891.000.747s0.150s
list-properties/simple_built_from_end.cil.cunsafe1.851.000.755s0.142s
list-properties/splice.cil.cunsafe3.372.161.908s0.721s
systemc/token_ring.01.BUG.cil.cunsafe3.011.721.464s0.532s
systemc/token_ring.02.BUG.cil.cunsafe5.192.762.502s1.226s
systemc/token_ring.03.BUG.cil.cunsafe7.123.883.597s2.030s
systemc/transmitter.01.BUG.cil.cunsafe2.371.321.074s0.311s
systemc/transmitter.02.BUG.cil.cunsafe3.431.891.636s0.656s
systemc/transmitter.03.BUG.cil.cunsafe4.422.272.014s0.808s
systemc/transmitter.04.BUG.cil.cunsafe5.562.722.466s1.009s
systemc/bist_cell.cil.csafe19.1815.8615.592s13.530s
systemc/kundu.cil.csafe68.4060.9460.598s57.260s
systemc/mem_slave_tlm.1.cil.cexception45.2239.65--
systemc/mem_slave_tlm.2.cil.csafe66.1661.0760.685s58.325s
systemc/mem_slave_tlm.4.cil.csafe67.6662.0361.658s58.706s
systemc/pc_sfifo_1.cil.csafe5.903.112.845s1.567s
systemc/pc_sfifo_2.cil.csafe9.295.044.759s2.932s
systemc/pc_sfifo_3.cil.csafe7.663.983.715s2.160s
systemc/token_ring.01.cil.csafe8.784.964.710s2.683s
systemc/token_ring.04.cil.csafe66.2760.9360.618s57.280s
systemc/toy.cil.csafe69.6360.9260.593s57.826s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.460.840.606s0.031s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.540.850.624s0.052s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.470.800.564s0.016s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.090.62--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.390.780.545s0.017s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.460.850.606s0.017s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.480.820.586s0.038s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.490.860.624s0.034s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.161.200.944s0.214s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.141.281.043s0.421s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.460.830.588s0.042s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.510.820.575s0.036s
ldv-regression/alias_of_return.c-safe.cil.csafe1.520.810.577s0.029s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.590.820.568s0.018s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.590.920.666s0.039s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.450.820.585s0.019s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.051.160.913s0.223s
ldv-regression/just_assert.c-safe.cil.csafe1.410.750.521s0.010s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.370.780.532s0.017s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.580.880.642s0.017s
ldv-regression/nested_structure-safe.cil.cunsafe1.540.840.603s0.041s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.420.790.556s0.020s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.480.780.546s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.520.830.588s0.026s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.690.980.743s0.101s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.500.800.564s0.023s
ldv-regression/oomInt.c-safe.cil.csafe1.460.800.564s0.030s
ldv-regression/oomInt.c-safe_1.cil.csafe1.490.800.567s0.032s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.520.860.632s0.048s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.470.800.571s0.023s
ldv-regression/rule60_list2.c-safe.cil.csafe2.021.271.019s0.262s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.290.750.524s0.024s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.480.790.547s0.017s
ldv-regression/test_address.c-safe.cil.cunsafe1.460.800.555s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.440.780.547s0.018s
ldv-regression/test_malloc-1-safe.cil.csafe1.500.790.557s0.029s
ldv-regression/test_malloc-2-safe.cil.csafe1.490.790.554s0.026s
ldv-regression/test_overflow.c-safe.cil.csafe1.490.800.566s0.029s
ldv-regression/test_union.c-safe.cil.csafe1.510.810.582s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.480.780.547s0.015s
ldv-regression/test_union_cast-1-safe.cil.csafe1.470.770.540s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.460.860.617s0.023s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.460.790.559s0.020s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.570.860.615s0.019s
ldv-regression/volatile_alias.c-safe.cil.csafe1.730.900.641s0.017s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.660.890.632s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.272.231.966s0.418s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.232.211.950s0.453s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.942.001.730s0.358s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.751.931.626s0.445s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.791.841.581s0.443s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.881.851.577s0.454s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.202.151.783s0.478s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.192.081.776s0.461s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.871.921.598s0.448s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.841.981.682s0.417s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.841.841.585s0.417s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.801.971.711s0.435s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.881.921.654s0.450s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe16.037.146.846s0.521s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe12.506.376.036s2.111s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe15.707.737.335s3.152s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe15.065.635.351s0.611s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe19.5010.009.662s3.221s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe10.614.724.393s1.636s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe20.4211.4111.025s4.783s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe9.473.773.432s0.268s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe22.908.858.557s1.377s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe13.267.116.748s3.122s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe45.5429.6829.285s12.275s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe7.503.503.130s0.704s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe18.4911.5311.127s4.415s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe6.182.892.591s0.792s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe19.299.499.076s6.372s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe18.168.087.715s1.284s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe39.6421.9721.486s11.768s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe13.706.946.586s4.152s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe15.247.977.566s4.412s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe22.1810.6510.278s1.364s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.922.402.095s0.759s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe8.323.963.612s1.494s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe23.8813.3812.926s7.635s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe5.552.772.489s0.836s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe15.507.567.154s4.606s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown85.7364.4464.005s60.071s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe21.4110.409.799s6.112s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.804.804.507s2.287s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe6.183.022.737s0.981s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.683.573.254s1.447s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.962.412.111s0.783s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe20.198.558.105s3.810s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.952.241.977s0.536s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe22.2211.9711.623s4.358s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.801.721.472s0.175s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe13.376.015.016s2.446s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe7.123.212.894s1.020s