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.1354
Test setintegration-predicateAnalysis
branch-r5655
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2211840.441300.83922.167658.690
correct results130871.05578.09536.778307.418
false negatives00000
false positives1019.0910.067.5670.736
score (221 files, max score: 357)183
pthread/fib_bench_BUG.cil.cunknown1.482.981.534s0.022s
pthread/fib_bench_longer_BUG.cil.cunknown1.710.890.642s0.022s
pthread/queue_BUG.cil.cexception1.551.36--
pthread/reorder_5_BUG.cil.cexception1.821.05--
pthread/twostage_3_BUG.cil.cexception1.640.90--
pthread/fib_bench.cil.cunknown1.510.830.591s0.021s
pthread/fib_bench_longer.cil.cunknown1.410.850.612s0.023s
pthread/queue_ok.cil.cexception1.640.95--
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe5.563.282.923s1.641s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.581.981.698s0.741s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe3.802.091.798s0.802s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe2.981.551.306s0.525s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe4.812.742.473s1.558s
ntdrivers-simplified/diskperf_simpl1.cil.csafe3.962.292.031s1.376s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.261.721.460s0.731s
ntdrivers-simplified/floppy_simpl4.cil.csafe3.691.911.638s0.867s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.341.150.882s0.302s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe2.901.381.128s0.463s
ntdrivers/cdaudio.BUG.i.cil.cunsafe9.254.904.597s2.465s
ntdrivers/diskperf.BUG.i.cil.cunsafe5.863.403.120s1.694s
ntdrivers/floppy.BUG.i.cil.cexception4.742.40--
ntdrivers/kbfiltr.BUG.i.cil.cexception2.201.17--
ntdrivers/parport.BUG.i.cil.cexception5.032.41--
ntdrivers/cdaudio.i.cil.csafe8.924.634.330s2.527s
ntdrivers/diskperf.i.cil.csafe5.282.932.625s1.625s
ntdrivers/floppy.i.cil.cexception4.752.38--
ntdrivers/parport.i.cil.cexception4.902.22--
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.381.881.614s0.693s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe3.942.171.895s0.832s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe3.902.241.948s0.858s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.392.402.126s0.995s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.781.431.165s0.307s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe6.383.423.115s1.651s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.987.997.691s5.776s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.561.851.534s0.524s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.942.161.871s0.846s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.611.841.549s0.602s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.191.180.922s0.068s
ssh-simplified/s3_clnt_1.cil.csafe8.735.725.386s3.266s
ssh-simplified/s3_clnt_2.cil.csafe9.125.955.607s3.725s
ssh-simplified/s3_clnt_3.cil.csafe9.916.726.389s3.175s
ssh-simplified/s3_clnt_4.cil.csafe9.106.105.782s3.546s
ssh-simplified/s3_srvr_1a.cil.csafe3.701.951.606s0.940s
ssh-simplified/s3_srvr_1b.cil.csafe1.801.030.776s0.139s
ssh-simplified/s3_srvr_1.cil.csafe35.1530.8430.331s22.281s
ssh-simplified/s3_srvr_3.cil.csafe25.1420.9720.522s13.665s
ssh-simplified/s3_srvr_4.cil.csafe14.2510.149.667s7.717s
ssh-simplified/s3_srvr_6.cil.csafe16.4912.1311.641s9.632s
ssh-simplified/s3_srvr_7.cil.csafe23.2719.0718.586s16.655s
ssh-simplified/s3_srvr_8.cil.csafe13.469.499.054s6.087s
ssh/s3_clnt.blast.01.BUG.i.cil.cexception2.021.18--
ssh/s3_clnt.blast.02.BUG.i.cil.cexception2.151.20--
ssh/s3_clnt.blast.03.BUG.i.cil.cexception2.161.27--
ssh/s3_clnt.blast.04.BUG.i.cil.cexception2.231.20--
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.492.321.994s0.862s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.042.101.788s0.703s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.382.372.090s0.896s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.282.302.006s0.848s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.192.842.524s1.067s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.434.554.228s2.697s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe8.084.874.486s2.576s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.424.093.759s1.832s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe6.203.493.168s1.708s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.853.002.726s1.280s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe11.118.027.732s6.162s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.323.002.703s1.365s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.894.333.986s1.916s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.722.642.357s1.114s
ssh/s3_clnt.blast.01.i.cil.cexception2.171.16--
ssh/s3_clnt.blast.03.i.cil.cexception2.051.12--
ssh/s3_clnt.blast.04.i.cil.cexception2.381.34--
ssh/s3_srvr.blast.01.i.cil.csafe13.528.878.404s5.377s
ssh/s3_srvr.blast.06.i.cil.csafe16.4912.0911.592s9.693s
ssh/s3_srvr.blast.07.i.cil.csafe15.0110.7410.208s8.566s
ssh/s3_srvr.blast.08.i.cil.cout of memory94.6790.83--
ssh/s3_srvr.blast.09.i.cil.csafe13.579.118.669s6.169s
ssh/s3_srvr.blast.10.i.cil.csafe51.2347.6147.067s15.263s
ssh/s3_srvr.blast.12.i.cil.csafe41.7537.2636.742s16.331s
ssh/s3_srvr.blast.13.i.cil.csafe22.2217.7717.274s14.647s
ssh/s3_srvr.blast.14.i.cil.csafe35.9030.7330.133s23.382s
ssh/s3_srvr.blast.15.i.cil.csafe13.969.398.915s6.092s
ssh/s3_srvr.blast.16.i.cil.csafe17.0312.2011.716s8.104s
locks/test_locks_14.BUG.cunsafe1.861.100.838s0.102s
locks/test_locks_15.BUG.cunsafe2.001.120.834s0.118s
locks/test_locks_11.csafe1.791.030.740s0.087s
locks/test_locks_12.csafe1.871.030.738s0.101s
locks/test_locks_13.csafe1.901.140.856s0.112s
locks/test_locks_14.csafe1.911.100.814s0.143s
locks/test_locks_15.csafe1.701.020.715s0.122s
locks/test_locks_5.csafe1.580.970.676s0.046s
locks/test_locks_6.csafe1.780.950.683s0.049s
locks/test_locks_7.csafe1.871.020.756s0.066s
locks/test_locks_8.csafe1.841.070.785s0.084s
locks/test_locks_9.csafe1.871.010.753s0.084s
heap-manipulation/bubble_sort_linux_BUG.cil.cexception1.801.01--
heap-manipulation/dll_of_dll_BUG.cil.cexception1.911.00--
heap-manipulation/merge_sort_BUG.cil.cexception1.630.93--
heap-manipulation/sll_to_dll_rev_BUG.cil.cexception1.700.95--
heap-manipulation/bubble_sort_linux.cil.cexception1.740.98--
heap-manipulation/dll_of_dll.cil.cexception1.670.89--
heap-manipulation/merge_sort.cil.cexception1.870.98--
heap-manipulation/sll_to_dll_rev.cil.cexception1.701.03--
list-properties/alternating_list.cil.cexception1.620.97--
list-properties/list.cil.cexception1.791.05--
list-properties/list_flag.cil.cexception1.650.97--
list-properties/simple.cil.cexception1.700.93--
list-properties/simple_built_from_end.cil.cexception1.660.91--
list-properties/splice.cil.cexception1.480.89--
systemc/token_ring.01.BUG.cil.cunsafe3.211.811.539s0.715s
systemc/token_ring.02.BUG.cil.cunsafe4.732.311.969s1.170s
systemc/token_ring.03.BUG.cil.cunsafe7.213.743.331s2.369s
systemc/transmitter.01.BUG.cil.cunsafe2.181.150.896s0.250s
systemc/transmitter.02.BUG.cil.cunsafe3.041.621.355s0.572s
systemc/transmitter.03.BUG.cil.cunsafe4.962.492.188s1.287s
systemc/transmitter.04.BUG.cil.cunsafe9.484.944.563s3.361s
systemc/bist_cell.cil.csafe2.381.361.074s0.417s
systemc/kundu.cil.csafe16.8612.5612.027s10.387s
systemc/mem_slave_tlm.1.cil.cunknown51.9247.65--
systemc/mem_slave_tlm.2.cil.csegmentation fault55.2250.02--
systemc/pc_sfifo_1.cil.csafe5.312.482.169s1.443s
systemc/pc_sfifo_2.cil.csafe5.292.742.456s1.602s
systemc/pc_sfifo_3.cil.csafe2.201.180.896s0.324s
systemc/token_ring.01.cil.csafe4.602.241.860s1.063s
systemc/token_ring.04.cil.cunknown74.7061.4960.619s54.872s
systemc/toy.cil.cunknown67.2861.9461.483s58.513s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.761.010.756s0.034s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.921.030.727s0.049s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.810.940.676s0.018s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.360.72--
ldv-regression/mutex_lock_int.c-unsafe.cil.cexception1.600.84--
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.720.980.691s0.023s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.540.860.615s0.031s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.550.880.636s0.029s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.700.930.666s0.085s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.071.200.926s0.241s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.650.880.635s0.048s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.610.910.680s0.029s
ldv-regression/alias_of_return.c-safe.cil.cexception1.410.72--
ldv-regression/alias_of_return.c-safe_1.cil.cexception1.260.71--
ldv-regression/alias_of_return_2.c-safe.cil.cexception1.460.75--
ldv-regression/alias_of_return_2.c-safe_1.cil.cexception1.390.76--
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.341.311.075s0.340s
ldv-regression/just_assert.c-safe.cil.csafe1.680.900.658s0.015s
ldv-regression/mutex_lock_int.c-safe_1.cil.cexception1.750.89--
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.590.830.569s0.015s
ldv-regression/nested_structure-safe.cil.cexception1.650.89--
ldv-regression/nested_structure.c-safe.cil.cunsafe1.700.890.654s0.023s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.770.890.649s0.021s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.780.920.663s0.024s
ldv-regression/nested_structure_ptr-safe.cil.cexception1.540.86--
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.570.900.647s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.510.810.582s0.019s
ldv-regression/oomInt.c-safe_1.cil.csafe1.520.880.635s0.023s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.490.830.600s0.042s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.570.860.633s0.026s
ldv-regression/rule60_list2.c-safe.cil.csafe1.820.970.722s0.093s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.760.900.632s0.023s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.620.820.577s0.023s
ldv-regression/test_address.c-safe.cil.cunsafe1.600.820.567s0.018s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.760.920.667s0.021s
ldv-regression/test_malloc-1-safe.cil.csafe1.740.930.676s0.036s
ldv-regression/test_malloc-2-safe.cil.csafe1.600.840.565s0.027s
ldv-regression/test_overflow.c-safe.cil.csafe1.580.870.613s0.022s
ldv-regression/test_union.c-safe.cil.csafe1.760.880.636s0.019s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.760.910.651s0.019s
ldv-regression/test_union_cast-1-safe.cil.csafe1.480.810.590s0.015s
ldv-regression/test_union_cast-2-safe.cil.cexception1.490.79--
ldv-regression/test_union_cast.c-safe.cil.cexception1.560.76--
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.490.830.599s0.015s
ldv-regression/volatile_alias.c-safe.cil.cexception1.390.82--
ldv-regression/volatile_alias.c-safe_1.cil.cexception1.430.73--
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.832.001.759s0.528s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.701.911.667s0.538s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.921.971.721s0.589s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.861.911.653s0.556s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.312.051.767s0.565s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.101.981.727s0.591s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.302.121.799s0.519s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.072.031.754s0.531s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.741.801.513s0.547s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.881.931.665s0.578s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.761.861.589s0.467s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.581.741.485s0.459s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.062.061.802s0.486s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe12.874.974.681s0.395s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cexception4.452.10--
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cexception5.682.36--
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cexception12.764.64--
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cexception8.663.53--
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cexception6.122.62--
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown84.5964.5464.083s61.467s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.923.082.827s0.231s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe19.146.926.667s0.385s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.507.727.343s5.093s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown81.8063.0062.472s53.887s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cexception5.552.47--
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cexception8.894.45--
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cexception3.711.80--
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cexception5.632.54--
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cexception13.275.14--
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cexception10.425.50--
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe8.555.014.707s3.050s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cexception5.012.44--
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cexception15.426.51--
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cexception3.871.93--
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cexception6.092.47--
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cexception8.273.77--
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.101.621.346s0.314s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cexception5.703.45--
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cexception7.797.30--
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cexception7.717.13--
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe9.427.956.847s4.015s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown83.2066.4363.153s60.692s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown82.9265.8462.633s61.017s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cexception4.292.16--
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cexception11.694.42--
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cexception3.581.83--
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cexception4.472.12--
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.851.891.594s0.208s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cexception7.773.50--
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cexception4.452.17--