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.1107
Test setintegration-predicateAnalysis-abm
branch-r5647
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202616.981950.591438.9751057.131
correct results1761649.161074.421021.170675.021
false negatives00000
false positives1935.1819.5815.0592.275
score (220 files, max score: 356)239
pthread/fib_bench_BUG.cil.cunknown1.590.990.717s0.037s
pthread/fib_bench_longer_BUG.cil.cunknown1.481.691.414s0.030s
pthread/queue_BUG.cil.cunknown2.041.370.947s0.121s
pthread/reorder_5_BUG.cil.cunknown2.071.160.880s0.127s
pthread/twostage_3_BUG.cil.cunknown2.071.100.815s0.144s
pthread/fib_bench.cil.cunknown1.622.000.668s0.035s
pthread/fib_bench_longer.cil.cunknown1.590.900.647s0.027s
pthread/queue_ok.cil.cunknown1.921.230.953s0.114s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe13.487.787.421s4.896s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.203.423.144s1.647s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe8.944.013.707s2.081s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe4.822.251.975s0.947s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe12.657.116.800s4.381s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.305.535.189s3.417s
ntdrivers-simplified/floppy_simpl3.cil.csafe9.514.924.606s2.834s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.926.265.890s3.697s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.321.911.552s0.582s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.932.662.333s1.036s
ntdrivers/cdaudio.BUG.i.cil.cunsafe14.607.687.283s4.146s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.096.015.672s2.937s
ntdrivers/floppy.BUG.i.cil.cunsafe12.506.496.099s3.102s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.693.703.364s1.377s
ntdrivers/parport.BUG.i.cil.cunsafe20.2211.7911.407s6.272s
ntdrivers/cdaudio.i.cil.csafe18.2010.6010.220s6.360s
ntdrivers/diskperf.i.cil.csafe11.866.496.179s3.606s
ntdrivers/floppy.i.cil.csafe15.188.878.501s4.319s
ntdrivers/parport.i.cil.csafe29.2920.0119.579s11.788s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.313.273.002s1.747s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.082.692.414s1.278s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.072.752.476s1.247s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.282.412.127s0.994s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.0113.3613.012s10.111s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe62.0155.0154.541s49.269s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.73115.52--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.4514.1313.787s10.640s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.842.111.812s0.782s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.822.502.198s1.228s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.231.090.818s0.055s
ssh-simplified/s3_clnt_1.cil.csafe10.366.916.607s4.551s
ssh-simplified/s3_clnt_2.cil.csafe9.385.465.172s3.151s
ssh-simplified/s3_clnt_3.cil.csafe7.924.674.353s2.709s
ssh-simplified/s3_clnt_4.cil.csafe12.568.378.087s5.117s
ssh-simplified/s3_srvr_1a.cil.csafe4.742.372.058s1.377s
ssh-simplified/s3_srvr_1b.cil.csafe2.021.080.817s0.221s
ssh-simplified/s3_srvr_1.cil.cout of memory67.9563.28--
ssh-simplified/s3_srvr_3.cil.csafe25.4319.9619.517s14.191s
ssh-simplified/s3_srvr_4.cil.csafe10.706.916.420s4.925s
ssh-simplified/s3_srvr_6.cil.ctimeout119.63114.91--
ssh-simplified/s3_srvr_7.cil.cunknown68.7666.2465.941s64.739s
ssh-simplified/s3_srvr_8.cil.csafe16.8112.2211.820s8.491s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.843.843.546s1.946s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe5.202.902.607s1.212s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.962.732.385s1.105s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe6.393.603.290s1.768s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe6.022.962.618s1.280s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.842.542.247s1.033s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe5.142.742.464s1.250s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.772.452.141s0.992s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.983.032.762s1.417s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown68.0163.6663.339s61.803s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.7020.0319.644s17.536s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe39.0432.6332.184s29.008s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.302.852.564s1.249s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.197.457.099s5.572s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe29.0723.4022.958s20.831s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.843.513.229s1.884s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.3414.5014.091s12.053s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe7.334.203.867s2.253s
ssh/s3_clnt.blast.01.i.cil.csafe9.386.165.680s3.586s
ssh/s3_clnt.blast.03.i.cil.csafe12.709.098.793s5.954s
ssh/s3_clnt.blast.04.i.cil.csafe12.928.548.201s4.759s
ssh/s3_srvr.blast.01.i.cil.csafe33.5629.3328.857s24.344s
ssh/s3_srvr.blast.06.i.cil.csafe27.2821.4221.007s15.916s
ssh/s3_srvr.blast.07.i.cil.cunknown69.2865.5065.168s63.623s
ssh/s3_srvr.blast.08.i.cil.csafe24.9720.0119.616s15.813s
ssh/s3_srvr.blast.09.i.cil.cunknown65.5862.3061.955s59.841s
ssh/s3_srvr.blast.10.i.cil.csafe10.726.776.398s4.418s
ssh/s3_srvr.blast.12.i.cil.csafe12.8611.4611.064s6.514s
ssh/s3_srvr.blast.13.i.cil.cunknown64.3464.0862.706s60.176s
ssh/s3_srvr.blast.14.i.cil.csafe36.0631.0630.633s24.896s
ssh/s3_srvr.blast.15.i.cil.csafe14.7610.7410.361s5.419s
ssh/s3_srvr.blast.16.i.cil.csafe41.2736.8336.381s26.553s
locks/test_locks_14.BUG.cunsafe2.271.301.061s0.391s
locks/test_locks_15.BUG.cunsafe2.271.331.090s0.431s
locks/test_locks_11.csafe1.961.140.898s0.273s
locks/test_locks_12.csafe2.081.210.971s0.344s
locks/test_locks_13.csafe2.121.231.000s0.350s
locks/test_locks_14.csafe2.161.251.017s0.375s
locks/test_locks_15.csafe2.501.481.247s0.463s
locks/test_locks_5.csafe1.540.910.667s0.108s
locks/test_locks_6.csafe1.520.910.669s0.118s
locks/test_locks_7.csafe1.630.960.716s0.140s
locks/test_locks_8.csafe1.701.010.770s0.180s
locks/test_locks_9.csafe1.761.050.816s0.209s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.121.170.931s0.163s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.720.950.704s0.093s
heap-manipulation/merge_sort_BUG.cil.cunsafe1.871.050.802s0.141s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.151.200.947s0.166s
heap-manipulation/dll_of_dll.cil.cunknown1.740.960.702s0.084s
heap-manipulation/merge_sort.cil.csafe1.700.950.714s0.071s
heap-manipulation/sll_to_dll_rev.cil.cunknown12.3410.8110.557s8.072s
list-properties/alternating_list.cil.csafe1.690.960.710s0.156s
list-properties/list.cil.csafe1.751.000.761s0.202s
list-properties/list_flag.cil.csafe1.870.980.727s0.153s
list-properties/simple.cil.cunsafe1.660.950.716s0.144s
list-properties/simple_built_from_end.cil.cunsafe1.660.970.734s0.141s
list-properties/splice.cil.cunsafe2.931.911.667s0.625s
systemc/token_ring.01.BUG.cil.cunsafe2.761.621.350s0.500s
systemc/token_ring.02.BUG.cil.cunsafe4.702.452.183s1.084s
systemc/token_ring.03.BUG.cil.cunsafe6.063.383.121s1.742s
systemc/transmitter.01.BUG.cil.cunsafe2.191.291.046s0.299s
systemc/transmitter.02.BUG.cil.cunsafe3.001.791.534s0.624s
systemc/transmitter.03.BUG.cil.cunsafe3.932.101.844s0.758s
systemc/transmitter.04.BUG.cil.cunsafe5.002.592.328s0.961s
systemc/bist_cell.cil.csafe18.0914.9414.652s12.798s
systemc/kundu.cil.cexception5.873.16--
systemc/mem_slave_tlm.1.cil.cexception40.9535.95--
systemc/mem_slave_tlm.2.cil.csafe66.3061.8161.470s59.290s
systemc/pc_sfifo_1.cil.csafe5.863.112.866s1.526s
systemc/pc_sfifo_2.cil.csafe7.904.724.475s2.740s
systemc/pc_sfifo_3.cil.csafe6.873.693.437s1.984s
systemc/token_ring.01.cil.csafe7.744.494.248s2.392s
systemc/token_ring.04.cil.csafe65.4260.8460.552s57.667s
systemc/toy.cil.ctimeout119.60112.96--
ldv-regression/1_3.c-unsafe.cil.cunsafe1.280.750.529s0.026s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.340.800.583s0.050s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.260.730.508s0.015s
ldv-regression/fo_test.c-unsafe.cil.cunknown0.980.57--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.270.740.511s0.016s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.290.760.518s0.017s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.310.770.546s0.037s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.320.810.566s0.032s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.931.130.873s0.202s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.091.261.037s0.432s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.300.780.550s0.042s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.350.770.541s0.033s
ldv-regression/alias_of_return.c-safe.cil.csafe1.280.750.524s0.029s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.270.730.505s0.018s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.280.760.534s0.033s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.260.740.509s0.017s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe1.771.060.820s0.197s
ldv-regression/just_assert.c-safe.cil.csafe1.270.710.486s0.009s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.260.740.510s0.016s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.290.750.515s0.017s
ldv-regression/nested_structure-safe.cil.cunsafe1.320.790.567s0.039s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.320.750.522s0.021s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.600.880.633s0.016s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.530.860.621s0.018s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.560.900.674s0.088s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.320.760.535s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.290.770.527s0.030s
ldv-regression/oomInt.c-safe_1.cil.csafe1.360.760.533s0.031s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.460.860.633s0.047s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.480.790.569s0.023s
ldv-regression/rule60_list2.c-safe.cil.csafe1.841.090.856s0.211s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.370.780.555s0.027s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.560.880.623s0.018s
ldv-regression/test_address.c-safe.cil.cunsafe1.640.910.649s0.022s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.390.810.538s0.019s
ldv-regression/test_malloc-1-safe.cil.csafe1.310.760.534s0.028s
ldv-regression/test_malloc-2-safe.cil.csafe1.300.750.524s0.026s
ldv-regression/test_overflow.c-safe.cil.csafe1.550.900.666s0.028s
ldv-regression/test_union.c-safe.cil.csafe1.280.740.516s0.016s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.330.770.543s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.300.740.514s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.300.750.526s0.023s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.360.770.546s0.020s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.310.760.527s0.018s
ldv-regression/volatile_alias.c-safe.cil.csafe1.300.740.515s0.017s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.300.750.512s0.016s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.491.841.593s0.332s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.331.801.560s0.336s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.321.801.565s0.338s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.091.561.321s0.337s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.011.561.325s0.331s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.051.561.327s0.331s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.051.561.328s0.330s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.021.551.310s0.328s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.291.741.507s0.412s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.061.571.333s0.330s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.081.581.343s0.348s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.131.571.337s0.336s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.061.571.333s0.331s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.055.725.452s0.432s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe9.945.355.063s1.841s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.246.666.264s2.646s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe11.924.514.228s0.511s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe16.508.628.315s3.114s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe8.463.773.482s1.290s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe17.379.779.444s3.948s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe8.363.533.263s0.258s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe13.615.375.099s0.986s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe10.715.995.684s2.534s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe41.4124.6124.234s9.920s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.122.932.664s0.558s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.2210.4010.066s4.311s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.922.742.456s0.852s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe15.497.727.362s5.253s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe15.166.666.349s1.167s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe35.0418.0217.594s10.445s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe9.954.984.679s2.980s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe11.045.805.469s3.276s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe16.217.667.341s0.981s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown3.811.921.671s0.650s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe6.012.852.579s1.051s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe16.848.037.692s5.014s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.042.141.895s0.677s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe12.726.145.793s3.629s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown87.9763.3862.962s60.119s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe18.208.568.206s5.588s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe7.834.063.784s1.820s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.852.732.479s0.921s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe7.983.533.221s1.499s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.262.071.795s0.630s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe16.857.286.899s3.505s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.462.061.813s0.487s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe19.2510.689.370s3.719s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.651.761.476s0.166s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe11.665.324.422s2.084s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe6.062.892.609s0.911s