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.1030
Test setintegration-predicateAnalysis-abm
branch-r5643
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2222835.672124.241624.2871210.973
correct results1791886.131262.471208.088832.510
false negatives00000
false positives1938.0021.0116.1752.455
score (222 files, max score: 360)245
pthread/fib_bench_BUG.cil.cunknown1.772.851.506s0.029s
pthread/fib_bench_longer_BUG.cil.cunknown1.703.171.582s0.033s
pthread/queue_BUG.cil.cunknown1.981.441.133s0.084s
pthread/reorder_5_BUG.cil.cunknown1.931.090.800s0.130s
pthread/twostage_3_BUG.cil.cunknown2.061.200.907s0.148s
pthread/fib_bench.cil.cunknown1.671.030.780s0.046s
pthread/fib_bench_longer.cil.cunknown1.510.900.617s0.028s
pthread/queue_ok.cil.cunknown1.790.990.744s0.087s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe14.298.217.842s5.037s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.193.563.255s1.731s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe8.564.133.672s2.050s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe4.832.522.226s0.909s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.667.817.469s4.961s
ntdrivers-simplified/diskperf_simpl1.cil.csafe9.945.575.213s3.405s
ntdrivers-simplified/floppy_simpl3.cil.csafe9.714.934.634s2.889s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.225.595.268s3.303s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.701.521.256s0.464s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.152.061.777s0.788s
ntdrivers/cdaudio.BUG.i.cil.cunsafe13.896.856.515s3.712s
ntdrivers/diskperf.BUG.i.cil.cunsafe10.705.515.189s2.717s
ntdrivers/floppy.BUG.i.cil.cunsafe12.726.666.292s3.025s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.303.383.071s1.306s
ntdrivers/parport.BUG.i.cil.cunsafe20.5013.0112.610s7.155s
ntdrivers/cdaudio.i.cil.csafe18.1510.5210.110s6.268s
ntdrivers/diskperf.i.cil.csafe11.926.336.000s3.527s
ntdrivers/floppy.i.cil.csafe15.838.798.451s4.366s
ntdrivers/parport.i.cil.csafe27.4118.9618.539s11.868s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.723.132.849s1.720s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.192.832.537s1.353s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.183.242.927s1.476s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.422.532.233s1.056s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.7014.6314.255s10.969s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe61.1253.6653.189s47.872s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.60115.44--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe17.6312.9912.627s9.886s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.902.061.784s0.833s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.792.502.217s1.172s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.341.300.981s0.068s
ssh-simplified/s3_clnt_1.cil.csafe11.117.967.667s5.211s
ssh-simplified/s3_clnt_2.cil.csafe9.786.015.685s3.654s
ssh-simplified/s3_clnt_3.cil.csafe8.244.974.661s3.002s
ssh-simplified/s3_clnt_4.cil.csafe12.168.768.442s5.437s
ssh-simplified/s3_srvr_1a.cil.csafe4.722.592.264s1.558s
ssh-simplified/s3_srvr_1b.cil.csafe2.021.070.819s0.212s
ssh-simplified/s3_srvr_1.cil.cout of memory63.9059.55--
ssh-simplified/s3_srvr_3.cil.csafe25.8119.9519.523s14.395s
ssh-simplified/s3_srvr_4.cil.csafe10.386.205.876s4.478s
ssh-simplified/s3_srvr_6.cil.ctimeout119.66115.49--
ssh-simplified/s3_srvr_7.cil.cunknown68.3366.2966.004s64.195s
ssh-simplified/s3_srvr_8.cil.csafe16.4711.9111.559s8.540s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.593.623.336s1.718s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe5.212.982.687s1.339s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe5.092.652.376s1.163s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe6.043.443.004s1.404s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe6.613.443.023s1.478s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.932.422.123s0.988s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.872.442.167s1.033s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe5.532.862.554s1.118s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.642.792.512s1.202s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown66.2261.8961.536s59.936s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.8520.1819.799s17.730s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe37.8631.6231.227s28.288s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.012.602.327s1.075s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.397.357.049s5.504s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe30.0524.5624.148s21.920s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe7.023.673.314s1.959s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.4514.8114.431s12.187s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.293.503.203s1.742s
ssh/s3_clnt.blast.01.i.cil.csafe8.865.415.045s3.234s
ssh/s3_clnt.blast.03.i.cil.csafe13.379.469.131s6.285s
ssh/s3_clnt.blast.04.i.cil.csafe12.067.547.265s4.204s
ssh/s3_srvr.blast.01.i.cil.csafe32.5728.1027.721s23.382s
ssh/s3_srvr.blast.06.i.cil.csafe24.8218.9518.543s14.025s
ssh/s3_srvr.blast.07.i.cil.cunknown68.5264.6364.341s62.846s
ssh/s3_srvr.blast.08.i.cil.csafe25.6720.6820.245s16.484s
ssh/s3_srvr.blast.09.i.cil.cunknown64.5261.3861.057s59.106s
ssh/s3_srvr.blast.10.i.cil.csafe10.286.476.160s4.572s
ssh/s3_srvr.blast.12.i.cil.csafe12.298.347.995s6.399s
ssh/s3_srvr.blast.13.i.cil.cunknown65.1461.2460.953s59.335s
ssh/s3_srvr.blast.14.i.cil.csafe33.3928.9228.542s23.198s
ssh/s3_srvr.blast.15.i.cil.csafe13.819.899.534s5.024s
ssh/s3_srvr.blast.16.i.cil.csafe37.0932.8532.476s23.183s
locks/test_locks_14.BUG.cunsafe2.091.241.006s0.357s
locks/test_locks_15.BUG.cunsafe2.141.261.038s0.404s
locks/test_locks_10.csafe1.781.050.825s0.238s
locks/test_locks_11.csafe2.061.180.946s0.280s
locks/test_locks_12.csafe1.941.120.893s0.300s
locks/test_locks_13.csafe2.151.180.951s0.320s
locks/test_locks_14.csafe2.021.220.992s0.385s
locks/test_locks_15.csafe2.181.281.046s0.415s
locks/test_locks_5.csafe1.440.860.620s0.092s
locks/test_locks_6.csafe1.470.870.648s0.113s
locks/test_locks_7.csafe1.530.930.685s0.139s
locks/test_locks_8.csafe1.600.950.723s0.165s
locks/test_locks_9.csafe1.701.040.817s0.196s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.151.180.938s0.159s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.720.960.717s0.083s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.131.220.931s0.157s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.231.190.946s0.157s
heap-manipulation/dll_of_dll.cil.cunknown1.640.910.670s0.085s
heap-manipulation/merge_sort.cil.csafe1.600.910.682s0.070s
heap-manipulation/sll_to_dll_rev.cil.cunknown11.7410.2710.018s7.783s
list-properties/alternating_list.cil.csafe1.670.930.694s0.142s
list-properties/list.cil.csafe1.821.050.810s0.207s
list-properties/list_flag.cil.csafe1.821.030.772s0.158s
list-properties/simple.cil.cunsafe1.800.970.715s0.141s
list-properties/simple_built_from_end.cil.cunsafe1.861.180.946s0.185s
list-properties/splice.cil.cunsafe2.821.831.598s0.589s
systemc/token_ring.01.BUG.cil.cunsafe2.531.461.223s0.437s
systemc/token_ring.02.BUG.cil.cunsafe4.442.332.081s1.017s
systemc/token_ring.03.BUG.cil.cunsafe6.053.583.330s1.894s
systemc/transmitter.01.BUG.cil.cunsafe2.071.240.996s0.307s
systemc/transmitter.02.BUG.cil.cunsafe2.931.701.460s0.584s
systemc/transmitter.03.BUG.cil.cunsafe3.701.991.765s0.714s
systemc/transmitter.04.BUG.cil.cunsafe4.692.432.179s0.914s
systemc/bist_cell.cil.csafe17.5314.7114.447s12.634s
systemc/kundu.cil.csafe67.7061.0160.648s57.315s
systemc/mem_slave_tlm.1.cil.cexception32.8328.19--
systemc/mem_slave_tlm.2.cil.csafe67.9462.9262.558s60.443s
systemc/mem_slave_tlm.4.cil.ctimeout119.73113.77--
systemc/pc_sfifo_1.cil.csafe4.872.652.417s1.283s
systemc/pc_sfifo_2.cil.csafe9.245.194.941s3.037s
systemc/pc_sfifo_3.cil.csafe6.643.773.498s2.035s
systemc/token_ring.01.cil.csafe7.494.384.145s2.298s
systemc/token_ring.04.cil.csafe67.0660.8960.560s54.398s
systemc/toy.cil.csafe106.42100.45100.036s98.408s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.300.760.537s0.027s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.350.810.587s0.049s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.260.740.511s0.016s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.070.61--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.490.830.555s0.017s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.490.880.618s0.025s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.380.800.564s0.038s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.400.820.565s0.033s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.021.150.885s0.212s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.441.351.119s0.459s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.520.850.613s0.042s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.460.850.605s0.035s
ldv-regression/alias_of_return.c-safe.cil.csafe1.510.830.573s0.030s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.400.760.521s0.017s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.500.890.641s0.038s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.560.890.626s0.018s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.071.160.896s0.207s
ldv-regression/just_assert.c-safe.cil.csafe1.330.740.507s0.011s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.480.840.589s0.018s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.410.790.551s0.018s
ldv-regression/nested_structure-safe.cil.cunsafe1.480.830.590s0.042s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.450.830.562s0.020s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.390.760.528s0.016s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.470.790.544s0.019s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.590.910.679s0.090s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.390.800.564s0.023s
ldv-regression/oomInt.c-safe.cil.csafe1.380.800.561s0.030s
ldv-regression/oomInt.c-safe_1.cil.csafe1.490.840.598s0.032s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.580.900.624s0.048s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.440.830.591s0.023s
ldv-regression/rule60_list2.c-safe.cil.csafe2.031.200.964s0.227s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.480.820.580s0.023s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.460.790.541s0.016s
ldv-regression/test_address.c-safe.cil.cunsafe1.500.870.629s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.360.810.540s0.018s
ldv-regression/test_malloc-1-safe.cil.csafe1.540.870.626s0.029s
ldv-regression/test_malloc-2-safe.cil.csafe1.480.840.601s0.029s
ldv-regression/test_overflow.c-safe.cil.csafe1.400.770.544s0.029s
ldv-regression/test_union.c-safe.cil.csafe1.490.860.574s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.500.850.600s0.017s
ldv-regression/test_union_cast-1-safe.cil.csafe1.330.760.530s0.020s
ldv-regression/test_union_cast-2-safe.cil.csafe1.350.770.536s0.024s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.430.790.557s0.022s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.440.810.573s0.019s
ldv-regression/volatile_alias.c-safe.cil.csafe1.450.780.523s0.022s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.420.790.545s0.016s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.771.921.664s0.366s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.972.081.843s0.369s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.862.001.723s0.359s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.661.851.572s0.340s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.701.801.546s0.414s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.621.811.549s0.343s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.641.751.510s0.439s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.401.681.441s0.372s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.651.791.536s0.418s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.481.761.491s0.353s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.701.841.555s0.384s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.631.801.518s0.341s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.411.791.515s0.337s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe15.266.816.525s0.441s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe11.986.315.978s2.159s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.076.856.505s2.940s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe12.774.904.598s0.533s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe15.968.388.052s2.668s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe9.464.243.885s1.469s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe18.1910.279.927s4.327s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe8.183.262.980s0.212s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe24.419.148.860s1.335s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.807.076.772s3.167s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe43.6528.8828.443s10.655s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe7.863.603.256s0.692s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.9610.7010.374s3.595s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe6.493.102.811s0.854s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe17.848.978.561s5.861s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe17.617.677.369s1.243s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe34.3519.8819.395s11.411s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe13.106.566.215s4.017s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe14.197.366.960s4.125s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe20.759.919.551s1.261s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.712.241.916s0.619s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe7.313.483.181s1.389s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe19.559.549.142s5.710s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.942.382.085s0.717s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe15.747.407.030s4.487s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown87.8065.2364.743s61.435s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe22.2310.9610.554s6.797s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe10.145.114.811s2.356s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe6.523.132.831s1.051s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.643.673.364s1.397s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe5.182.592.224s0.742s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe18.898.077.668s3.313s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe5.142.582.227s0.608s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe24.0714.4214.051s5.158s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.372.071.770s0.210s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe13.966.495.532s2.633s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe7.103.343.019s1.096s