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-20.1447
Test setintegration-predicateAnalysis-abm
branch-r5669
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202693.622021.951624.4031232.382
correct results1791843.731258.641205.908848.526
false negatives00000
false positives1937.5721.0616.1442.571
score (220 files, max score: 356)244
pthread/fib_bench_BUG.cil.cunknown1.813.021.554s0.035s
pthread/fib_bench_longer_BUG.cil.cunknown1.500.820.582s0.027s
pthread/queue_BUG.cil.cunknown1.961.050.816s0.116s
pthread/reorder_5_BUG.cil.cunknown1.981.100.839s0.128s
pthread/twostage_3_BUG.cil.cunknown2.091.120.868s0.131s
pthread/fib_bench.cil.cunknown1.740.950.697s0.034s
pthread/fib_bench_longer.cil.cunknown1.542.060.606s0.025s
pthread/queue_ok.cil.cunknown1.941.010.767s0.099s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe16.4710.5210.200s7.160s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.383.623.339s1.730s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe8.974.434.121s2.356s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.682.722.410s1.197s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.818.347.984s5.167s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.205.775.362s3.401s
ntdrivers-simplified/floppy_simpl3.cil.csafe9.535.014.694s2.835s
ntdrivers-simplified/floppy_simpl4.cil.csafe12.086.906.547s4.391s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.921.671.402s0.566s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.582.502.158s0.948s
ntdrivers/cdaudio.BUG.i.cil.cunsafe14.287.026.703s3.801s
ntdrivers/diskperf.BUG.i.cil.cunsafe10.425.325.006s2.596s
ntdrivers/floppy.BUG.i.cil.cunsafe12.476.546.165s2.980s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe6.893.232.937s1.225s
ntdrivers/parport.BUG.i.cil.cunsafe20.2612.2311.827s6.685s
ntdrivers/cdaudio.i.cil.csafe18.3511.0810.686s6.768s
ntdrivers/diskperf.i.cil.csafe12.807.697.324s4.370s
ntdrivers/floppy.i.cil.csafe15.989.889.518s5.110s
ntdrivers/parport.i.cil.csafe28.2319.4919.038s11.336s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.503.222.946s1.814s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.942.652.382s1.251s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.742.952.654s1.428s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.482.482.216s1.077s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe18.6213.7113.353s10.382s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe62.3056.1655.700s49.928s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.58115.55--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.0913.1812.750s9.938s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.882.221.920s0.905s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.702.482.183s1.225s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.161.070.819s0.058s
ssh-simplified/s3_clnt_1.cil.csafe10.967.777.406s5.003s
ssh-simplified/s3_clnt_2.cil.csafe9.296.275.952s3.700s
ssh-simplified/s3_clnt_3.cil.csafe8.305.194.780s2.984s
ssh-simplified/s3_clnt_4.cil.csafe11.408.087.806s5.006s
ssh-simplified/s3_srvr_1a.cil.csafe4.682.532.193s1.435s
ssh-simplified/s3_srvr_1b.cil.csafe2.001.070.827s0.247s
ssh-simplified/s3_srvr_1.cil.cout of memory69.2264.95--
ssh-simplified/s3_srvr_3.cil.csafe25.1420.0219.587s14.292s
ssh-simplified/s3_srvr_4.cil.csafe11.326.536.175s4.735s
ssh-simplified/s3_srvr_6.cil.ctimeout119.66116.03--
ssh-simplified/s3_srvr_7.cil.cunknown68.7165.6965.290s63.864s
ssh-simplified/s3_srvr_8.cil.csafe14.4411.1710.838s7.745s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe5.542.812.550s1.359s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.102.322.062s0.973s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.352.312.060s0.911s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.372.832.553s1.346s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.122.572.300s1.127s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.162.372.098s1.018s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.272.352.091s0.976s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.272.322.063s1.032s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.433.022.767s1.295s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown67.8064.2063.908s62.605s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe23.7319.2318.849s17.021s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe34.1729.2828.893s26.345s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.042.252.013s0.972s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe9.536.566.277s4.983s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe26.9722.1521.781s19.877s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.803.232.950s1.778s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe17.7413.6213.232s11.321s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.042.992.722s1.530s
ssh/s3_clnt.blast.01.i.cil.csafe7.794.814.552s3.084s
ssh/s3_clnt.blast.03.i.cil.csafe10.887.997.728s5.438s
ssh/s3_clnt.blast.04.i.cil.csafe10.236.696.399s3.725s
ssh/s3_srvr.blast.01.i.cil.csafe30.6226.3225.960s21.732s
ssh/s3_srvr.blast.06.i.cil.csafe23.3218.4418.061s13.535s
ssh/s3_srvr.blast.07.i.cil.cunknown69.6166.0765.787s64.293s
ssh/s3_srvr.blast.08.i.cil.csafe20.5916.5716.200s13.097s
ssh/s3_srvr.blast.09.i.cil.cunknown65.6361.7661.453s59.768s
ssh/s3_srvr.blast.10.i.cil.csafe10.526.636.297s4.725s
ssh/s3_srvr.blast.12.i.cil.csafe12.698.718.319s6.647s
ssh/s3_srvr.blast.13.i.cil.cunknown65.2261.4161.087s59.420s
ssh/s3_srvr.blast.14.i.cil.csafe34.1329.4629.066s23.826s
ssh/s3_srvr.blast.15.i.cil.csafe14.3010.4110.058s5.528s
ssh/s3_srvr.blast.16.i.cil.csafe39.6234.8234.408s24.816s
locks/test_locks_14.BUG.cunsafe2.231.271.029s0.367s
locks/test_locks_15.BUG.cunsafe2.261.341.104s0.424s
locks/test_locks_11.csafe1.851.080.843s0.256s
locks/test_locks_12.csafe1.951.130.896s0.291s
locks/test_locks_13.csafe2.051.190.966s0.332s
locks/test_locks_14.csafe2.061.210.980s0.370s
locks/test_locks_15.csafe2.271.301.068s0.436s
locks/test_locks_5.csafe1.440.850.620s0.092s
locks/test_locks_6.csafe1.500.870.651s0.114s
locks/test_locks_7.csafe1.540.920.688s0.141s
locks/test_locks_8.csafe1.580.940.719s0.163s
locks/test_locks_9.csafe1.600.990.767s0.194s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.051.140.898s0.170s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.650.920.683s0.094s
heap-manipulation/merge_sort_BUG.cil.cunsafe1.801.030.787s0.148s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.301.261.025s0.179s
heap-manipulation/dll_of_dll.cil.cunknown1.700.920.690s0.105s
heap-manipulation/merge_sort.cil.csafe1.600.910.683s0.077s
heap-manipulation/sll_to_dll_rev.cil.cunknown12.1310.6110.379s8.139s
list-properties/alternating_list.cil.csafe1.600.910.681s0.140s
list-properties/list.cil.csafe1.780.990.742s0.188s
list-properties/list_flag.cil.csafe1.630.910.686s0.143s
list-properties/simple.cil.cunsafe1.640.930.699s0.137s
list-properties/simple_built_from_end.cil.cunsafe1.580.910.682s0.128s
list-properties/splice.cil.cunsafe2.971.911.673s0.653s
systemc/token_ring.01.BUG.cil.cunsafe2.641.541.299s0.475s
systemc/token_ring.02.BUG.cil.cunsafe4.592.352.096s1.008s
systemc/token_ring.03.BUG.cil.cunsafe5.743.152.905s1.594s
systemc/transmitter.01.BUG.cil.cunsafe2.151.241.011s0.323s
systemc/transmitter.02.BUG.cil.cunsafe3.261.871.619s0.716s
systemc/transmitter.03.BUG.cil.cunsafe3.752.041.803s0.754s
systemc/transmitter.04.BUG.cil.cunsafe5.062.482.213s0.936s
systemc/bist_cell.cil.csafe17.5514.8914.619s12.818s
systemc/kundu.cil.csafe67.4360.8360.519s56.975s
systemc/mem_slave_tlm.1.cil.cexception41.2935.99--
systemc/mem_slave_tlm.2.cil.csafe70.3465.9865.674s62.963s
systemc/pc_sfifo_1.cil.csafe4.802.672.432s1.279s
systemc/pc_sfifo_2.cil.csafe7.564.614.358s2.609s
systemc/pc_sfifo_3.cil.csafe6.333.573.313s1.874s
systemc/token_ring.01.cil.csafe7.604.484.239s2.389s
systemc/token_ring.04.cil.csafe65.7460.8660.546s57.928s
systemc/toy.cil.csafe114.04108.23107.901s106.278s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.520.860.611s0.031s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.670.970.713s0.061s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.510.880.624s0.020s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.640.910.671s0.050s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.420.800.544s0.018s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.510.790.545s0.017s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.590.840.582s0.040s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.640.940.657s0.041s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.141.210.956s0.217s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.481.381.138s0.421s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.380.820.580s0.043s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.500.860.623s0.034s
ldv-regression/alias_of_return.c-safe.cil.csafe1.680.960.701s0.043s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.570.890.627s0.027s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.390.810.567s0.037s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.410.810.561s0.019s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.311.230.992s0.254s
ldv-regression/just_assert.c-safe.cil.csafe1.620.900.633s0.011s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.620.890.635s0.024s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.400.780.536s0.018s
ldv-regression/nested_structure-safe.cil.cunsafe1.700.910.615s0.051s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.681.060.786s0.030s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.450.810.543s0.020s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.540.830.584s0.019s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.830.980.718s0.107s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.490.860.597s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.591.030.727s0.043s
ldv-regression/oomInt.c-safe_1.cil.csafe1.380.770.537s0.033s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.560.920.652s0.050s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.380.810.542s0.023s
ldv-regression/rule60_list2.c-safe.cil.csafe1.921.150.872s0.213s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.340.810.571s0.023s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.410.830.561s0.017s
ldv-regression/test_address.c-safe.cil.cunsafe1.390.790.554s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.500.790.555s0.022s
ldv-regression/test_malloc-1-safe.cil.csafe1.540.830.563s0.033s
ldv-regression/test_malloc-2-safe.cil.csafe1.650.950.698s0.030s
ldv-regression/test_overflow.c-safe.cil.csafe1.560.900.655s0.033s
ldv-regression/test_union.c-safe.cil.csafe1.410.850.579s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.450.890.613s0.023s
ldv-regression/test_union_cast-1-safe.cil.csafe1.500.880.592s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.450.870.596s0.037s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.550.860.635s0.026s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.470.860.595s0.022s
ldv-regression/volatile_alias.c-safe.cil.csafe1.380.870.581s0.017s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.390.810.551s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.012.151.863s0.429s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.242.322.059s0.443s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.902.241.972s0.469s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.481.761.511s0.402s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.621.931.662s0.471s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.661.821.505s0.381s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.551.851.551s0.424s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.781.961.658s0.448s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.441.921.681s0.419s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.211.641.391s0.356s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.281.661.411s0.375s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.271.621.374s0.357s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.351.701.438s0.394s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.366.115.822s0.465s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe10.835.685.391s2.094s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.457.246.919s3.449s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe12.324.624.362s0.556s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe17.149.298.973s3.042s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe10.524.704.359s1.769s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe18.5510.4510.109s4.203s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe6.892.902.643s0.204s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe13.485.445.169s1.057s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe10.776.095.780s2.599s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe44.8028.3327.922s9.387s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.293.072.765s0.590s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.5010.8310.490s3.717s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.963.032.752s1.009s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe19.1610.6210.271s7.772s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe16.367.246.909s1.074s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe42.0123.0622.571s14.353s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe10.825.605.261s3.451s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe12.186.616.267s3.829s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe17.218.097.782s1.090s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.462.181.916s0.808s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe8.083.913.583s1.658s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe22.2610.9910.618s7.331s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.602.372.118s0.770s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe15.297.757.302s4.947s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown91.1064.8464.429s61.594s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe24.4511.8011.478s8.118s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe8.344.324.027s1.968s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.082.612.344s0.954s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.133.773.480s1.568s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.772.221.942s0.738s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe19.618.998.633s4.941s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.662.342.008s0.545s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe18.8111.2110.830s5.142s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.651.901.621s0.263s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe14.257.116.697s3.819s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe6.002.842.559s1.012s