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-16.1721
Test setintegration-predicateAnalysis-abm
branch-r5628
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2222769.652058.431660.7331266.106
correct results1801922.191302.191247.965887.524
false negatives00000
false positives1936.7120.7916.0002.490
score (222 files, max score: 360)247
pthread/fib_bench_BUG.cil.cunknown1.280.750.506s0.026s
pthread/fib_bench_longer_BUG.cil.cunknown1.320.770.520s0.032s
pthread/queue_BUG.cil.cunknown1.530.900.655s0.083s
pthread/reorder_5_BUG.cil.cunknown1.781.000.764s0.109s
pthread/twostage_3_BUG.cil.cunknown1.921.100.852s0.126s
pthread/fib_bench.cil.cunknown1.450.850.581s0.032s
pthread/fib_bench_longer.cil.cunknown1.390.850.619s0.028s
pthread/queue_ok.cil.cunknown1.600.920.690s0.082s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe17.1910.9910.601s7.596s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.563.673.251s1.677s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe8.664.314.012s2.236s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.952.852.512s1.195s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.828.137.744s5.107s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.375.855.477s3.602s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.255.304.988s3.090s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.736.406.040s3.930s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.161.781.502s0.556s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.402.271.925s0.878s
ntdrivers/cdaudio.BUG.i.cil.cunsafe15.137.917.561s4.242s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.205.995.639s2.955s
ntdrivers/floppy.BUG.i.cil.cunsafe12.766.756.369s2.965s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.473.743.409s1.384s
ntdrivers/parport.BUG.i.cil.cunsafe20.5212.0511.581s5.756s
ntdrivers/cdaudio.i.cil.csafe16.889.819.449s5.959s
ntdrivers/diskperf.i.cil.csafe12.426.205.886s3.421s
ntdrivers/floppy.i.cil.csafe14.838.678.346s4.260s
ntdrivers/parport.i.cil.csafe28.5919.1118.689s11.783s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.533.293.012s1.867s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.052.862.571s1.420s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.943.092.828s1.485s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.442.542.270s1.095s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.4314.0613.659s10.585s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe63.0556.8156.254s50.445s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.61115.48--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe17.3712.8212.482s9.851s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.892.161.872s0.904s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.742.442.177s1.141s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.241.150.884s0.051s
ssh-simplified/s3_clnt_1.cil.csafe10.927.176.896s4.839s
ssh-simplified/s3_clnt_2.cil.csafe9.535.625.335s3.387s
ssh-simplified/s3_clnt_3.cil.csafe7.894.524.237s2.690s
ssh-simplified/s3_clnt_4.cil.csafe11.628.237.891s5.009s
ssh-simplified/s3_srvr_1a.cil.csafe4.282.251.940s1.283s
ssh-simplified/s3_srvr_1b.cil.csafe1.961.050.797s0.214s
ssh-simplified/s3_srvr_1.cil.cout of memory65.4360.35--
ssh-simplified/s3_srvr_3.cil.csafe25.0919.5219.092s13.893s
ssh-simplified/s3_srvr_4.cil.csafe10.896.456.140s4.608s
ssh-simplified/s3_srvr_6.cil.ctimeout119.65115.07--
ssh-simplified/s3_srvr_7.cil.cunknown65.7862.5862.264s61.002s
ssh-simplified/s3_srvr_8.cil.csafe15.5410.9710.647s7.876s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.363.022.746s1.431s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.942.612.345s1.154s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.402.332.072s0.957s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.932.762.480s1.282s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe6.122.912.660s1.359s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.662.502.238s1.069s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.982.612.355s1.235s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.742.492.209s1.062s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.522.742.449s1.174s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown68.4064.3263.996s62.550s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.6920.3119.899s17.870s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.6630.2529.843s27.038s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.822.392.131s1.042s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.267.497.180s5.557s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe28.4723.0322.635s20.529s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.663.493.214s1.900s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe18.4413.5713.233s11.260s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.603.042.776s1.530s
ssh/s3_clnt.blast.01.i.cil.csafe8.254.844.570s3.052s
ssh/s3_clnt.blast.03.i.cil.csafe13.129.058.779s6.178s
ssh/s3_clnt.blast.04.i.cil.csafe10.956.816.536s3.783s
ssh/s3_srvr.blast.01.i.cil.csafe31.9627.4527.095s22.785s
ssh/s3_srvr.blast.06.i.cil.csafe25.4420.0819.659s14.479s
ssh/s3_srvr.blast.07.i.cil.cunknown67.5063.6563.363s61.901s
ssh/s3_srvr.blast.08.i.cil.csafe23.5318.4618.040s14.439s
ssh/s3_srvr.blast.09.i.cil.cunknown65.9461.5061.128s59.270s
ssh/s3_srvr.blast.10.i.cil.csafe11.617.196.841s4.940s
ssh/s3_srvr.blast.12.i.cil.csafe15.2610.259.848s7.950s
ssh/s3_srvr.blast.13.i.cil.cunknown68.1263.5163.141s61.126s
ssh/s3_srvr.blast.14.i.cil.csafe35.4530.2529.848s24.405s
ssh/s3_srvr.blast.15.i.cil.csafe16.0511.0410.675s5.704s
ssh/s3_srvr.blast.16.i.cil.csafe43.9937.9737.550s27.331s
locks/test_locks_14.BUG.cunsafe2.371.321.074s0.394s
locks/test_locks_15.BUG.cunsafe2.791.551.292s0.504s
locks/test_locks_10.csafe2.121.200.948s0.258s
locks/test_locks_11.csafe2.361.301.056s0.317s
locks/test_locks_12.csafe2.441.431.150s0.354s
locks/test_locks_13.csafe2.611.551.252s0.404s
locks/test_locks_14.csafe2.671.691.428s0.474s
locks/test_locks_15.csafe2.801.601.323s0.527s
locks/test_locks_5.csafe1.991.210.844s0.109s
locks/test_locks_6.csafe1.981.110.842s0.149s
locks/test_locks_7.csafe2.031.220.953s0.242s
locks/test_locks_8.csafe1.951.140.907s0.193s
locks/test_locks_9.csafe2.101.250.979s0.253s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.581.421.147s0.202s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.071.110.848s0.101s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.391.321.078s0.217s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.541.481.222s0.203s
heap-manipulation/dll_of_dll.cil.cunknown2.041.300.859s0.151s
heap-manipulation/merge_sort.cil.csafe2.211.190.857s0.085s
heap-manipulation/sll_to_dll_rev.cil.cunknown14.4012.3912.132s9.397s
list-properties/alternating_list.cil.csafe2.051.050.792s0.152s
list-properties/list.cil.csafe2.281.260.969s0.239s
list-properties/list_flag.cil.csafe2.161.160.907s0.199s
list-properties/simple.cil.cunsafe2.081.150.874s0.173s
list-properties/simple_built_from_end.cil.cunsafe2.081.200.913s0.156s
list-properties/splice.cil.cunsafe3.682.261.989s0.740s
systemc/token_ring.01.BUG.cil.cunsafe3.031.731.448s0.541s
systemc/token_ring.02.BUG.cil.cunsafe6.413.122.792s1.386s
systemc/token_ring.03.BUG.cil.cunsafe7.784.193.904s2.182s
systemc/transmitter.01.BUG.cil.cunsafe2.721.731.423s0.420s
systemc/transmitter.02.BUG.cil.cunsafe3.782.091.794s0.717s
systemc/transmitter.03.BUG.cil.cunsafe4.672.462.197s0.920s
systemc/transmitter.04.BUG.cil.cunsafe5.922.962.649s1.170s
systemc/bist_cell.cil.csafe21.0417.1516.878s14.780s
systemc/kundu.cil.csafe68.2461.0960.665s57.154s
systemc/mem_slave_tlm.1.cil.cexception44.8239.58--
systemc/mem_slave_tlm.2.cil.csafe73.1968.1367.742s65.466s
systemc/mem_slave_tlm.4.cil.csafe89.7583.7683.379s81.190s
systemc/pc_sfifo_1.cil.csafe5.092.792.549s1.366s
systemc/pc_sfifo_2.cil.csafe7.984.924.642s2.902s
systemc/pc_sfifo_3.cil.csafe6.873.833.535s2.093s
systemc/token_ring.01.cil.csafe8.384.874.623s2.626s
systemc/token_ring.04.cil.csafe66.7361.0060.682s57.429s
systemc/toy.cil.csafe70.4364.2563.919s61.899s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.320.790.554s0.028s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.460.880.647s0.058s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.300.750.520s0.016s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.060.61--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.360.780.533s0.018s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.440.820.582s0.017s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.360.790.564s0.038s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.440.860.628s0.035s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.041.170.913s0.212s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.151.291.058s0.428s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.420.850.587s0.043s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.360.800.558s0.036s
ldv-regression/alias_of_return.c-safe.cil.csafe1.340.790.544s0.032s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.370.790.534s0.019s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.350.790.555s0.036s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.450.840.596s0.026s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe1.871.120.857s0.206s
ldv-regression/just_assert.c-safe.cil.csafe1.360.740.506s0.010s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.360.800.553s0.019s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.340.790.533s0.017s
ldv-regression/nested_structure-safe.cil.cunsafe1.400.820.586s0.042s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.410.810.571s0.023s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.320.760.514s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.370.770.533s0.019s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.590.940.700s0.096s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.340.780.540s0.024s
ldv-regression/oomInt.c-safe.cil.csafe1.340.770.543s0.031s
ldv-regression/oomInt.c-safe_1.cil.csafe1.460.820.587s0.035s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.490.890.651s0.053s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.340.790.551s0.024s
ldv-regression/rule60_list2.c-safe.cil.csafe1.871.130.896s0.222s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.320.760.534s0.025s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.330.770.530s0.018s
ldv-regression/test_address.c-safe.cil.cunsafe1.380.810.549s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.320.770.539s0.020s
ldv-regression/test_malloc-1-safe.cil.csafe1.340.770.537s0.029s
ldv-regression/test_malloc-2-safe.cil.csafe1.390.800.547s0.026s
ldv-regression/test_overflow.c-safe.cil.csafe1.340.780.546s0.033s
ldv-regression/test_union.c-safe.cil.csafe1.320.760.528s0.017s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.380.800.546s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.370.770.535s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.350.770.533s0.024s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.400.810.565s0.021s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.320.760.530s0.017s
ldv-regression/volatile_alias.c-safe.cil.csafe1.320.750.516s0.017s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.390.790.547s0.016s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.431.891.639s0.354s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.591.931.660s0.373s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.972.171.917s0.400s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.521.781.530s0.374s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.551.831.570s0.452s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.651.831.575s0.396s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.381.721.456s0.391s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.571.961.657s0.432s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.331.711.449s0.397s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.561.871.580s0.432s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.791.981.650s0.452s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.351.731.469s0.366s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.461.791.533s0.410s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.526.035.755s0.459s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe10.775.545.230s1.909s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.936.385.976s2.531s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe12.694.774.483s0.554s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe16.788.868.546s3.313s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe8.623.873.579s1.334s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe17.9810.149.803s4.162s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe8.063.403.153s0.232s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe20.007.877.584s1.508s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe11.556.356.070s2.924s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe41.8725.9325.586s10.518s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.363.002.739s0.583s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe16.8310.129.793s3.867s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.242.542.259s0.750s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe16.367.947.560s5.335s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe14.266.536.222s1.081s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe35.0319.0518.648s12.652s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.285.675.302s3.206s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe11.846.275.867s3.438s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe18.168.347.964s0.942s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown3.971.971.721s0.697s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe6.383.202.918s1.212s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe17.528.257.910s5.120s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.242.171.919s0.672s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe13.246.285.906s3.652s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown89.6964.8962.129s59.379s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe19.338.848.381s5.455s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.534.924.578s2.219s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.622.762.422s0.951s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.803.913.575s1.653s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.512.422.114s0.636s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe17.397.437.031s3.142s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.342.081.836s0.472s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe17.419.799.456s3.615s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.361.691.434s0.166s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe11.395.455.111s2.882s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe5.852.772.506s0.932s