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-abm
branch-r5690
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202777.502068.171561.2951159.282
correct results1781809.901201.601145.953777.103
false negatives00000
false positives1937.0620.3015.6142.531
score (220 files, max score: 356)242
pthread/fib_bench_BUG.cil.cunknown1.310.760.510s0.027s
pthread/fib_bench_longer_BUG.cil.cunknown1.290.760.517s0.029s
pthread/queue_BUG.cil.cunknown1.560.900.642s0.098s
pthread/reorder_5_BUG.cil.cunknown1.881.080.818s0.144s
pthread/twostage_3_BUG.cil.cunknown1.941.030.794s0.149s
pthread/fib_bench.cil.cunknown1.550.890.648s0.024s
pthread/fib_bench_longer.cil.cunknown1.380.770.540s0.023s
pthread/queue_ok.cil.cunknown1.560.890.630s0.087s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe18.6112.2011.825s8.438s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.453.633.349s1.721s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe9.184.664.293s2.339s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.362.682.344s1.076s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.758.107.685s4.966s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.616.065.694s3.700s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.415.475.154s3.130s
ntdrivers-simplified/floppy_simpl4.cil.csafe12.316.836.473s4.148s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.191.851.519s0.545s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.592.432.082s0.965s
ntdrivers/cdaudio.BUG.i.cil.cunsafe15.518.137.736s4.450s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.506.255.919s3.114s
ntdrivers/floppy.BUG.i.cil.cunsafe12.747.036.550s3.171s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe8.044.093.764s1.600s
ntdrivers/parport.BUG.i.cil.cunsafe20.2712.4511.955s6.652s
ntdrivers/cdaudio.i.cil.csafe17.9510.4010.036s6.341s
ntdrivers/diskperf.i.cil.csafe12.526.906.547s4.019s
ntdrivers/floppy.i.cil.csafe15.579.308.930s4.773s
ntdrivers/parport.i.cil.csafe28.9219.6019.116s11.899s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.373.052.753s1.608s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.082.822.535s1.364s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.013.242.954s1.394s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.402.402.121s0.912s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe19.0014.5914.255s10.810s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe62.9656.3755.879s50.600s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.60114.49--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe17.6212.9712.630s10.204s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe3.842.111.865s0.838s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.832.622.352s1.309s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.301.180.892s0.075s
ssh-simplified/s3_clnt_1.cil.csafe10.787.346.949s4.663s
ssh-simplified/s3_clnt_2.cil.csafe9.095.565.243s3.193s
ssh-simplified/s3_clnt_3.cil.csafe8.324.924.575s2.910s
ssh-simplified/s3_clnt_4.cil.csafe12.478.518.168s5.186s
ssh-simplified/s3_srvr_1a.cil.csafe5.032.652.310s1.493s
ssh-simplified/s3_srvr_1b.cil.csafe2.121.240.939s0.238s
ssh-simplified/s3_srvr_1.cil.cunknown66.0561.57--
ssh-simplified/s3_srvr_3.cil.csafe25.2519.5019.089s14.089s
ssh-simplified/s3_srvr_4.cil.csafe10.176.446.117s4.598s
ssh-simplified/s3_srvr_6.cil.ctimeout119.62115.27--
ssh-simplified/s3_srvr_7.cil.cunknown65.6062.1461.847s60.787s
ssh-simplified/s3_srvr_8.cil.csafe16.3811.6711.291s8.526s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.883.723.421s1.836s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.812.552.261s1.031s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.722.572.286s1.075s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.502.842.558s1.287s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.212.572.299s1.087s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.542.382.109s0.961s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.632.452.186s1.038s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.802.552.278s1.075s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe6.163.072.815s1.454s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown68.8064.8764.537s63.063s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.8920.7120.309s18.115s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.1030.7630.379s27.500s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe4.722.472.208s1.084s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe10.936.866.552s5.188s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe29.0823.3522.946s20.911s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.643.533.244s1.938s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.2613.9913.598s11.611s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.133.353.065s1.761s
ssh/s3_clnt.blast.01.i.cil.csafe8.525.274.976s3.268s
ssh/s3_clnt.blast.03.i.cil.csafe13.479.929.588s6.641s
ssh/s3_clnt.blast.04.i.cil.csafe11.847.907.560s4.469s
ssh/s3_srvr.blast.01.i.cil.csafe32.6027.7527.374s23.368s
ssh/s3_srvr.blast.06.i.cil.csafe24.8819.6119.117s14.414s
ssh/s3_srvr.blast.07.i.cil.cunknown68.6664.8964.563s62.990s
ssh/s3_srvr.blast.08.i.cil.csafe25.4920.5020.006s15.938s
ssh/s3_srvr.blast.09.i.cil.cunknown66.6262.1061.722s59.885s
ssh/s3_srvr.blast.10.i.cil.csafe11.417.156.814s5.176s
ssh/s3_srvr.blast.12.i.cil.csafe14.119.619.212s7.342s
ssh/s3_srvr.blast.13.i.cil.cunknown65.6061.7061.391s59.669s
ssh/s3_srvr.blast.14.i.cil.csafe40.0334.0033.455s27.331s
ssh/s3_srvr.blast.15.i.cil.csafe18.4913.3012.895s7.171s
ssh/s3_srvr.blast.16.i.cil.csafe46.4740.7740.317s28.607s
locks/test_locks_14.BUG.cunsafe2.521.391.125s0.409s
locks/test_locks_15.BUG.cunsafe2.711.451.195s0.456s
locks/test_locks_11.csafe2.261.200.933s0.277s
locks/test_locks_12.csafe2.321.321.065s0.343s
locks/test_locks_13.csafe2.441.301.044s0.370s
locks/test_locks_14.csafe2.571.381.131s0.439s
locks/test_locks_15.csafe2.531.441.193s0.452s
locks/test_locks_5.csafe1.860.990.737s0.111s
locks/test_locks_6.csafe1.800.970.724s0.123s
locks/test_locks_7.csafe1.971.110.851s0.151s
locks/test_locks_8.csafe1.971.080.814s0.178s
locks/test_locks_9.csafe2.001.090.847s0.216s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.561.301.037s0.202s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.991.030.781s0.115s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.241.150.908s0.159s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.511.261.006s0.205s
heap-manipulation/dll_of_dll.cil.cunknown1.921.040.788s0.108s
heap-manipulation/merge_sort.cil.csafe1.921.040.795s0.085s
heap-manipulation/sll_to_dll_rev.cil.cunknown14.5712.6312.381s9.702s
list-properties/alternating_list.cil.csafe2.231.210.902s0.181s
list-properties/list.cil.csafe2.261.371.034s0.263s
list-properties/list_flag.cil.csafe2.101.160.890s0.197s
list-properties/simple.cil.cunsafe1.971.020.759s0.152s
list-properties/simple_built_from_end.cil.cunsafe1.911.000.761s0.140s
list-properties/splice.cil.cunsafe3.412.111.854s0.693s
systemc/token_ring.01.BUG.cil.cunsafe2.841.671.408s0.565s
systemc/token_ring.02.BUG.cil.cunsafe5.572.802.546s1.271s
systemc/token_ring.03.BUG.cil.cunsafe7.103.823.496s1.946s
systemc/transmitter.01.BUG.cil.cunsafe2.651.491.220s0.366s
systemc/transmitter.02.BUG.cil.cunsafe4.402.572.198s0.943s
systemc/transmitter.03.BUG.cil.cunsafe4.472.352.072s0.860s
systemc/transmitter.04.BUG.cil.cunsafe6.423.323.003s1.360s
systemc/bist_cell.cil.csafe19.6816.3116.036s13.960s
systemc/kundu.cil.csafe66.1462.7061.483s58.024s
systemc/mem_slave_tlm.1.cil.cexception42.7437.80--
systemc/mem_slave_tlm.2.cil.csafe69.1664.1363.812s61.434s
systemc/pc_sfifo_1.cil.csafe5.493.072.834s1.500s
systemc/pc_sfifo_2.cil.csafe8.825.254.992s3.037s
systemc/pc_sfifo_3.cil.csafe7.163.843.564s1.862s
systemc/token_ring.01.cil.csafe8.164.724.485s2.547s
systemc/token_ring.04.cil.ctimeout119.74112.34--
systemc/toy.cil.csafe66.7661.4661.158s59.311s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.671.030.753s0.033s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.500.910.631s0.055s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.390.790.551s0.015s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.740.970.737s0.062s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.330.770.531s0.018s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.400.810.547s0.017s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.370.810.578s0.040s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.380.820.586s0.039s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.061.180.921s0.218s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.261.321.069s0.423s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.420.840.590s0.043s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.380.810.568s0.036s
ldv-regression/alias_of_return.c-safe.cil.csafe1.500.830.591s0.030s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.370.800.539s0.018s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.330.820.581s0.037s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.340.780.535s0.019s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe1.981.160.897s0.223s
ldv-regression/just_assert.c-safe.cil.csafe1.320.740.504s0.010s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.380.800.558s0.020s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.340.780.530s0.018s
ldv-regression/nested_structure-safe.cil.cunsafe1.470.830.587s0.051s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.420.820.583s0.023s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.310.750.513s0.015s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.490.800.551s0.020s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.660.960.716s0.107s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.330.770.542s0.023s
ldv-regression/oomInt.c-safe.cil.csafe1.440.800.548s0.031s
ldv-regression/oomInt.c-safe_1.cil.csafe1.440.820.588s0.032s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.530.910.664s0.058s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.360.790.552s0.024s
ldv-regression/rule60_list2.c-safe.cil.csafe1.921.140.883s0.216s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.370.790.556s0.025s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.340.790.547s0.020s
ldv-regression/test_address.c-safe.cil.cunsafe1.380.800.545s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.340.770.538s0.020s
ldv-regression/test_malloc-1-safe.cil.csafe1.350.780.543s0.033s
ldv-regression/test_malloc-2-safe.cil.csafe1.400.800.548s0.029s
ldv-regression/test_overflow.c-safe.cil.csafe1.380.790.561s0.031s
ldv-regression/test_union.c-safe.cil.csafe1.360.760.533s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.390.790.548s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.360.770.532s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.340.780.547s0.026s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.460.820.587s0.022s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.350.800.551s0.024s
ldv-regression/volatile_alias.c-safe.cil.csafe1.340.770.527s0.018s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.400.800.561s0.016s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.661.941.687s0.380s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.052.071.825s0.355s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.611.871.617s0.349s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.691.921.661s0.472s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.861.951.681s0.467s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.921.911.625s0.431s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.941.911.622s0.369s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.561.731.471s0.370s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.421.921.623s0.412s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.541.811.570s0.440s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.501.851.588s0.454s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.661.901.649s0.440s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.661.851.572s0.386s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe15.086.786.515s0.435s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe11.606.215.899s2.230s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.947.627.263s3.418s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe12.464.714.459s0.537s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe15.678.137.819s2.660s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe9.184.564.260s1.737s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe19.3411.4011.063s4.384s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.483.152.855s0.214s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe21.378.077.780s1.368s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe12.536.706.399s2.861s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe41.9228.7128.308s11.578s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.923.152.887s0.632s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.0510.419.403s3.587s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.482.732.463s0.892s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe18.5110.4210.051s7.831s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe15.847.647.340s1.448s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe42.7122.9622.563s15.791s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.165.515.205s3.408s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe14.047.537.184s4.007s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe18.338.378.037s1.113s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.482.292.019s0.769s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe6.753.303.003s1.405s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe21.1611.5911.223s7.146s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.582.412.141s0.783s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe15.708.177.747s5.360s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown92.0865.0364.600s61.979s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe21.9410.9610.603s7.664s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe8.444.404.102s2.023s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.202.682.408s1.027s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.333.793.484s1.577s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.202.191.905s0.698s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe17.688.648.298s5.117s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.262.071.815s0.491s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe20.6612.3512.021s5.342s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.961.821.563s0.224s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe12.576.195.849s3.301s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe6.773.403.085s1.190s