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.1004
Test setintegration-predicateAnalysis
branch-r5639
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2232918.842152.651816.1391479.808
correct results137936.19655.16610.810390.220
false negatives25101.5050.7443.62916.433
false positives1428.4116.0412.0902.015
score (223 files, max score: 361)104
pthread/fib_bench_BUG.cil.csafe1.440.800.564s0.030s
pthread/fib_bench_longer_BUG.cil.csafe1.430.790.561s0.030s
pthread/queue_BUG.cil.csafe1.630.930.690s0.091s
pthread/reorder_5_BUG.cil.cunknown1.700.930.694s0.104s
pthread/twostage_3_BUG.cil.cunknown1.791.000.741s0.132s
pthread/fib_bench.cil.csafe1.480.820.572s0.029s
pthread/fib_bench_longer.cil.csafe1.440.800.565s0.029s
pthread/queue_ok.cil.csafe1.680.920.679s0.090s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.csafe6.323.583.199s2.356s
ntdrivers-simplified/floppy_simpl3_BUG.cil.csafe3.921.961.676s0.983s
ntdrivers-simplified/floppy_simpl4_BUG.cil.csafe4.792.532.244s1.478s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.csafe3.401.601.319s0.681s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe6.173.383.058s2.188s
ntdrivers-simplified/diskperf_simpl1.cil.csafe4.813.172.883s2.182s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.841.971.680s0.995s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.442.332.056s1.285s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.621.341.029s0.434s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.271.601.324s0.687s
ntdrivers/cdaudio.BUG.i.cil.csafe8.093.913.591s2.072s
ntdrivers/diskperf.BUG.i.cil.csafe5.763.423.125s2.050s
ntdrivers/floppy.BUG.i.cil.csafe7.383.853.544s2.091s
ntdrivers/kbfiltr.BUG.i.cil.csafe4.252.221.939s1.002s
ntdrivers/parport.BUG.i.cil.cunknown86.5569.7863.531s62.182s
ntdrivers/cdaudio.i.cil.csafe8.093.903.572s2.095s
ntdrivers/diskperf.i.cil.csafe5.573.102.803s1.820s
ntdrivers/floppy.i.cil.csafe7.664.063.751s2.366s
ntdrivers/parport.i.cil.cunknown85.9267.9261.844s60.482s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe5.162.772.457s1.327s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe5.162.872.564s1.393s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe5.102.752.433s1.304s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe5.763.212.880s1.609s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.981.681.398s0.530s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe7.584.243.893s2.188s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe7.744.454.093s2.294s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.401.771.489s0.670s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.842.522.233s1.217s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe4.012.041.739s0.893s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.111.070.834s0.059s
ssh-simplified/s3_clnt_1.cil.csafe16.5712.8012.413s9.921s
ssh-simplified/s3_clnt_2.cil.csafe25.3921.2620.849s17.588s
ssh-simplified/s3_clnt_3.cil.csafe13.219.118.723s5.316s
ssh-simplified/s3_clnt_4.cil.csafe12.728.908.490s5.559s
ssh-simplified/s3_srvr_1a.cil.csafe4.682.592.248s1.539s
ssh-simplified/s3_srvr_1b.cil.csafe2.101.210.917s0.235s
ssh-simplified/s3_srvr_1.cil.csafe28.4423.5322.977s17.274s
ssh-simplified/s3_srvr_3.cil.csafe17.7913.1712.604s8.741s
ssh-simplified/s3_srvr_4.cil.csafe18.6514.2713.696s9.793s
ssh-simplified/s3_srvr_6.cil.csafe21.8117.4116.783s13.647s
ssh-simplified/s3_srvr_7.cil.cout of memory77.1072.65--
ssh-simplified/s3_srvr_8.cil.csafe14.449.919.393s6.937s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe6.133.443.085s1.737s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.572.462.177s1.181s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.752.572.260s1.157s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe5.543.122.787s1.593s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe5.783.102.782s1.552s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.482.261.962s0.961s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe4.392.282.002s1.027s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe4.662.352.074s1.111s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe7.503.923.598s2.002s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe5.982.892.588s1.455s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe8.515.244.893s3.144s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe8.925.555.204s2.710s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe6.303.272.946s1.668s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe7.073.993.650s2.175s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe6.754.033.699s2.372s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe6.943.683.361s1.882s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe8.544.834.457s2.583s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe7.043.683.364s1.917s
ssh/s3_clnt.blast.01.i.cil.csafe16.5512.8112.458s10.771s
ssh/s3_clnt.blast.03.i.cil.csafe10.076.426.085s3.701s
ssh/s3_clnt.blast.04.i.cil.csafe10.226.886.525s4.623s
ssh/s3_srvr.blast.01.i.cil.csafe28.4023.4122.848s14.427s
ssh/s3_srvr.blast.06.i.cil.csafe55.3249.9949.368s30.077s
ssh/s3_srvr.blast.07.i.cil.cunknown66.1061.3660.845s57.276s
ssh/s3_srvr.blast.08.i.cil.csafe16.2711.3810.833s7.241s
ssh/s3_srvr.blast.09.i.cil.cunknown71.4761.7060.852s58.111s
ssh/s3_srvr.blast.10.i.cil.csafe15.4610.8310.306s7.354s
ssh/s3_srvr.blast.12.i.cil.csafe37.1731.5430.917s28.179s
ssh/s3_srvr.blast.13.i.cil.csafe52.3246.4945.924s43.982s
ssh/s3_srvr.blast.14.i.cil.csafe48.6143.6043.013s37.683s
ssh/s3_srvr.blast.15.i.cil.csafe65.4159.7359.111s27.957s
ssh/s3_srvr.blast.16.i.cil.cunknown66.8361.4160.806s41.834s
locks/test_locks_14.BUG.cunsafe1.881.130.831s0.177s
locks/test_locks_15.BUG.cunsafe2.041.170.886s0.183s
locks/test_locks_10.csafe1.791.000.746s0.129s
locks/test_locks_11.csafe1.740.970.710s0.137s
locks/test_locks_12.csafe1.640.920.671s0.136s
locks/test_locks_13.csafe1.751.040.781s0.151s
locks/test_locks_14.csafe1.821.060.785s0.175s
locks/test_locks_15.csafe2.011.200.885s0.184s
locks/test_locks_5.csafe1.711.050.774s0.088s
locks/test_locks_6.csafe1.720.970.715s0.075s
locks/test_locks_7.csafe1.700.960.709s0.085s
locks/test_locks_8.csafe1.790.970.720s0.098s
locks/test_locks_9.csafe1.821.050.773s0.107s
heap-manipulation/bubble_sort_linux_BUG.cil.csegmentation fault2.351.33--
heap-manipulation/dll_of_dll_BUG.cil.csafe1.961.070.804s0.097s
heap-manipulation/merge_sort_BUG.cil.csafe1.760.940.697s0.087s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown65.6762.7362.462s58.109s
heap-manipulation/bubble_sort_linux.cil.csegmentation fault2.591.35--
heap-manipulation/dll_of_dll.cil.csafe2.011.110.854s0.132s
heap-manipulation/merge_sort.cil.csafe1.921.080.817s0.097s
heap-manipulation/sll_to_dll_rev.cil.cunknown65.1261.6661.333s54.989s
list-properties/alternating_list.cil.csafe1.981.310.974s0.198s
list-properties/list.cil.csafe2.061.230.889s0.254s
list-properties/list_flag.cil.csafe2.141.170.882s0.229s
list-properties/simple.cil.cunsafe2.081.210.931s0.200s
list-properties/simple_built_from_end.cil.cunsafe2.001.120.829s0.147s
list-properties/splice.cil.cunsafe3.522.111.803s0.698s
systemc/token_ring.01.BUG.cil.csafe1.931.100.803s0.138s
systemc/token_ring.02.BUG.cil.csafe1.921.120.818s0.136s
systemc/token_ring.03.BUG.cil.csafe2.101.210.912s0.180s
systemc/transmitter.01.BUG.cil.csafe1.901.100.798s0.131s
systemc/transmitter.02.BUG.cil.csafe2.781.561.262s0.485s
systemc/transmitter.03.BUG.cil.csafe2.891.491.196s0.488s
systemc/transmitter.04.BUG.cil.csafe3.431.801.524s0.631s
systemc/bist_cell.cil.csafe2.341.381.063s0.273s
systemc/kundu.cil.csafe1.861.100.814s0.126s
systemc/mem_slave_tlm.1.cil.csafe3.211.931.558s0.442s
systemc/mem_slave_tlm.2.cil.csafe3.011.671.322s0.341s
systemc/mem_slave_tlm.4.cil.csafe2.941.521.237s0.380s
systemc/pc_sfifo_1.cil.csafe1.911.100.844s0.188s
systemc/pc_sfifo_2.cil.csafe1.921.190.901s0.153s
systemc/pc_sfifo_3.cil.csafe2.151.240.899s0.155s
systemc/token_ring.01.cil.csafe1.901.090.814s0.104s
systemc/token_ring.04.cil.csafe2.211.280.998s0.220s
systemc/toy.cil.csafe1.981.150.844s0.144s
ldv-regression/1_3.c-unsafe.cil.cunsafe1.790.990.722s0.034s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.610.950.687s0.055s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.700.860.605s0.017s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.410.82--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.680.950.680s0.034s
ldv-regression/mutex_lock_struct.c-unsafe.cil.csafe1.660.900.657s0.026s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.791.050.751s0.044s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.csafe1.721.020.753s0.075s
ldv-regression/rule60_list2.c-unsafe_1.cil.csafe1.871.020.765s0.118s
ldv-regression/stateful_check-unsafe.cil.cunsafe2.481.411.130s0.397s
ldv-regression/test_while_int.c-unsafe.cil.csegmentation fault1.740.93--
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.731.000.697s0.047s
ldv-regression/alias_of_return.c-safe.cil.csafe1.640.870.636s0.027s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.750.950.702s0.024s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.660.940.676s0.035s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.580.890.633s0.026s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.911.601.300s0.582s
ldv-regression/just_assert.c-safe.cil.csafe1.560.870.567s0.016s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.690.950.694s0.031s
ldv-regression/mutex_lock_struct.c-safe_1.cil.csafe1.690.940.668s0.031s
ldv-regression/nested_structure-safe.cil.cunsafe1.831.000.739s0.056s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.790.980.679s0.029s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.720.960.670s0.026s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.670.950.688s0.021s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.931.100.820s0.100s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.851.060.758s0.037s
ldv-regression/oomInt.c-safe.cil.csegmentation fault1.731.03--
ldv-regression/oomInt.c-safe_1.cil.csafe1.660.860.623s0.024s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.csafe1.801.000.737s0.085s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.720.980.718s0.027s
ldv-regression/rule60_list2.c-safe.cil.csafe1.841.070.794s0.116s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.750.950.666s0.025s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.780.980.736s0.029s
ldv-regression/test_address.c-safe.cil.cunsafe1.640.950.670s0.028s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.780.950.679s0.028s
ldv-regression/test_malloc-1-safe.cil.csafe1.761.000.654s0.041s
ldv-regression/test_malloc-2-safe.cil.csafe1.600.890.630s0.034s
ldv-regression/test_overflow.c-safe.cil.csafe1.660.890.638s0.031s
ldv-regression/test_union.c-safe.cil.csafe1.620.880.625s0.017s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.871.010.751s0.023s
ldv-regression/test_union_cast-1-safe.cil.csafe1.820.980.702s0.025s
ldv-regression/test_union_cast-2-safe.cil.csafe1.730.990.692s0.034s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.800.990.662s0.028s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.740.980.701s0.031s
ldv-regression/volatile_alias.c-safe.cil.csafe1.740.900.641s0.026s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.700.970.692s0.021s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe4.662.412.063s0.897s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe4.532.272.010s0.796s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe4.522.362.066s0.842s
ddv-machzwd/ddv_machzwd_inb.cil.csafe4.512.181.906s0.719s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe4.502.071.790s0.651s
ddv-machzwd/ddv_machzwd_inl.cil.csafe4.302.081.746s0.715s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe4.492.312.006s0.711s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe4.822.271.974s0.708s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe4.742.171.859s0.620s
ddv-machzwd/ddv_machzwd_outl.cil.csafe4.282.151.867s0.801s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe4.682.271.966s0.734s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe4.382.161.827s0.642s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe4.242.071.802s0.703s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.csafe13.985.545.245s0.462s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.csegmentation fault5.642.71--
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown86.2965.0764.410s62.160s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.csegmentation fault15.155.56--
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.csegmentation fault11.564.45--
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.csegmentation fault14.457.66--
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.csegmentation fault9.744.78--
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe9.443.893.542s0.393s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.csafe13.195.284.943s0.515s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.csegmentation fault4.162.07--
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.csegmentation fault5.272.27--
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.csegmentation fault6.332.94--
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.csegmentation fault4.952.46--
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.csegmentation fault5.502.55--
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown94.2270.8363.491s61.366s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown97.4676.0066.899s61.935s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown93.4570.0063.322s62.143s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csegmentation fault7.319.15--
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown6.445.665.340s2.764s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown90.7674.9372.470s61.326s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown5.372.532.194s0.917s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.csegmentation fault16.388.43--
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown86.7866.3763.238s61.134s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.801.791.510s0.510s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown92.2072.9561.951s60.103s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown89.0865.7665.193s62.070s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown85.2064.6363.996s61.128s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csegmentation fault3.521.67--
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown89.3168.7362.182s60.659s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown86.7067.6561.816s60.216s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.csegmentation fault23.7313.00--
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.csegmentation fault32.3815.89--
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.csafe4.742.121.839s0.789s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.csegmentation fault17.008.91--
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.csegmentation fault3.511.71--
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.csegmentation fault45.8026.80--
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.csegmentation fault19.039.99--