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.1331
Test setintegration-predicateAnalysis-abm
branch-r5654
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202360.011767.031205.531939.210
correct results1271296.54919.31879.905631.529
false negatives00000
false positives1019.8810.768.0180.606
score (220 files, max score: 356)178
pthread/fib_bench_BUG.cil.cunknown1.400.780.553s0.023s
pthread/fib_bench_longer_BUG.cil.cunknown1.560.840.611s0.024s
pthread/queue_BUG.cil.cexception1.640.93--
pthread/reorder_5_BUG.cil.cexception1.860.93--
pthread/twostage_3_BUG.cil.cexception1.770.94--
pthread/fib_bench.cil.cunknown1.590.840.585s0.026s
pthread/fib_bench_longer.cil.cunknown1.760.980.716s0.029s
pthread/queue_ok.cil.cexception1.500.83--
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe16.8910.7810.451s7.631s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe8.004.193.847s2.063s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe10.665.695.363s2.875s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.452.732.322s1.110s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.947.577.181s4.759s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.806.275.925s3.883s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.175.234.905s3.050s
ntdrivers-simplified/floppy_simpl4.cil.csafe12.206.716.354s4.078s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.991.721.394s0.495s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.722.442.105s0.951s
ntdrivers/cdaudio.BUG.i.cil.cunsafe14.927.737.340s4.231s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.465.935.550s2.838s
ntdrivers/floppy.BUG.i.cil.cexception8.294.01--
ntdrivers/kbfiltr.BUG.i.cil.cexception2.821.50--
ntdrivers/parport.BUG.i.cil.cexception7.383.41--
ntdrivers/cdaudio.i.cil.csafe18.0910.4710.098s6.219s
ntdrivers/diskperf.i.cil.csafe11.966.516.183s3.547s
ntdrivers/floppy.i.cil.cexception7.623.28--
ntdrivers/parport.i.cil.cexception6.653.04--
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.583.302.963s1.804s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.432.982.687s1.422s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.462.972.687s1.369s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.262.342.047s1.010s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe17.7113.3713.027s10.123s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe60.0753.6053.142s48.206s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.58115.43--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.0713.5513.161s10.421s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.162.251.967s0.880s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.662.572.286s1.168s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.091.070.830s0.054s
ssh-simplified/s3_clnt_1.cil.csafe10.106.816.525s4.463s
ssh-simplified/s3_clnt_2.cil.csafe8.435.194.849s2.933s
ssh-simplified/s3_clnt_3.cil.csafe7.694.263.985s2.446s
ssh-simplified/s3_clnt_4.cil.csafe11.678.047.770s4.906s
ssh-simplified/s3_srvr_1a.cil.csafe4.542.292.012s1.357s
ssh-simplified/s3_srvr_1b.cil.csafe2.001.080.825s0.241s
ssh-simplified/s3_srvr_1.cil.cout of memory66.7862.09--
ssh-simplified/s3_srvr_3.cil.csafe24.2819.2418.792s13.706s
ssh-simplified/s3_srvr_4.cil.csafe10.186.125.796s4.422s
ssh-simplified/s3_srvr_6.cil.ctimeout119.62115.74--
ssh-simplified/s3_srvr_7.cil.cunknown68.0464.9564.627s63.445s
ssh-simplified/s3_srvr_8.cil.csafe16.6912.2611.911s8.864s
ssh/s3_clnt.blast.01.BUG.i.cil.cexception1.981.06--
ssh/s3_clnt.blast.02.BUG.i.cil.cexception1.971.07--
ssh/s3_clnt.blast.03.BUG.i.cil.cexception1.991.06--
ssh/s3_clnt.blast.04.BUG.i.cil.cexception1.941.05--
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.362.562.291s1.156s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.562.462.202s1.061s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.652.522.225s1.126s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.562.272.016s0.906s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.773.052.786s1.288s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown68.7764.3163.971s62.505s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe24.7619.8819.440s17.350s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.7831.1030.668s27.769s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.972.592.325s1.087s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.347.176.866s5.342s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe29.6723.9323.512s21.305s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.833.463.175s1.815s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe18.7914.1413.759s11.636s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.183.533.275s1.761s
ssh/s3_clnt.blast.01.i.cil.cexception1.941.05--
ssh/s3_clnt.blast.03.i.cil.cexception1.941.06--
ssh/s3_clnt.blast.04.i.cil.cexception2.021.08--
ssh/s3_srvr.blast.01.i.cil.csafe31.6326.8126.451s22.481s
ssh/s3_srvr.blast.06.i.cil.csafe26.2720.7820.343s15.391s
ssh/s3_srvr.blast.07.i.cil.cunknown67.6263.8863.583s61.983s
ssh/s3_srvr.blast.08.i.cil.csafe27.3121.7621.316s17.405s
ssh/s3_srvr.blast.09.i.cil.cunknown66.5161.5361.064s58.894s
ssh/s3_srvr.blast.10.i.cil.csafe11.607.417.026s5.180s
ssh/s3_srvr.blast.12.i.cil.csafe14.309.519.065s7.042s
ssh/s3_srvr.blast.13.i.cil.cunknown66.3062.2261.898s60.146s
ssh/s3_srvr.blast.14.i.cil.csafe38.5232.6432.199s25.389s
ssh/s3_srvr.blast.15.i.cil.csafe17.1711.8811.476s5.964s
ssh/s3_srvr.blast.16.i.cil.csafe46.5741.2840.805s28.075s
locks/test_locks_14.BUG.cunsafe2.501.451.163s0.406s
locks/test_locks_15.BUG.cunsafe2.751.481.183s0.450s
locks/test_locks_11.csafe2.321.260.969s0.311s
locks/test_locks_12.csafe2.351.271.008s0.334s
locks/test_locks_13.csafe2.561.481.211s0.416s
locks/test_locks_14.csafe2.621.491.223s0.455s
locks/test_locks_15.csafe2.831.581.325s0.498s
locks/test_locks_5.csafe1.830.990.733s0.099s
locks/test_locks_6.csafe1.821.060.799s0.135s
locks/test_locks_7.csafe1.861.110.868s0.180s
locks/test_locks_8.csafe2.121.240.984s0.224s
locks/test_locks_9.csafe1.961.100.839s0.226s
heap-manipulation/bubble_sort_linux_BUG.cil.cexception2.011.07--
heap-manipulation/dll_of_dll_BUG.cil.cexception1.931.07--
heap-manipulation/merge_sort_BUG.cil.cexception1.901.00--
heap-manipulation/bubble_sort_linux.cil.cexception1.951.02--
heap-manipulation/dll_of_dll.cil.cexception1.961.03--
heap-manipulation/merge_sort.cil.cexception1.951.05--
heap-manipulation/sll_to_dll_rev.cil.cexception1.780.96--
list-properties/alternating_list.cil.cexception1.891.05--
list-properties/list.cil.cexception1.882.69--
list-properties/list_flag.cil.cexception1.822.73--
list-properties/simple.cil.cexception1.681.81--
list-properties/simple_built_from_end.cil.cexception1.783.47--
list-properties/splice.cil.cexception1.811.66--
systemc/token_ring.01.BUG.cil.cunsafe3.113.343.064s0.520s
systemc/token_ring.02.BUG.cil.cunsafe5.694.354.011s1.223s
systemc/token_ring.03.BUG.cil.cunsafe7.684.854.481s2.262s
systemc/transmitter.01.BUG.cil.cunsafe2.741.561.268s0.357s
systemc/transmitter.02.BUG.cil.cunsafe3.842.101.837s0.751s
systemc/transmitter.03.BUG.cil.cunsafe4.793.333.062s0.852s
systemc/transmitter.04.BUG.cil.cunsafe5.434.384.116s0.984s
systemc/bist_cell.cil.csafe18.4616.3816.083s12.990s
systemc/kundu.cil.csafe67.4562.2561.851s57.652s
systemc/mem_slave_tlm.1.cil.cexception45.9340.31--
systemc/mem_slave_tlm.2.cil.csafe71.2065.8365.492s63.111s
systemc/pc_sfifo_1.cil.csafe6.413.423.131s1.634s
systemc/pc_sfifo_2.cil.csafe10.066.165.838s3.700s
systemc/pc_sfifo_3.cil.csafe8.314.464.101s2.342s
systemc/token_ring.01.cil.csafe9.925.685.410s3.126s
systemc/token_ring.04.cil.csafe66.5661.0160.682s57.142s
systemc/toy.cil.cexception43.4536.86--
ldv-regression/1_3.c-unsafe.cil.cunsafe1.740.910.662s0.033s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.700.960.694s0.055s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.720.930.650s0.024s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.070.61--
ldv-regression/mutex_lock_int.c-unsafe.cil.cexception1.500.79--
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.670.880.626s0.020s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.660.940.664s0.043s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.670.940.706s0.041s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.281.250.973s0.232s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.511.431.187s0.492s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.640.900.622s0.045s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.570.920.658s0.037s
ldv-regression/alias_of_return.c-safe.cil.cexception1.690.95--
ldv-regression/alias_of_return.c-safe_1.cil.cexception1.660.94--
ldv-regression/alias_of_return_2.c-safe.cil.cexception1.861.01--
ldv-regression/alias_of_return_2.c-safe_1.cil.cexception1.640.88--
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.301.301.015s0.221s
ldv-regression/just_assert.c-safe.cil.csafe1.550.870.620s0.015s
ldv-regression/mutex_lock_int.c-safe_1.cil.cexception1.540.87--
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.660.940.670s0.018s
ldv-regression/nested_structure-safe.cil.cexception1.620.91--
ldv-regression/nested_structure.c-safe.cil.cunsafe1.540.840.600s0.021s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.450.820.546s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.550.870.623s0.021s
ldv-regression/nested_structure_ptr-safe.cil.cexception1.570.84--
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.710.940.687s0.027s
ldv-regression/oomInt.c-safe.cil.csafe1.740.940.670s0.035s
ldv-regression/oomInt.c-safe_1.cil.csafe1.771.000.709s0.038s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.821.050.760s0.048s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.590.870.585s0.022s
ldv-regression/rule60_list2.c-safe.cil.csafe2.241.311.033s0.259s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.660.910.654s0.031s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.740.930.653s0.022s
ldv-regression/test_address.c-safe.cil.cunsafe1.750.930.661s0.023s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.821.050.730s0.027s
ldv-regression/test_malloc-1-safe.cil.csafe1.630.920.637s0.046s
ldv-regression/test_malloc-2-safe.cil.csafe1.691.030.721s0.032s
ldv-regression/test_overflow.c-safe.cil.csafe1.721.030.674s0.035s
ldv-regression/test_union.c-safe.cil.csafe1.851.000.690s0.022s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.820.970.707s0.017s
ldv-regression/test_union_cast-1-safe.cil.csafe1.610.900.612s0.020s
ldv-regression/test_union_cast-2-safe.cil.cexception1.821.00--
ldv-regression/test_union_cast.c-safe.cil.cexception1.480.84--
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.480.840.595s0.019s
ldv-regression/volatile_alias.c-safe.cil.cexception1.640.93--
ldv-regression/volatile_alias.c-safe_1.cil.cexception1.520.78--
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.342.292.020s0.412s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.102.121.836s0.403s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.962.071.815s0.401s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.951.911.621s0.427s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.112.051.787s0.516s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.052.021.708s0.423s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.821.951.639s0.395s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.002.001.676s0.419s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.821.981.723s0.518s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.771.881.624s0.437s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.641.751.501s0.427s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.741.941.601s0.381s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.881.871.602s0.445s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe16.517.096.783s0.506s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cexception5.212.46--
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cexception7.212.92--
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cexception14.765.49--
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cexception10.413.96--
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cexception7.183.02--
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cexception9.083.82--
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe9.043.723.439s0.270s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe17.107.106.788s1.449s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.566.696.380s3.099s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe42.3726.5626.185s11.268s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cexception5.562.59--
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cexception8.534.03--
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cexception3.771.89--
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cexception6.282.51--
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cexception14.356.02--
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cexception4.562.08--
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.125.415.099s3.138s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cexception5.012.54--
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cexception15.057.05--
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cexception3.571.71--
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cexception5.642.56--
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cexception7.403.28--
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.592.221.955s0.671s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cexception6.342.51--
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cexception14.155.03--
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cexception8.953.70--
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe8.934.534.241s1.995s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cexception4.752.22--
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe9.144.013.693s1.458s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cexception4.061.92--
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cexception12.184.59--
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cexception3.961.88--
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cexception5.232.52--
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.951.991.680s0.187s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cexception8.533.44--
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cexception4.702.20--