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-22.1231
Test setintegration-predicateAnalysis
branch-r5690
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2213506.552551.222292.4881903.278
correct results1611055.40683.67633.800370.997
false negatives00000
false positives1937.4320.3715.5012.708
score (221 files, max score: 357)211
pthread/fib_bench_BUG.cil.cunknown1.841.090.803s0.024s
pthread/fib_bench_longer_BUG.cil.cunknown1.821.120.784s0.032s
pthread/queue_BUG.cil.cunknown2.221.300.971s0.129s
pthread/reorder_5_BUG.cil.cunknown2.301.310.949s0.140s
pthread/twostage_3_BUG.cil.cunknown2.021.170.795s0.133s
pthread/fib_bench.cil.cunknown1.680.910.676s0.023s
pthread/fib_bench_longer.cil.cunknown1.620.950.620s0.031s
pthread/queue_ok.cil.cunknown2.051.190.905s0.108s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.704.354.030s2.597s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.942.261.978s0.865s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.562.592.264s1.067s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.301.751.462s0.570s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.853.613.265s2.256s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.402.682.389s1.572s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.672.111.787s0.985s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.162.241.953s1.034s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.511.331.058s0.389s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.201.631.305s0.494s
ntdrivers/cdaudio.BUG.i.cil.cunsafe10.646.055.648s3.076s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.113.713.423s1.860s
ntdrivers/floppy.BUG.i.cil.cunsafe11.216.746.346s4.171s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe5.032.792.387s1.008s
ntdrivers/parport.BUG.i.cil.cunknown87.4066.3462.446s60.875s
ntdrivers/cdaudio.i.cil.csafe8.954.854.494s2.682s
ntdrivers/diskperf.i.cil.csafe5.343.222.951s1.873s
ntdrivers/floppy.i.cil.csafe11.787.357.002s4.970s
ntdrivers/parport.i.cil.cunknown84.0266.8063.607s62.121s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.531.901.618s0.717s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe3.972.231.942s0.882s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe3.812.071.799s0.782s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.042.362.067s0.950s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.451.261.017s0.254s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe5.723.022.709s1.374s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.967.727.439s5.746s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.141.581.293s0.478s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.761.941.653s0.711s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.641.861.573s0.654s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe1.941.000.764s0.062s
ssh-simplified/s3_clnt_1.cil.csafe8.625.515.162s3.145s
ssh-simplified/s3_clnt_2.cil.csafe8.505.525.170s3.385s
ssh-simplified/s3_clnt_3.cil.csafe9.686.406.064s3.185s
ssh-simplified/s3_clnt_4.cil.csafe8.995.905.583s3.361s
ssh-simplified/s3_srvr_1a.cil.csafe3.712.071.773s1.088s
ssh-simplified/s3_srvr_1b.cil.csafe1.811.010.772s0.141s
ssh-simplified/s3_srvr_1.cil.csafe33.9329.6329.149s21.541s
ssh-simplified/s3_srvr_3.cil.csafe24.6120.3219.817s13.135s
ssh-simplified/s3_srvr_4.cil.csafe14.4410.199.764s7.946s
ssh-simplified/s3_srvr_6.cil.csafe16.1511.7111.260s9.354s
ssh-simplified/s3_srvr_7.cil.csafe22.5118.4417.945s16.147s
ssh-simplified/s3_srvr_8.cil.csafe13.649.659.211s5.985s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe5.082.802.499s1.208s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.632.612.314s1.113s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.632.482.183s0.937s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe3.982.141.854s0.773s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.482.392.086s0.961s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.262.241.942s0.873s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe3.881.961.687s0.701s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.182.131.800s0.723s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.012.702.398s1.086s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.844.524.212s2.711s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe7.764.584.264s2.505s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.413.923.599s1.769s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.592.942.660s1.551s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.422.692.402s1.110s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.267.447.161s5.764s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.112.822.530s1.326s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.214.023.691s1.841s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.942.602.301s1.075s
ssh/s3_clnt.blast.01.i.cil.csafe9.386.165.834s3.962s
ssh/s3_clnt.blast.03.i.cil.csafe8.835.515.187s3.728s
ssh/s3_clnt.blast.04.i.cil.csafe10.937.537.159s5.081s
ssh/s3_srvr.blast.01.i.cil.csafe13.949.148.679s5.833s
ssh/s3_srvr.blast.06.i.cil.csafe16.4111.6111.124s9.273s
ssh/s3_srvr.blast.07.i.cil.csafe14.6010.209.734s8.245s
ssh/s3_srvr.blast.08.i.cil.csegmentation fault87.8883.74--
ssh/s3_srvr.blast.09.i.cil.csafe13.078.598.153s5.988s
ssh/s3_srvr.blast.10.i.cil.csafe52.7947.8947.358s15.544s
ssh/s3_srvr.blast.12.i.cil.csafe39.9534.7434.222s15.852s
ssh/s3_srvr.blast.13.i.cil.csafe21.7517.3716.886s14.526s
ssh/s3_srvr.blast.14.i.cil.csafe35.4530.0929.488s22.690s
ssh/s3_srvr.blast.15.i.cil.csafe14.149.098.546s5.892s
ssh/s3_srvr.blast.16.i.cil.csafe16.8012.0311.552s8.248s
locks/test_locks_14.BUG.cunsafe1.811.020.757s0.109s
locks/test_locks_15.BUG.cunsafe1.901.130.869s0.135s
locks/test_locks_11.csafe1.821.000.727s0.093s
locks/test_locks_12.csafe1.660.880.622s0.086s
locks/test_locks_13.csafe1.660.890.634s0.096s
locks/test_locks_14.csafe1.630.870.638s0.102s
locks/test_locks_15.csafe1.700.980.729s0.115s
locks/test_locks_5.csafe1.490.840.606s0.043s
locks/test_locks_6.csafe1.530.860.583s0.047s
locks/test_locks_7.csafe1.660.910.660s0.060s
locks/test_locks_8.csafe1.680.930.688s0.068s
locks/test_locks_9.csafe1.570.830.595s0.067s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.261.170.914s0.191s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.890.970.731s0.115s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.001.090.837s0.175s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown63.8061.3060.992s58.001s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.331.190.929s0.189s
heap-manipulation/dll_of_dll.cil.cunknown1.871.060.808s0.112s
heap-manipulation/merge_sort.cil.csafe1.680.920.676s0.079s
heap-manipulation/sll_to_dll_rev.cil.cunknown62.8460.9760.702s54.253s
list-properties/alternating_list.cil.csafe1.921.010.769s0.166s
list-properties/list.cil.csafe2.041.090.827s0.202s
list-properties/list_flag.cil.csafe2.161.090.829s0.197s
list-properties/simple.cil.cunsafe1.881.030.782s0.143s
list-properties/simple_built_from_end.cil.cunsafe1.901.030.762s0.113s
list-properties/splice.cil.cunsafe3.502.271.993s0.975s
systemc/token_ring.01.BUG.cil.cunsafe2.911.541.275s0.545s
systemc/token_ring.02.BUG.cil.cunsafe5.102.652.339s1.309s
systemc/token_ring.03.BUG.cil.cunsafe7.963.933.542s2.418s
systemc/transmitter.01.BUG.cil.cunsafe2.281.240.964s0.290s
systemc/transmitter.02.BUG.cil.cunsafe2.971.631.355s0.585s
systemc/transmitter.03.BUG.cil.cunsafe5.012.452.154s1.339s
systemc/transmitter.04.BUG.cil.cunsafe8.974.864.447s3.314s
systemc/bist_cell.cil.csafe2.501.381.055s0.387s
systemc/kundu.cil.csafe17.1712.2911.723s10.203s
systemc/mem_slave_tlm.1.cil.cout of memory51.8247.08--
systemc/mem_slave_tlm.2.cil.cout of memory54.4950.01--
systemc/pc_sfifo_1.cil.csafe5.672.672.315s1.457s
systemc/pc_sfifo_2.cil.csafe5.743.032.711s1.716s
systemc/pc_sfifo_3.cil.csafe2.291.210.950s0.348s
systemc/token_ring.01.cil.csafe4.922.422.080s1.286s
systemc/token_ring.04.cil.cunknown73.3361.5960.747s54.563s
systemc/toy.cil.cunknown68.5862.9362.454s59.381s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.580.920.680s0.023s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.750.950.704s0.046s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.420.790.544s0.014s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.600.850.601s0.048s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.580.890.576s0.015s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.730.970.663s0.019s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.580.820.586s0.034s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.611.000.670s0.049s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.971.080.822s0.106s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.171.180.866s0.230s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.640.890.653s0.043s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.550.870.569s0.031s
ldv-regression/alias_of_return.c-safe.cil.csafe1.630.960.626s0.018s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.520.900.671s0.021s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.540.820.574s0.020s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.540.800.545s0.016s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.361.230.989s0.309s
ldv-regression/just_assert.c-safe.cil.csafe1.530.820.560s0.015s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.470.890.594s0.026s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.580.940.682s0.081s
ldv-regression/nested_structure-safe.cil.cunsafe1.720.860.611s0.051s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.640.860.596s0.019s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.500.800.546s0.016s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.440.810.576s0.020s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.880.960.717s0.115s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.560.840.593s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.500.820.569s0.020s
ldv-regression/oomInt.c-safe_1.cil.csafe1.660.910.659s0.021s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.610.880.640s0.047s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.600.840.576s0.023s
ldv-regression/rule60_list2.c-safe.cil.csafe1.720.900.653s0.106s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.480.790.547s0.018s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.570.800.561s0.016s
ldv-regression/test_address.c-safe.cil.cunsafe1.590.870.622s0.019s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.720.930.643s0.025s
ldv-regression/test_malloc-1-safe.cil.csafe1.840.970.709s0.044s
ldv-regression/test_malloc-2-safe.cil.csafe1.881.060.746s0.033s
ldv-regression/test_overflow.c-safe.cil.csafe1.490.810.556s0.022s
ldv-regression/test_union.c-safe.cil.csafe1.580.880.643s0.020s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.590.950.684s0.015s
ldv-regression/test_union_cast-1-safe.cil.csafe1.660.850.620s0.016s
ldv-regression/test_union_cast-2-safe.cil.csafe1.520.850.601s0.027s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.600.820.579s0.022s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.500.820.563s0.015s
ldv-regression/volatile_alias.c-safe.cil.csafe1.520.800.556s0.018s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.490.770.535s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.242.091.819s0.629s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.871.911.646s0.496s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.911.931.682s0.567s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.621.721.470s0.484s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.781.821.566s0.476s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.931.841.578s0.525s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.181.971.694s0.513s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.162.051.783s0.589s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.731.791.522s0.475s
ddv-machzwd/ddv_machzwd_outl.cil.csafe4.001.911.643s0.563s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.751.871.595s0.572s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.811.801.540s0.493s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.212.061.803s0.615s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe12.745.315.009s0.450s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe17.8410.339.992s7.214s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown89.6063.4162.843s60.770s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe13.414.874.596s0.803s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown78.6463.6963.257s40.390s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe17.639.539.139s6.800s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown84.2563.4262.984s59.430s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe6.062.562.302s0.194s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe10.474.113.849s0.380s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe11.867.667.312s5.104s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown86.4162.4761.891s53.666s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe5.822.572.290s0.533s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe41.2931.4030.833s22.024s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe4.682.332.058s0.878s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown91.9563.5963.124s61.346s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown87.2165.1664.671s61.131s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown84.9162.0861.429s60.444s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe8.344.824.513s3.061s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown4.722.292.009s0.856s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown94.1267.3866.876s61.379s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.722.251.946s0.821s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown90.9164.1563.660s61.459s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown86.6264.2063.706s61.973s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.361.791.503s0.342s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown82.5462.5662.000s60.238s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown87.5063.2462.749s60.531s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown87.4163.8163.305s60.952s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe7.004.063.770s2.422s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown82.6763.0462.333s61.256s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown84.1362.9862.386s60.987s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown89.4562.7062.174s61.016s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown88.3364.5464.042s61.437s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.261.621.359s0.356s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown101.5962.2061.706s50.210s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe2.791.491.232s0.167s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown80.1362.5061.940s57.855s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown92.4463.6963.166s61.385s