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.1332
Test setintegration-predicateAnalysis
branch-r5654
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2211829.351273.15845.324595.385
correct results130855.08561.98520.612301.037
false negatives00000
false positives1019.4310.427.7110.676
score (221 files, max score: 357)183
pthread/fib_bench_BUG.cil.cunknown1.771.160.835s0.023s
pthread/fib_bench_longer_BUG.cil.cunknown1.981.270.887s0.039s
pthread/queue_BUG.cil.cexception2.081.32--
pthread/reorder_5_BUG.cil.cexception2.081.35--
pthread/twostage_3_BUG.cil.cexception2.241.58--
pthread/fib_bench.cil.cunknown2.061.451.054s0.038s
pthread/fib_bench_longer.cil.cunknown1.881.200.850s0.029s
pthread/queue_ok.cil.cexception1.901.09--
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.063.713.366s1.961s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.962.281.974s0.831s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.302.462.172s0.980s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.401.701.423s0.563s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.573.342.970s1.977s
ntdrivers-simplified/diskperf_simpl1.cil.csafe3.932.412.142s1.399s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.502.001.703s0.867s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.272.341.957s0.982s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.591.321.019s0.336s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe2.991.491.212s0.512s
ntdrivers/cdaudio.BUG.i.cil.cunsafe10.595.865.499s3.050s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.373.913.555s1.894s
ntdrivers/floppy.BUG.i.cil.cexception5.703.09--
ntdrivers/kbfiltr.BUG.i.cil.cexception2.601.46--
ntdrivers/parport.BUG.i.cil.cexception4.972.41--
ntdrivers/cdaudio.i.cil.csafe9.985.395.069s3.018s
ntdrivers/diskperf.i.cil.csafe5.803.423.103s1.925s
ntdrivers/floppy.i.cil.cexception5.202.60--
ntdrivers/parport.i.cil.cexception5.232.56--
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.782.041.693s0.701s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.562.612.285s1.092s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe4.022.231.956s0.860s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.202.512.205s1.037s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.571.391.069s0.264s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe6.273.413.108s1.617s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.757.727.300s5.558s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.231.631.351s0.464s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.801.981.693s0.777s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.641.901.604s0.633s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.161.130.872s0.054s
ssh-simplified/s3_clnt_1.cil.csafe8.705.705.371s3.284s
ssh-simplified/s3_clnt_2.cil.csafe8.515.565.204s3.432s
ssh-simplified/s3_clnt_3.cil.csafe9.125.945.635s2.902s
ssh-simplified/s3_clnt_4.cil.csafe9.206.155.851s3.627s
ssh-simplified/s3_srvr_1a.cil.csafe3.501.931.598s1.003s
ssh-simplified/s3_srvr_1b.cil.csafe1.690.930.695s0.131s
ssh-simplified/s3_srvr_1.cil.csafe35.3730.9230.463s22.895s
ssh-simplified/s3_srvr_3.cil.csafe25.1621.0520.515s13.580s
ssh-simplified/s3_srvr_4.cil.csafe15.0410.8310.401s8.420s
ssh-simplified/s3_srvr_6.cil.csafe17.0912.4711.973s9.971s
ssh-simplified/s3_srvr_7.cil.csafe22.7318.3717.914s16.040s
ssh-simplified/s3_srvr_8.cil.csafe12.418.648.208s5.554s
ssh/s3_clnt.blast.01.BUG.i.cil.cexception1.880.99--
ssh/s3_clnt.blast.02.BUG.i.cil.cexception2.021.09--
ssh/s3_clnt.blast.03.BUG.i.cil.cexception1.870.99--
ssh/s3_clnt.blast.04.BUG.i.cil.cexception2.061.16--
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.282.231.954s0.833s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe3.661.931.606s0.687s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.032.091.794s0.810s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe3.852.011.721s0.758s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe4.792.482.205s0.915s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.564.414.091s2.658s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe7.364.384.039s2.288s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.344.083.761s1.937s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.793.232.925s1.651s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.322.852.564s1.191s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.517.547.248s5.810s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.333.162.872s1.490s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.224.093.758s1.914s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.662.562.270s1.059s
ssh/s3_clnt.blast.01.i.cil.cexception1.921.07--
ssh/s3_clnt.blast.03.i.cil.cexception1.931.12--
ssh/s3_clnt.blast.04.i.cil.cexception1.991.12--
ssh/s3_srvr.blast.01.i.cil.csafe12.998.598.126s5.330s
ssh/s3_srvr.blast.06.i.cil.csafe15.9811.3910.401s8.664s
ssh/s3_srvr.blast.07.i.cil.csafe15.0810.319.813s8.196s
ssh/s3_srvr.blast.08.i.cil.cout of memory89.4385.03--
ssh/s3_srvr.blast.09.i.cil.csafe12.888.498.050s5.690s
ssh/s3_srvr.blast.10.i.cil.csafe52.1247.8747.354s15.127s
ssh/s3_srvr.blast.12.i.cil.csafe39.7134.4733.981s15.910s
ssh/s3_srvr.blast.13.i.cil.csafe21.2116.5516.110s13.843s
ssh/s3_srvr.blast.14.i.cil.csafe32.1127.4726.969s20.840s
ssh/s3_srvr.blast.15.i.cil.csafe12.528.277.813s5.360s
ssh/s3_srvr.blast.16.i.cil.csafe16.1211.4610.897s7.448s
locks/test_locks_14.BUG.cunsafe1.780.980.709s0.105s
locks/test_locks_15.BUG.cunsafe1.811.050.778s0.108s
locks/test_locks_11.csafe1.680.880.644s0.087s
locks/test_locks_12.csafe1.650.930.694s0.098s
locks/test_locks_13.csafe1.680.890.651s0.101s
locks/test_locks_14.csafe1.721.000.732s0.116s
locks/test_locks_15.csafe1.660.910.659s0.121s
locks/test_locks_5.csafe1.700.860.591s0.042s
locks/test_locks_6.csafe1.560.820.581s0.048s
locks/test_locks_7.csafe1.650.890.637s0.075s
locks/test_locks_8.csafe1.630.860.610s0.064s
locks/test_locks_9.csafe1.660.910.652s0.076s
heap-manipulation/bubble_sort_linux_BUG.cil.cexception1.901.00--
heap-manipulation/dll_of_dll_BUG.cil.cexception1.620.86--
heap-manipulation/merge_sort_BUG.cil.cexception1.640.85--
heap-manipulation/sll_to_dll_rev_BUG.cil.cexception1.670.86--
heap-manipulation/bubble_sort_linux.cil.cexception1.870.99--
heap-manipulation/dll_of_dll.cil.cexception1.640.86--
heap-manipulation/merge_sort.cil.cexception1.620.86--
heap-manipulation/sll_to_dll_rev.cil.cexception1.530.89--
list-properties/alternating_list.cil.cexception1.520.81--
list-properties/list.cil.cexception1.490.84--
list-properties/list_flag.cil.cexception1.620.82--
list-properties/simple.cil.cexception1.580.89--
list-properties/simple_built_from_end.cil.cexception1.580.80--
list-properties/splice.cil.cexception1.610.83--
systemc/token_ring.01.BUG.cil.cunsafe2.771.531.269s0.540s
systemc/token_ring.02.BUG.cil.cunsafe4.732.372.074s1.251s
systemc/token_ring.03.BUG.cil.cunsafe8.104.093.723s2.730s
systemc/transmitter.01.BUG.cil.cunsafe2.061.220.920s0.240s
systemc/transmitter.02.BUG.cil.cunsafe2.991.511.251s0.554s
systemc/transmitter.03.BUG.cil.cunsafe4.662.251.942s1.138s
systemc/transmitter.04.BUG.cil.cunsafe8.814.564.223s3.159s
systemc/bist_cell.cil.csafe2.501.301.027s0.370s
systemc/kundu.cil.csafe16.6212.1311.565s10.093s
systemc/mem_slave_tlm.1.cil.cout of memory52.9248.24--
systemc/mem_slave_tlm.2.cil.csegmentation fault60.9856.27--
systemc/pc_sfifo_1.cil.csafe4.992.412.044s1.269s
systemc/pc_sfifo_2.cil.csafe5.442.772.482s1.638s
systemc/pc_sfifo_3.cil.csafe2.291.230.957s0.290s
systemc/token_ring.01.cil.csafe4.862.382.032s1.266s
systemc/token_ring.04.cil.csegmentation fault67.7956.89--
systemc/toy.cil.cunknown67.2061.9861.553s58.626s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.600.840.586s0.022s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.540.900.664s0.039s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.460.820.585s0.017s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.070.61--
ldv-regression/mutex_lock_int.c-unsafe.cil.cexception1.420.75--
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.500.780.550s0.016s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.770.940.687s0.040s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.550.860.620s0.030s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.881.080.777s0.087s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.101.270.981s0.235s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.680.930.689s0.044s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.610.930.682s0.047s
ldv-regression/alias_of_return.c-safe.cil.cexception1.470.78--
ldv-regression/alias_of_return.c-safe_1.cil.cexception1.600.88--
ldv-regression/alias_of_return_2.c-safe.cil.cexception1.440.81--
ldv-regression/alias_of_return_2.c-safe_1.cil.cexception1.670.89--
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.401.301.037s0.297s
ldv-regression/just_assert.c-safe.cil.csafe1.740.930.664s0.015s
ldv-regression/mutex_lock_int.c-safe_1.cil.cexception1.690.95--
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.530.970.672s0.015s
ldv-regression/nested_structure-safe.cil.cexception1.550.86--
ldv-regression/nested_structure.c-safe.cil.cunsafe1.690.900.629s0.027s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.520.850.592s0.022s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.610.850.589s0.017s
ldv-regression/nested_structure_ptr-safe.cil.cexception1.490.80--
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.580.900.635s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.660.860.610s0.018s
ldv-regression/oomInt.c-safe_1.cil.csafe1.620.850.601s0.016s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.710.940.649s0.041s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.700.880.629s0.021s
ldv-regression/rule60_list2.c-safe.cil.csafe1.671.000.696s0.088s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.610.830.565s0.016s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.510.880.580s0.020s
ldv-regression/test_address.c-safe.cil.cunsafe1.650.900.639s0.018s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.650.870.624s0.018s
ldv-regression/test_malloc-1-safe.cil.csafe1.620.880.597s0.029s
ldv-regression/test_malloc-2-safe.cil.csafe1.480.870.588s0.033s
ldv-regression/test_overflow.c-safe.cil.csafe1.740.900.655s0.026s
ldv-regression/test_union.c-safe.cil.csafe1.640.880.638s0.015s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.680.830.580s0.015s
ldv-regression/test_union_cast-1-safe.cil.csafe1.500.780.552s0.016s
ldv-regression/test_union_cast-2-safe.cil.cexception1.610.84--
ldv-regression/test_union_cast.c-safe.cil.cexception1.620.84--
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.580.850.610s0.015s
ldv-regression/volatile_alias.c-safe.cil.cexception1.670.89--
ldv-regression/volatile_alias.c-safe_1.cil.cexception1.550.81--
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.302.211.946s0.648s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.881.991.734s0.583s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.132.051.767s0.568s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.961.881.614s0.577s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.651.751.497s0.499s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.781.841.553s0.472s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.121.991.735s0.546s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.001.951.675s0.508s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.811.781.499s0.465s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.831.851.549s0.472s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.102.021.713s0.564s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.901.821.542s0.467s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.871.991.682s0.541s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.345.485.194s0.462s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cexception4.792.37--
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cexception6.952.89--
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cexception14.965.64--
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cexception9.013.60--
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cexception6.682.73--
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown83.7062.3561.911s59.378s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe8.673.182.911s0.263s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe14.425.565.264s0.506s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe13.018.297.815s5.378s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown85.4362.4761.904s53.280s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cexception5.732.45--
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cexception9.024.52--
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cexception3.661.79--
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cexception6.002.52--
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cexception13.655.21--
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cexception10.164.85--
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe8.575.064.754s3.139s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cexception4.872.16--
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cexception15.046.32--
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cexception3.501.80--
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cexception6.232.40--
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cexception8.013.41--
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.151.511.245s0.280s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cexception5.982.54--
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cexception9.243.54--
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cexception8.573.38--
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.034.924.624s2.999s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown81.5163.3762.541s61.070s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown81.1370.7065.466s61.189s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cexception4.542.26--
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cexception11.404.35--
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cexception4.142.02--
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cexception4.902.46--
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.981.921.661s0.200s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cexception7.353.25--
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cexception4.272.04--