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.0841
Test setintegration-predicateAnalysis
branch-r5630
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2233580.512686.322325.5161922.228
correct results1611078.75699.44649.420375.213
false negatives00000
false positives1939.2021.9616.8852.666
score (223 files, max score: 361)212
pthread/fib_bench_BUG.cil.cunknown1.791.060.791s0.033s
pthread/fib_bench_longer_BUG.cil.cunknown1.891.210.877s0.037s
pthread/queue_BUG.cil.cunknown2.141.290.969s0.115s
pthread/reorder_5_BUG.cil.cunknown2.121.350.996s0.136s
pthread/twostage_3_BUG.cil.cunknown1.921.140.775s0.123s
pthread/fib_bench.cil.cunknown1.730.980.725s0.034s
pthread/fib_bench_longer.cil.cunknown1.540.880.629s0.029s
pthread/queue_ok.cil.cunknown1.901.010.752s0.085s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.364.023.712s2.229s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.962.291.978s0.841s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.572.712.391s0.998s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.441.801.507s0.583s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.553.272.949s1.882s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.292.622.344s1.583s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.722.051.688s0.788s
ntdrivers-simplified/floppy_simpl4.cil.csafe3.762.071.798s1.011s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.621.381.064s0.347s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.141.621.302s0.556s
ntdrivers/cdaudio.BUG.i.cil.cunsafe10.415.565.247s2.956s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.503.943.619s1.889s
ntdrivers/floppy.BUG.i.cil.cunsafe11.627.186.808s4.438s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe4.632.492.193s0.907s
ntdrivers/parport.BUG.i.cil.cunknown88.2970.8762.023s60.471s
ntdrivers/cdaudio.i.cil.csafe9.565.194.868s3.090s
ntdrivers/diskperf.i.cil.csafe5.683.383.053s1.876s
ntdrivers/floppy.i.cil.csafe26.4719.7719.346s14.629s
ntdrivers/parport.i.cil.cunknown86.0069.0562.900s61.345s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.621.941.654s0.715s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.312.412.123s0.987s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe4.082.171.897s0.839s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.392.482.193s1.029s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.611.391.101s0.306s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe6.253.363.072s1.656s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.667.567.247s5.510s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.101.611.342s0.493s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.832.031.752s0.764s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.441.841.561s0.650s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe1.971.040.793s0.046s
ssh-simplified/s3_clnt_1.cil.csafe8.055.204.898s2.993s
ssh-simplified/s3_clnt_2.cil.csafe8.295.324.983s3.306s
ssh-simplified/s3_clnt_3.cil.csafe9.366.115.819s3.061s
ssh-simplified/s3_clnt_4.cil.csafe9.205.865.506s3.250s
ssh-simplified/s3_srvr_1a.cil.csafe3.341.821.531s0.946s
ssh-simplified/s3_srvr_1b.cil.csafe1.690.910.650s0.126s
ssh-simplified/s3_srvr_1.cil.csafe33.9729.8729.432s22.104s
ssh-simplified/s3_srvr_3.cil.csafe24.9520.6520.166s13.591s
ssh-simplified/s3_srvr_4.cil.csafe14.6810.519.987s8.132s
ssh-simplified/s3_srvr_6.cil.csafe17.4813.0912.638s10.702s
ssh-simplified/s3_srvr_7.cil.csafe23.3118.7318.238s16.420s
ssh-simplified/s3_srvr_8.cil.csafe12.588.828.408s5.538s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe4.842.662.314s1.035s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.342.382.099s0.929s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.162.211.906s0.865s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe4.022.191.889s0.836s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe3.992.121.855s0.794s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe3.851.931.653s0.694s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe3.731.991.648s0.702s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe3.771.981.695s0.687s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe4.642.552.250s1.025s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.094.213.882s2.500s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe7.274.343.994s2.266s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe6.843.743.419s1.671s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.823.152.854s1.657s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.282.772.470s1.209s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.137.226.921s5.625s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe4.922.762.463s1.274s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.223.953.628s1.730s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.742.682.365s1.098s
ssh/s3_clnt.blast.01.i.cil.csafe9.946.636.292s4.242s
ssh/s3_clnt.blast.03.i.cil.csafe8.365.375.033s3.466s
ssh/s3_clnt.blast.04.i.cil.csafe11.097.557.135s5.072s
ssh/s3_srvr.blast.01.i.cil.csafe14.119.198.741s5.616s
ssh/s3_srvr.blast.06.i.cil.csafe15.3411.2010.712s8.746s
ssh/s3_srvr.blast.07.i.cil.csafe13.699.468.959s7.520s
ssh/s3_srvr.blast.08.i.cil.cout of memory91.3587.11--
ssh/s3_srvr.blast.09.i.cil.csafe12.248.377.919s5.764s
ssh/s3_srvr.blast.10.i.cil.csafe51.0546.4845.939s14.298s
ssh/s3_srvr.blast.12.i.cil.csafe40.4935.4234.873s15.926s
ssh/s3_srvr.blast.13.i.cil.csafe23.0918.3917.908s14.991s
ssh/s3_srvr.blast.14.i.cil.csafe33.1028.1227.610s21.286s
ssh/s3_srvr.blast.15.i.cil.csafe13.138.468.001s5.447s
ssh/s3_srvr.blast.16.i.cil.csafe15.7111.1410.664s7.057s
locks/test_locks_14.BUG.cunsafe1.880.990.729s0.106s
locks/test_locks_15.BUG.cunsafe1.821.060.812s0.120s
locks/test_locks_10.csafe1.600.920.666s0.082s
locks/test_locks_11.csafe1.660.930.699s0.091s
locks/test_locks_12.csafe1.821.010.754s0.100s
locks/test_locks_13.csafe1.881.010.735s0.103s
locks/test_locks_14.csafe1.781.020.764s0.110s
locks/test_locks_15.csafe1.710.930.683s0.120s
locks/test_locks_5.csafe1.780.970.695s0.046s
locks/test_locks_6.csafe1.720.940.680s0.064s
locks/test_locks_7.csafe1.801.000.744s0.076s
locks/test_locks_8.csafe1.730.910.634s0.058s
locks/test_locks_9.csafe1.700.980.734s0.071s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.261.301.061s0.214s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.951.130.891s0.111s
heap-manipulation/merge_sort_BUG.cil.cunsafe1.971.050.795s0.141s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown63.7561.0760.783s56.168s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.201.140.887s0.171s
heap-manipulation/dll_of_dll.cil.cunknown1.720.900.657s0.079s
heap-manipulation/merge_sort.cil.csafe1.670.880.656s0.069s
heap-manipulation/sll_to_dll_rev.cil.cunknown66.0263.9963.712s57.767s
list-properties/alternating_list.cil.csafe1.790.940.693s0.136s
list-properties/list.cil.csafe1.861.020.769s0.186s
list-properties/list_flag.cil.csafe1.800.970.735s0.158s
list-properties/simple.cil.cunsafe1.800.990.719s0.134s
list-properties/simple_built_from_end.cil.cunsafe1.590.970.734s0.151s
list-properties/splice.cil.cunsafe3.041.961.686s0.785s
systemc/token_ring.01.BUG.cil.cunsafe3.001.691.425s0.641s
systemc/token_ring.02.BUG.cil.cunsafe4.532.271.980s1.200s
systemc/token_ring.03.BUG.cil.cunsafe7.923.673.281s2.373s
systemc/transmitter.01.BUG.cil.cunsafe2.111.200.947s0.259s
systemc/transmitter.02.BUG.cil.cunsafe3.111.651.393s0.619s
systemc/transmitter.03.BUG.cil.cunsafe5.142.562.249s1.339s
systemc/transmitter.04.BUG.cil.cunsafe8.854.434.060s3.025s
systemc/bist_cell.cil.csafe2.401.281.001s0.368s
systemc/kundu.cil.csafe16.0112.1511.596s10.007s
systemc/mem_slave_tlm.1.cil.cout of memory55.8051.27--
systemc/mem_slave_tlm.2.cil.cout of memory56.0251.37--
systemc/mem_slave_tlm.4.cil.cout of memory66.4760.97--
systemc/pc_sfifo_1.cil.csafe4.602.482.177s1.409s
systemc/pc_sfifo_2.cil.csafe5.492.762.481s1.670s
systemc/pc_sfifo_3.cil.csafe2.151.200.935s0.328s
systemc/token_ring.01.cil.csafe4.342.081.760s1.049s
systemc/token_ring.04.cil.cunknown73.6061.5860.659s54.673s
systemc/toy.cil.cunknown66.5661.5261.148s58.178s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.680.940.682s0.024s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.660.950.704s0.045s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.620.890.647s0.013s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.100.66--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.650.970.700s0.015s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.590.900.646s0.020s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.731.010.726s0.038s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.660.940.687s0.029s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.761.000.741s0.093s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.001.160.902s0.236s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.630.910.664s0.038s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.530.880.618s0.032s
ldv-regression/alias_of_return.c-safe.cil.csafe1.560.900.615s0.024s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.590.850.603s0.015s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.600.870.619s0.024s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.530.900.647s0.016s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.571.521.155s0.355s
ldv-regression/just_assert.c-safe.cil.csafe1.580.880.580s0.010s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.771.030.708s0.020s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.660.940.705s0.016s
ldv-regression/nested_structure-safe.cil.cunsafe1.650.930.664s0.043s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.591.000.745s0.019s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.761.010.770s0.017s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.500.870.611s0.018s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.931.130.875s0.123s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.611.000.727s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.721.030.723s0.027s
ldv-regression/oomInt.c-safe_1.cil.csafe1.580.860.600s0.019s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.781.030.721s0.053s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.721.040.783s0.026s
ldv-regression/rule60_list2.c-safe.cil.csafe1.620.910.662s0.084s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.580.880.643s0.016s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.650.910.660s0.017s
ldv-regression/test_address.c-safe.cil.cunsafe1.610.880.624s0.023s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.520.820.549s0.024s
ldv-regression/test_malloc-1-safe.cil.csafe1.520.790.561s0.030s
ldv-regression/test_malloc-2-safe.cil.csafe1.420.810.572s0.031s
ldv-regression/test_overflow.c-safe.cil.csafe1.580.790.550s0.021s
ldv-regression/test_union.c-safe.cil.csafe1.540.800.542s0.014s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.520.790.546s0.015s
ldv-regression/test_union_cast-1-safe.cil.csafe1.390.800.560s0.017s
ldv-regression/test_union_cast-2-safe.cil.csafe1.520.800.552s0.025s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.540.820.584s0.020s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.510.780.546s0.016s
ldv-regression/volatile_alias.c-safe.cil.csafe1.690.850.591s0.018s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.500.830.593s0.026s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.362.241.962s0.650s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.042.081.801s0.518s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.132.151.894s0.645s
ddv-machzwd/ddv_machzwd_inb.cil.csafe4.142.031.754s0.587s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.881.941.639s0.474s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.162.031.724s0.497s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.282.051.768s0.481s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.021.991.683s0.504s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe4.131.961.670s0.482s
ddv-machzwd/ddv_machzwd_outl.cil.csafe4.131.971.698s0.568s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.232.061.772s0.598s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.062.041.731s0.559s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.142.011.728s0.584s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.015.645.341s0.442s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe16.739.469.103s5.681s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown87.5064.7664.241s62.153s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe13.705.254.975s0.675s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown77.3163.3962.951s39.424s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe17.639.048.591s6.243s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown80.3762.1761.722s59.150s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.993.162.898s0.221s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe19.477.076.766s0.399s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe14.669.449.027s6.217s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown80.0862.2761.770s57.223s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.142.892.610s0.592s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe42.2832.5731.968s22.560s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.522.502.231s0.943s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown86.8863.1462.615s60.182s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown92.9170.0266.745s62.469s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown80.4763.6762.911s61.785s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe9.615.705.347s3.435s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown5.402.612.313s0.957s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown92.4669.5168.937s62.184s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.592.281.973s0.807s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown82.1563.8763.375s61.417s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown90.2169.5764.077s61.391s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.441.651.373s0.356s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown88.2767.7364.462s62.740s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown85.8965.5465.000s62.386s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown84.1470.0865.868s61.218s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.245.024.688s3.094s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown83.5865.8861.652s60.181s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown85.6068.1262.033s60.224s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown83.1563.5963.057s61.746s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown89.8765.7765.255s61.880s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.052.001.736s0.476s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown93.0363.1662.674s56.738s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.921.881.626s0.197s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown86.5864.7664.187s61.368s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown88.4662.6262.106s57.342s