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-19.0042
Test setintegration-predicateAnalysis
branch-r5662
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2213543.712586.292319.9481918.971
correct results1611067.78713.54660.292382.509
false negatives00000
false positives1937.7020.2815.6042.520
score (221 files, max score: 357)211
pthread/fib_bench_BUG.cil.cunknown1.801.080.806s0.029s
pthread/fib_bench_longer_BUG.cil.cunknown1.921.170.882s0.033s
pthread/queue_BUG.cil.cunknown2.031.250.954s0.174s
pthread/reorder_5_BUG.cil.cunknown2.191.260.960s0.134s
pthread/twostage_3_BUG.cil.cunknown2.191.120.877s0.142s
pthread/fib_bench.cil.cunknown1.690.940.681s0.032s
pthread/fib_bench_longer.cil.cunknown1.701.030.745s0.034s
pthread/queue_ok.cil.cunknown2.051.120.841s0.115s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe6.343.943.600s2.123s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.783.553.216s0.840s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.514.723.373s1.117s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.433.383.050s0.601s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.526.025.679s1.871s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.314.364.039s1.581s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.884.202.786s1.028s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.312.322.017s1.087s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.541.381.017s0.294s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.031.951.674s0.562s
ntdrivers/cdaudio.BUG.i.cil.cunsafe10.575.785.407s2.982s
ntdrivers/diskperf.BUG.i.cil.cunsafe6.263.853.499s2.006s
ntdrivers/floppy.BUG.i.cil.cunsafe11.216.536.157s3.942s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe4.742.592.297s0.916s
ntdrivers/parport.BUG.i.cil.cunknown90.8570.4364.165s62.468s
ntdrivers/cdaudio.i.cil.csafe9.385.144.779s2.980s
ntdrivers/diskperf.i.cil.csafe5.633.332.991s1.856s
ntdrivers/floppy.i.cil.csafe25.6719.1818.765s14.189s
ntdrivers/parport.i.cil.cunknown93.3071.8963.056s61.516s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe3.672.041.755s0.739s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.152.382.105s0.958s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe4.342.352.063s0.960s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.082.261.994s0.950s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.681.371.110s0.275s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe5.973.262.958s1.527s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.507.427.113s5.410s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.131.631.363s0.469s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.791.981.692s0.735s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.471.771.489s0.560s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.201.070.823s0.056s
ssh-simplified/s3_clnt_1.cil.csafe8.125.234.849s2.928s
ssh-simplified/s3_clnt_2.cil.csafe7.985.345.021s3.364s
ssh-simplified/s3_clnt_3.cil.csafe9.376.105.755s2.902s
ssh-simplified/s3_clnt_4.cil.csafe9.026.055.730s3.358s
ssh-simplified/s3_srvr_1a.cil.csafe3.551.981.620s1.001s
ssh-simplified/s3_srvr_1b.cil.csafe1.831.050.791s0.164s
ssh-simplified/s3_srvr_1.cil.csafe34.0229.7029.215s21.570s
ssh-simplified/s3_srvr_3.cil.csafe24.4520.2719.741s13.152s
ssh-simplified/s3_srvr_4.cil.csafe15.0510.6810.223s8.112s
ssh-simplified/s3_srvr_6.cil.csafe17.6613.0412.556s10.438s
ssh-simplified/s3_srvr_7.cil.csafe23.2218.9318.422s16.629s
ssh-simplified/s3_srvr_8.cil.csafe12.728.808.376s5.720s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe4.542.542.249s1.058s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.382.462.186s0.999s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.422.432.143s1.045s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe4.002.111.837s0.828s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.012.191.918s0.863s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.042.091.802s0.833s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe3.921.981.697s0.733s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.022.061.780s0.819s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe4.632.392.098s0.933s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.074.243.954s2.590s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe7.524.464.146s2.330s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.013.843.528s1.796s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.683.022.732s1.599s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.432.642.355s1.106s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.427.276.984s5.660s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.032.842.554s1.309s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.174.143.828s1.866s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe4.922.642.343s1.084s
ssh/s3_clnt.blast.01.i.cil.csafe9.986.556.225s4.359s
ssh/s3_clnt.blast.03.i.cil.csafe8.725.515.174s3.655s
ssh/s3_clnt.blast.04.i.cil.csafe11.097.587.231s5.155s
ssh/s3_srvr.blast.01.i.cil.csafe13.799.479.026s5.753s
ssh/s3_srvr.blast.06.i.cil.csafe15.9811.3410.842s8.955s
ssh/s3_srvr.blast.07.i.cil.csafe14.409.929.455s7.962s
ssh/s3_srvr.blast.08.i.cil.cout of memory84.4280.19--
ssh/s3_srvr.blast.09.i.cil.csafe13.048.778.347s6.161s
ssh/s3_srvr.blast.10.i.cil.csafe52.2547.1346.605s15.398s
ssh/s3_srvr.blast.12.i.cil.csafe41.3136.1435.625s16.901s
ssh/s3_srvr.blast.13.i.cil.csafe23.4318.5117.968s15.444s
ssh/s3_srvr.blast.14.i.cil.csafe33.1728.2727.747s21.559s
ssh/s3_srvr.blast.15.i.cil.csafe13.478.908.436s5.925s
ssh/s3_srvr.blast.16.i.cil.csafe15.9511.2410.771s7.589s
locks/test_locks_14.BUG.cunsafe1.931.040.781s0.112s
locks/test_locks_15.BUG.cunsafe1.761.100.792s0.144s
locks/test_locks_11.csafe1.680.870.614s0.081s
locks/test_locks_12.csafe1.730.970.690s0.095s
locks/test_locks_13.csafe1.750.990.703s0.120s
locks/test_locks_14.csafe1.690.930.699s0.110s
locks/test_locks_15.csafe1.700.980.729s0.121s
locks/test_locks_5.csafe1.640.910.645s0.051s
locks/test_locks_6.csafe1.670.900.612s0.046s
locks/test_locks_7.csafe1.560.890.640s0.054s
locks/test_locks_8.csafe1.540.910.677s0.089s
locks/test_locks_9.csafe1.730.910.661s0.071s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.271.261.010s0.216s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.981.090.805s0.116s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.231.210.920s0.180s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown64.0461.4861.189s56.270s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.351.261.011s0.206s
heap-manipulation/dll_of_dll.cil.cunknown1.820.970.697s0.097s
heap-manipulation/merge_sort.cil.csafe1.650.920.684s0.082s
heap-manipulation/sll_to_dll_rev.cil.cunknown63.0560.9560.670s54.237s
list-properties/alternating_list.cil.csafe1.941.050.793s0.168s
list-properties/list.cil.csafe2.041.130.795s0.188s
list-properties/list_flag.cil.csafe2.051.100.768s0.161s
list-properties/simple.cil.cunsafe1.971.060.823s0.167s
list-properties/simple_built_from_end.cil.cunsafe1.770.980.738s0.107s
list-properties/splice.cil.cunsafe3.221.931.666s0.803s
systemc/token_ring.01.BUG.cil.cunsafe3.081.641.383s0.626s
systemc/token_ring.02.BUG.cil.cunsafe4.592.292.002s1.182s
systemc/token_ring.03.BUG.cil.cunsafe8.323.973.552s2.616s
systemc/transmitter.01.BUG.cil.cunsafe2.241.180.909s0.262s
systemc/transmitter.02.BUG.cil.cunsafe2.901.511.253s0.556s
systemc/transmitter.03.BUG.cil.cunsafe4.742.322.023s1.207s
systemc/transmitter.04.BUG.cil.cunsafe9.154.724.383s3.266s
systemc/bist_cell.cil.csafe2.511.311.021s0.388s
systemc/kundu.cil.csafe16.6012.0711.439s9.875s
systemc/mem_slave_tlm.1.cil.cout of memory52.8748.41--
systemc/mem_slave_tlm.2.cil.csegmentation fault51.3046.70--
systemc/pc_sfifo_1.cil.csafe5.332.942.578s1.761s
systemc/pc_sfifo_2.cil.csafe6.103.052.759s1.734s
systemc/pc_sfifo_3.cil.csafe2.161.150.877s0.292s
systemc/token_ring.01.cil.csafe4.482.251.934s1.114s
systemc/token_ring.04.cil.cunknown73.0661.5260.631s54.673s
systemc/toy.cil.cunknown66.5161.2860.844s57.924s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.490.780.549s0.023s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.580.880.648s0.047s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.460.840.591s0.017s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.600.890.646s0.043s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.560.890.655s0.020s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.520.830.587s0.015s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.791.010.772s0.043s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.560.890.609s0.044s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.231.260.904s0.137s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.331.361.080s0.335s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.560.860.613s0.038s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.510.820.572s0.033s
ldv-regression/alias_of_return.c-safe.cil.csafe1.600.940.693s0.021s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.500.860.612s0.016s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.710.970.675s0.025s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.500.840.591s0.017s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.361.220.966s0.308s
ldv-regression/just_assert.c-safe.cil.csafe1.740.940.660s0.014s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.510.910.681s0.016s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.620.870.634s0.016s
ldv-regression/nested_structure-safe.cil.cunsafe1.730.930.692s0.053s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.630.880.637s0.021s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.520.810.560s0.017s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.620.880.634s0.020s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe2.021.080.832s0.125s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.610.850.593s0.022s
ldv-regression/oomInt.c-safe.cil.csafe1.510.780.543s0.019s
ldv-regression/oomInt.c-safe_1.cil.csafe1.500.800.556s0.016s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.660.910.665s0.052s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.620.880.636s0.024s
ldv-regression/rule60_list2.c-safe.cil.csafe1.720.970.725s0.120s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.580.870.619s0.024s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.620.870.632s0.016s
ldv-regression/test_address.c-safe.cil.cunsafe1.750.940.687s0.019s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.490.840.575s0.016s
ldv-regression/test_malloc-1-safe.cil.csafe1.520.850.610s0.038s
ldv-regression/test_malloc-2-safe.cil.csafe1.550.800.561s0.029s
ldv-regression/test_overflow.c-safe.cil.csafe1.620.840.591s0.024s
ldv-regression/test_union.c-safe.cil.csafe1.530.800.565s0.014s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.620.810.573s0.014s
ldv-regression/test_union_cast-1-safe.cil.csafe1.530.790.546s0.016s
ldv-regression/test_union_cast-2-safe.cil.csafe1.660.890.620s0.027s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.610.820.570s0.021s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.690.930.679s0.025s
ldv-regression/volatile_alias.c-safe.cil.csafe1.690.950.660s0.023s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.610.910.636s0.022s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.422.392.120s0.643s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.991.911.652s0.488s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.861.911.649s0.532s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.982.011.726s0.638s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.911.881.623s0.509s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.042.011.741s0.595s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.051.881.614s0.549s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.921.851.571s0.494s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.891.861.560s0.494s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.981.871.602s0.553s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.821.791.523s0.479s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.091.891.630s0.632s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.711.951.654s0.509s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe12.555.385.096s0.490s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe18.3110.6210.222s7.283s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown92.9564.5864.107s62.082s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe15.705.925.615s0.689s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown79.7464.9564.455s41.193s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe15.9616.2914.892s10.259s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown84.5962.1761.763s57.318s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.482.942.632s0.197s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe11.904.564.302s0.417s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe11.187.176.843s4.785s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown87.5562.4561.934s54.632s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe4.892.362.087s0.456s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe41.1630.5430.005s21.420s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe4.782.312.047s0.880s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown95.8264.2063.698s62.073s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown88.6364.6264.101s60.016s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown86.4762.4661.725s60.231s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe9.025.044.723s3.297s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown4.342.211.934s0.789s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown94.6967.3966.872s61.019s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.482.211.934s0.849s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown88.6462.1961.693s59.800s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown82.3562.5362.021s60.394s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.101.561.292s0.319s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown83.0464.0363.468s61.709s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown89.7664.2163.727s61.732s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown87.4964.2663.757s61.653s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe6.884.023.712s2.377s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown86.1262.8262.134s61.068s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown85.4162.8362.242s60.842s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown88.2162.9362.425s61.272s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown89.7464.3363.813s61.198s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.231.611.350s0.363s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown101.6162.9662.445s57.178s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe2.801.471.218s0.167s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown84.8664.6661.921s57.643s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown92.9763.6063.080s61.257s