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.1341
Test setintegration-predicateAnalysis-abm
branch-r5692
Options-noout
-predicateAnalysis-abm
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2202725.952014.851619.0981210.452
correct results1781812.401197.211142.984771.422
false negatives00000
false positives1937.6620.8116.2122.785
score (220 files, max score: 356)242
pthread/fib_bench_BUG.cil.cunknown1.270.760.510s0.029s
pthread/fib_bench_longer_BUG.cil.cunknown1.300.760.509s0.029s
pthread/queue_BUG.cil.cunknown1.540.870.622s0.087s
pthread/reorder_5_BUG.cil.cunknown1.680.930.686s0.110s
pthread/twostage_3_BUG.cil.cunknown1.941.000.743s0.126s
pthread/fib_bench.cil.cunknown1.560.850.602s0.025s
pthread/fib_bench_longer.cil.cunknown1.580.880.630s0.025s
pthread/queue_ok.cil.cunknown1.700.980.731s0.095s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe18.0111.8611.450s8.224s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe7.783.923.573s1.793s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe9.294.594.265s2.389s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe5.552.692.336s1.130s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe13.987.827.446s4.875s
ntdrivers-simplified/diskperf_simpl1.cil.csafe10.155.815.483s3.531s
ntdrivers-simplified/floppy_simpl3.cil.csafe10.425.505.123s3.072s
ntdrivers-simplified/floppy_simpl4.cil.csafe11.846.275.920s3.718s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe3.131.741.464s0.581s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe4.522.352.045s0.987s
ntdrivers/cdaudio.BUG.i.cil.cunsafe15.468.307.904s4.587s
ntdrivers/diskperf.BUG.i.cil.cunsafe11.626.115.650s3.087s
ntdrivers/floppy.BUG.i.cil.cunsafe12.736.826.391s3.112s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe7.283.553.223s1.330s
ntdrivers/parport.BUG.i.cil.cunsafe21.2613.4712.996s7.264s
ntdrivers/cdaudio.i.cil.csafe17.609.889.521s5.971s
ntdrivers/diskperf.i.cil.csafe12.356.816.481s3.816s
ntdrivers/floppy.i.cil.csafe15.278.908.534s4.454s
ntdrivers/parport.i.cil.csafe29.9220.7620.255s12.462s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.303.162.822s1.710s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.122.872.588s1.380s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe6.103.312.972s1.563s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.642.592.305s1.100s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe19.3914.9414.555s11.406s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe61.9355.2054.689s49.357s
ssh-simplified/s3_srvr_12_BUG.cil.ctimeout119.65115.42--
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe18.0113.2712.921s9.896s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.072.271.982s0.912s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.732.562.279s1.220s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.061.030.780s0.060s
ssh-simplified/s3_clnt_1.cil.csafe10.026.746.467s4.431s
ssh-simplified/s3_clnt_2.cil.csafe8.715.375.078s3.182s
ssh-simplified/s3_clnt_3.cil.csafe8.194.904.592s2.886s
ssh-simplified/s3_clnt_4.cil.csafe12.108.368.091s5.276s
ssh-simplified/s3_srvr_1a.cil.csafe5.082.612.279s1.502s
ssh-simplified/s3_srvr_1b.cil.csafe2.101.200.913s0.231s
ssh-simplified/s3_srvr_1.cil.cout of memory67.0362.36--
ssh-simplified/s3_srvr_3.cil.csafe24.7519.5019.055s13.807s
ssh-simplified/s3_srvr_4.cil.csafe10.126.235.856s4.494s
ssh-simplified/s3_srvr_6.cil.ctimeout119.59114.47--
ssh-simplified/s3_srvr_7.cil.cunknown67.1463.6763.368s62.287s
ssh-simplified/s3_srvr_8.cil.csafe16.4911.7911.459s8.487s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe7.023.523.223s1.685s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.822.582.318s1.024s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.662.632.361s1.096s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.742.892.634s1.389s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe6.202.932.636s1.365s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe5.162.812.517s1.204s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe5.042.592.270s1.107s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.472.382.072s0.990s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe5.853.182.900s1.453s
ssh/s3_srvr.blast.07.BUG.i.cil.cunknown68.7864.7764.463s63.124s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe25.2219.8519.451s17.417s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe36.7830.5130.084s27.359s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.282.752.489s1.260s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe11.257.457.142s5.581s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe29.2523.8223.414s21.439s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.543.323.041s1.788s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe19.2914.1813.796s11.823s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe6.403.202.942s1.662s
ssh/s3_clnt.blast.01.i.cil.csafe8.394.994.708s3.116s
ssh/s3_clnt.blast.03.i.cil.csafe13.079.519.215s6.444s
ssh/s3_clnt.blast.04.i.cil.csafe11.757.697.385s4.353s
ssh/s3_srvr.blast.01.i.cil.csafe33.3028.0627.643s23.518s
ssh/s3_srvr.blast.06.i.cil.csafe25.7720.1219.678s14.632s
ssh/s3_srvr.blast.07.i.cil.cunknown67.2463.6563.322s61.743s
ssh/s3_srvr.blast.08.i.cil.csafe24.8019.9419.538s15.867s
ssh/s3_srvr.blast.09.i.cil.cunknown65.9661.2160.883s58.778s
ssh/s3_srvr.blast.10.i.cil.csafe13.168.357.987s6.179s
ssh/s3_srvr.blast.12.i.cil.csafe14.159.609.187s7.403s
ssh/s3_srvr.blast.13.i.cil.cunknown65.8861.9861.654s59.930s
ssh/s3_srvr.blast.14.i.cil.csafe39.2633.0032.500s26.234s
ssh/s3_srvr.blast.15.i.cil.csafe18.6113.2712.842s7.199s
ssh/s3_srvr.blast.16.i.cil.csafe46.0540.7540.268s27.921s
locks/test_locks_14.BUG.cunsafe2.641.591.338s0.525s
locks/test_locks_15.BUG.cunsafe2.781.591.329s0.484s
locks/test_locks_11.csafe2.261.290.986s0.303s
locks/test_locks_12.csafe2.371.401.153s0.387s
locks/test_locks_13.csafe2.421.461.178s0.422s
locks/test_locks_14.csafe2.811.611.322s0.454s
locks/test_locks_15.csafe2.611.501.229s0.524s
locks/test_locks_5.csafe1.781.100.829s0.120s
locks/test_locks_6.csafe1.881.130.837s0.141s
locks/test_locks_7.csafe1.901.030.779s0.151s
locks/test_locks_8.csafe1.931.050.807s0.186s
locks/test_locks_9.csafe1.991.130.880s0.214s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe2.481.271.010s0.200s
heap-manipulation/dll_of_dll_BUG.cil.cunknown2.051.050.795s0.114s
heap-manipulation/merge_sort_BUG.cil.cunsafe2.161.200.952s0.204s
heap-manipulation/bubble_sort_linux.cil.cunsafe2.561.311.056s0.211s
heap-manipulation/dll_of_dll.cil.cunknown2.041.100.851s0.142s
heap-manipulation/merge_sort.cil.csafe1.961.010.761s0.087s
heap-manipulation/sll_to_dll_rev.cil.cunknown14.1312.0411.752s9.036s
list-properties/alternating_list.cil.csafe1.991.070.802s0.157s
list-properties/list.cil.csafe2.241.260.973s0.279s
list-properties/list_flag.cil.csafe2.061.050.771s0.165s
list-properties/simple.cil.cunsafe2.001.020.780s0.156s
list-properties/simple_built_from_end.cil.cunsafe2.041.040.788s0.145s
list-properties/splice.cil.cunsafe3.892.472.210s0.935s
systemc/token_ring.01.BUG.cil.cunsafe3.031.741.491s0.567s
systemc/token_ring.02.BUG.cil.cunsafe5.902.862.562s1.274s
systemc/token_ring.03.BUG.cil.cunsafe8.344.894.487s2.461s
systemc/transmitter.01.BUG.cil.cunsafe2.951.741.393s0.473s
systemc/transmitter.02.BUG.cil.cunsafe4.272.562.269s0.862s
systemc/transmitter.03.BUG.cil.cunsafe4.842.562.263s0.920s
systemc/transmitter.04.BUG.cil.cunsafe5.342.632.368s1.054s
systemc/bist_cell.cil.csafe19.8716.5816.304s13.971s
systemc/kundu.cil.csafe67.3761.4361.111s57.203s
systemc/mem_slave_tlm.1.cil.cexception43.7039.26--
systemc/mem_slave_tlm.2.cil.csafe69.0764.5764.277s62.132s
systemc/pc_sfifo_1.cil.csafe5.282.852.615s1.376s
systemc/pc_sfifo_2.cil.csafe7.804.764.502s2.753s
systemc/pc_sfifo_3.cil.csafe7.063.993.736s2.145s
systemc/token_ring.01.cil.csafe8.364.854.608s2.576s
systemc/token_ring.04.cil.cunknown65.8861.1060.774s58.043s
systemc/toy.cil.csafe68.6960.9760.668s57.425s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.580.880.618s0.028s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.500.860.617s0.057s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.390.800.569s0.016s
ldv-regression/fo_test.c-unsafe.cil.cunsafe1.560.890.657s0.059s
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.490.930.604s0.028s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.620.930.685s0.022s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.701.030.757s0.055s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.400.820.585s0.035s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe2.291.401.155s0.261s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.471.501.212s0.471s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.470.850.587s0.044s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.440.840.599s0.043s
ldv-regression/alias_of_return.c-safe.cil.csafe1.440.860.622s0.031s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.440.880.619s0.043s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.570.890.629s0.048s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.470.860.588s0.027s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.141.150.918s0.246s
ldv-regression/just_assert.c-safe.cil.csafe1.300.720.495s0.009s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.470.790.553s0.019s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.380.810.563s0.019s
ldv-regression/nested_structure-safe.cil.cunsafe1.440.840.604s0.051s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.380.780.541s0.021s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.380.780.554s0.019s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.340.780.538s0.018s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.690.970.721s0.102s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.380.800.566s0.025s
ldv-regression/oomInt.c-safe.cil.csafe1.360.800.545s0.032s
ldv-regression/oomInt.c-safe_1.cil.csafe1.350.780.551s0.032s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.520.890.656s0.056s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.350.790.549s0.024s
ldv-regression/rule60_list2.c-safe.cil.csafe1.871.120.867s0.220s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.390.800.551s0.024s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.340.790.554s0.018s
ldv-regression/test_address.c-safe.cil.cunsafe1.340.780.541s0.021s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.380.800.548s0.019s
ldv-regression/test_malloc-1-safe.cil.csafe1.360.770.545s0.033s
ldv-regression/test_malloc-2-safe.cil.csafe1.410.790.553s0.030s
ldv-regression/test_overflow.c-safe.cil.csafe1.410.820.573s0.030s
ldv-regression/test_union.c-safe.cil.csafe1.330.760.534s0.018s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.350.760.532s0.016s
ldv-regression/test_union_cast-1-safe.cil.csafe1.580.890.639s0.016s
ldv-regression/test_union_cast-2-safe.cil.csafe1.350.760.532s0.025s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.360.780.550s0.025s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.370.800.541s0.019s
ldv-regression/volatile_alias.c-safe.cil.csafe1.320.750.520s0.018s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.320.760.519s0.017s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.561.921.651s0.357s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.601.891.639s0.356s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.581.901.646s0.359s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.341.691.443s0.395s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.211.641.385s0.365s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.201.621.383s0.351s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.371.731.489s0.401s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.361.771.525s0.480s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.231.641.398s0.356s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.461.761.510s0.430s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.781.881.592s0.409s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.791.821.556s0.421s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.621.801.541s0.362s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.246.205.918s0.498s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe11.746.235.888s2.251s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunsafe14.947.687.309s3.548s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe12.314.654.376s0.545s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunsafe16.959.118.782s3.372s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe9.604.414.107s1.686s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunsafe19.5411.3711.042s4.474s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe7.553.082.805s0.212s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe18.857.397.120s1.360s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe11.856.666.337s2.876s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunsafe45.3929.5229.119s11.850s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.473.092.806s0.595s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe17.4510.5510.206s3.547s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.442.672.395s0.885s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.csafe17.319.338.995s6.830s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.csafe14.156.556.236s1.233s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.csafe41.4522.7122.262s13.664s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe11.396.055.721s3.660s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.csafe14.047.517.144s4.015s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.csafe17.148.237.910s1.068s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.462.261.997s0.720s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csafe6.523.272.979s1.362s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.csafe18.9710.059.692s6.789s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe4.202.181.914s0.669s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.csafe15.467.847.433s5.081s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown89.7965.4665.010s61.802s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.csafe26.7512.5612.221s8.626s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe8.404.624.253s2.036s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.csafe5.722.932.638s1.022s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.csafe8.013.653.363s1.568s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csafe4.322.191.914s0.701s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csafe18.718.478.125s4.610s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.332.141.883s0.488s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csafe21.6112.9712.635s5.633s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.701.901.647s0.207s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csafe12.185.975.658s3.173s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csafe6.222.922.641s1.108s