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.0902
Test setintegration-predicateAnalysis
branch-r5623
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2233526.742654.832253.2641857.944
correct results1611062.47695.94643.352369.321
false negatives00000
false positives1937.0220.4715.6062.457
score (223 files, max score: 361)212
pthread/fib_bench_BUG.cil.cunknown1.831.040.768s0.024s
pthread/fib_bench_longer_BUG.cil.cunknown1.921.170.788s0.031s
pthread/queue_BUG.cil.cunknown2.051.330.915s0.117s
pthread/reorder_5_BUG.cil.cunknown2.251.401.060s0.132s
pthread/twostage_3_BUG.cil.cunknown2.331.411.029s0.160s
pthread/fib_bench.cil.cunknown1.901.100.758s0.039s
pthread/fib_bench_longer.cil.cunknown1.741.090.711s0.032s
pthread/queue_ok.cil.cunknown1.871.070.773s0.079s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.113.923.578s2.114s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe4.012.271.945s0.826s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.442.622.286s1.105s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.211.681.373s0.510s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.503.182.833s1.840s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.282.642.251s1.317s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.602.051.717s0.864s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.422.402.110s1.144s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.751.411.042s0.343s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.211.601.292s0.519s
ntdrivers/cdaudio.BUG.i.cil.cunsafe10.415.515.151s2.752s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.253.683.365s1.813s
ntdrivers/floppy.BUG.i.cil.cunsafe11.476.706.345s3.992s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe4.502.462.129s0.863s
ntdrivers/parport.BUG.i.cil.cunknown87.4770.8062.171s60.532s
ntdrivers/cdaudio.i.cil.csafe9.695.294.942s3.116s
ntdrivers/diskperf.i.cil.csafe5.503.252.955s1.805s
ntdrivers/floppy.i.cil.csafe12.988.187.819s5.391s
ntdrivers/parport.i.cil.cunknown83.6967.4766.903s65.578s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.902.181.873s0.858s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.262.392.108s0.969s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe3.902.121.814s0.818s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.102.362.070s0.933s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.741.421.170s0.289s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe5.943.262.964s1.541s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.487.447.135s5.474s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe2.991.521.250s0.459s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.902.111.768s0.772s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.321.621.372s0.556s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.031.080.835s0.054s
ssh-simplified/s3_clnt_1.cil.csafe8.335.264.944s2.944s
ssh-simplified/s3_clnt_2.cil.csafe8.725.575.222s3.489s
ssh-simplified/s3_clnt_3.cil.csafe9.496.285.938s3.045s
ssh-simplified/s3_clnt_4.cil.csafe8.585.615.315s3.159s
ssh-simplified/s3_srvr_1a.cil.csafe3.641.971.637s1.050s
ssh-simplified/s3_srvr_1b.cil.csafe1.741.030.758s0.139s
ssh-simplified/s3_srvr_1.cil.csafe34.2029.8229.366s21.591s
ssh-simplified/s3_srvr_3.cil.csafe24.6420.3719.917s13.226s
ssh-simplified/s3_srvr_4.cil.csafe14.7610.6110.169s8.337s
ssh-simplified/s3_srvr_6.cil.csafe16.5112.2211.798s9.845s
ssh-simplified/s3_srvr_7.cil.csafe23.3918.9318.415s16.650s
ssh-simplified/s3_srvr_8.cil.csafe13.069.138.691s5.930s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe4.592.582.277s1.067s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.222.231.945s0.882s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.622.452.151s0.937s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe4.412.422.085s0.844s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.452.382.058s0.972s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe3.962.141.856s0.751s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe3.721.921.631s0.699s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe3.841.981.705s0.732s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe4.602.432.126s0.947s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe6.723.983.686s2.383s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe7.284.364.009s2.357s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe6.863.783.466s1.718s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.783.252.943s1.766s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.312.692.387s1.100s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.307.457.129s5.591s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe4.992.862.543s1.279s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.154.043.731s1.892s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.622.512.205s0.990s
ssh/s3_clnt.blast.01.i.cil.csafe9.606.265.929s4.039s
ssh/s3_clnt.blast.03.i.cil.csafe7.945.134.815s3.393s
ssh/s3_clnt.blast.04.i.cil.csafe11.567.797.423s5.326s
ssh/s3_srvr.blast.01.i.cil.csafe12.888.337.904s5.104s
ssh/s3_srvr.blast.06.i.cil.csafe15.4010.9810.484s8.693s
ssh/s3_srvr.blast.07.i.cil.csafe15.5510.9710.514s8.900s
ssh/s3_srvr.blast.08.i.cil.cout of memory90.6986.59--
ssh/s3_srvr.blast.09.i.cil.csafe12.188.137.684s5.550s
ssh/s3_srvr.blast.10.i.cil.csafe52.2847.3346.820s15.164s
ssh/s3_srvr.blast.12.i.cil.csafe38.8534.0133.487s15.015s
ssh/s3_srvr.blast.13.i.cil.csafe23.1418.2217.742s15.242s
ssh/s3_srvr.blast.14.i.cil.csafe32.7527.7627.175s20.620s
ssh/s3_srvr.blast.15.i.cil.csafe12.488.137.708s5.335s
ssh/s3_srvr.blast.16.i.cil.csafe16.6511.8711.384s8.022s
locks/test_locks_14.BUG.cunsafe1.660.960.712s0.110s
locks/test_locks_15.BUG.cunsafe1.720.960.705s0.106s
locks/test_locks_10.csafe1.620.860.620s0.080s
locks/test_locks_11.csafe1.680.900.649s0.082s
locks/test_locks_12.csafe1.640.870.632s0.089s
locks/test_locks_13.csafe1.660.890.644s0.097s
locks/test_locks_14.csafe1.670.890.652s0.103s
locks/test_locks_15.csafe1.730.930.678s0.110s
locks/test_locks_5.csafe1.630.920.659s0.046s
locks/test_locks_6.csafe1.690.910.663s0.051s
locks/test_locks_7.csafe1.620.870.613s0.052s
locks/test_locks_8.csafe1.810.970.732s0.062s
locks/test_locks_9.csafe1.640.890.640s0.066s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.591.451.196s0.188s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.901.040.796s0.080s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.271.160.914s0.162s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown63.9461.0160.706s57.596s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.261.190.905s0.160s
heap-manipulation/dll_of_dll.cil.cunknown1.851.030.789s0.099s
heap-manipulation/merge_sort.cil.csafe1.881.030.799s0.074s
heap-manipulation/sll_to_dll_rev.cil.cunknown65.9863.8463.558s57.468s
list-properties/alternating_list.cil.csafe1.811.060.808s0.165s
list-properties/list.cil.csafe2.041.150.846s0.204s
list-properties/list_flag.cil.csafe1.901.080.817s0.177s
list-properties/simple.cil.cunsafe1.791.020.780s0.148s
list-properties/simple_built_from_end.cil.cunsafe1.660.940.710s0.108s
list-properties/splice.cil.cunsafe2.941.811.561s0.739s
systemc/token_ring.01.BUG.cil.cunsafe2.891.541.265s0.545s
systemc/token_ring.02.BUG.cil.cunsafe4.922.502.201s1.344s
systemc/token_ring.03.BUG.cil.cunsafe7.583.753.391s2.399s
systemc/transmitter.01.BUG.cil.cunsafe2.121.180.919s0.266s
systemc/transmitter.02.BUG.cil.cunsafe2.881.551.292s0.589s
systemc/transmitter.03.BUG.cil.cunsafe4.792.312.010s1.204s
systemc/transmitter.04.BUG.cil.cunsafe8.624.564.209s3.106s
systemc/bist_cell.cil.csafe2.431.311.046s0.421s
systemc/kundu.cil.csafe17.2712.4511.936s10.369s
systemc/mem_slave_tlm.1.cil.cout of memory52.3347.03--
systemc/mem_slave_tlm.2.cil.cout of memory53.9248.56--
systemc/mem_slave_tlm.4.cil.cout of memory56.4451.37--
systemc/pc_sfifo_1.cil.csafe4.932.482.177s1.400s
systemc/pc_sfifo_2.cil.csafe5.993.172.884s1.880s
systemc/pc_sfifo_3.cil.csafe2.541.311.020s0.310s
systemc/token_ring.01.cil.csafe4.842.502.081s1.277s
systemc/token_ring.04.cil.cunknown72.8761.4860.692s54.659s
systemc/toy.cil.cout of memory67.7362.49--
ldv-regression/1_3.c-unsafe.cil.cunsafe1.610.900.570s0.022s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.540.850.627s0.039s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.420.760.526s0.012s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.090.62--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.490.780.532s0.015s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.450.760.533s0.015s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.440.820.592s0.031s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.480.840.613s0.028s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.670.920.677s0.089s
ldv-regression/stateful_check-unsafe.cil.cunsafe1.821.100.859s0.246s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.490.810.560s0.037s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.500.790.565s0.029s
ldv-regression/alias_of_return.c-safe.cil.csafe1.480.800.554s0.016s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.370.740.513s0.015s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.440.750.525s0.019s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.380.760.525s0.016s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.201.210.962s0.329s
ldv-regression/just_assert.c-safe.cil.csafe1.490.790.561s0.009s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.640.870.619s0.015s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.550.880.610s0.015s
ldv-regression/nested_structure-safe.cil.cunsafe1.540.860.608s0.041s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.480.790.536s0.018s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.430.760.532s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.380.780.545s0.015s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.790.990.756s0.113s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.740.960.684s0.021s
ldv-regression/oomInt.c-safe.cil.csafe1.740.910.633s0.023s
ldv-regression/oomInt.c-safe_1.cil.csafe1.530.860.611s0.021s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.711.050.799s0.063s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.681.020.732s0.032s
ldv-regression/rule60_list2.c-safe.cil.csafe1.861.000.734s0.092s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.700.920.669s0.016s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.720.940.678s0.022s
ldv-regression/test_address.c-safe.cil.cunsafe1.520.860.605s0.036s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.640.910.649s0.021s
ldv-regression/test_malloc-1-safe.cil.csafe1.700.930.669s0.033s
ldv-regression/test_malloc-2-safe.cil.csafe1.780.940.678s0.031s
ldv-regression/test_overflow.c-safe.cil.csafe1.820.980.714s0.033s
ldv-regression/test_union.c-safe.cil.csafe1.740.960.672s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.550.900.604s0.013s
ldv-regression/test_union_cast-1-safe.cil.csafe1.580.860.631s0.023s
ldv-regression/test_union_cast-2-safe.cil.csafe1.760.920.672s0.034s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.580.880.643s0.020s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.510.840.611s0.020s
ldv-regression/volatile_alias.c-safe.cil.csafe1.640.890.605s0.017s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.590.890.612s0.024s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.072.061.754s0.544s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.791.921.633s0.523s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.102.221.963s0.690s
ddv-machzwd/ddv_machzwd_inb.cil.csafe4.102.031.704s0.548s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.402.111.794s0.579s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.002.181.896s0.506s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.022.091.716s0.517s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.911.911.633s0.536s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.721.871.532s0.556s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.741.881.596s0.506s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.852.011.700s0.642s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.112.041.789s0.571s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.651.821.544s0.536s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.945.535.209s0.446s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe18.0110.159.736s5.955s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown84.6462.6062.117s60.196s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe13.365.074.794s0.640s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown76.5563.3562.857s39.333s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe16.998.598.204s5.749s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown83.9263.3362.825s60.302s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe8.823.583.257s0.221s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe17.808.548.252s1.491s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.0317.1814.399s8.039s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown81.8767.2066.679s57.047s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.342.962.658s0.590s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe46.5934.3433.758s24.171s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.332.422.115s0.891s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown89.9268.9163.298s61.306s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown86.1667.6067.068s62.732s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown82.4162.6561.890s60.675s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe8.965.234.800s3.070s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown5.102.592.255s0.929s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown91.5566.7666.201s60.041s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown5.142.472.141s0.891s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown82.3263.1762.689s60.601s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown83.5466.0262.994s60.947s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.241.541.281s0.282s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown83.3567.2563.620s62.028s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown84.0065.2463.821s60.854s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown80.9362.7862.295s60.047s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe7.444.293.992s2.562s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown81.5165.3861.696s60.557s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown82.5465.2261.722s60.193s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown85.0962.4661.939s60.766s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown90.7769.6764.564s61.806s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.441.681.430s0.376s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown98.8562.9862.447s56.379s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.231.621.384s0.188s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown85.4364.9664.391s61.871s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown85.8762.8962.380s60.039s