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.1041
Test setintegration-predicateAnalysis
branch-r5643
Options-noout
-predicateAnalysis
-heap 2000m
-setprop cpa.conditions.global.time.wall=1min
test/programs/benchmarks/statuscputimewalltimetotalcpa time
total files2233453.882599.702161.2951786.166
correct results1611017.82669.95616.423355.560
false negatives00000
false positives1935.3819.3814.7082.428
score (223 files, max score: 361)212
pthread/fib_bench_BUG.cil.cunknown1.510.860.623s0.025s
pthread/fib_bench_longer_BUG.cil.cunknown1.710.910.664s0.024s
pthread/queue_BUG.cil.cunknown1.821.010.768s0.098s
pthread/reorder_5_BUG.cil.cunknown1.821.080.815s0.118s
pthread/twostage_3_BUG.cil.cunknown1.901.070.814s0.121s
pthread/fib_bench.cil.cunknown1.640.910.666s0.029s
pthread/fib_bench_longer.cil.cunknown1.720.890.639s0.025s
pthread/queue_ok.cil.cunknown1.871.050.791s0.083s
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.cunsafe5.663.433.142s1.862s
ntdrivers-simplified/floppy_simpl3_BUG.cil.cunsafe3.642.121.795s0.743s
ntdrivers-simplified/floppy_simpl4_BUG.cil.cunsafe4.232.292.015s0.963s
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.cunsafe3.241.711.450s0.582s
ntdrivers-simplified/cdaudio_simpl1.cil.csafe5.192.922.629s1.656s
ntdrivers-simplified/diskperf_simpl1.cil.csafe3.962.332.056s1.387s
ntdrivers-simplified/floppy_simpl3.cil.csafe3.521.891.615s0.830s
ntdrivers-simplified/floppy_simpl4.cil.csafe4.122.211.912s1.013s
ntdrivers-simplified/kbfiltr_simpl1.cil.csafe2.441.250.967s0.328s
ntdrivers-simplified/kbfiltr_simpl2.cil.csafe3.001.541.267s0.538s
ntdrivers/cdaudio.BUG.i.cil.cunsafe9.765.134.768s2.525s
ntdrivers/diskperf.BUG.i.cil.cunsafe5.703.292.990s1.554s
ntdrivers/floppy.BUG.i.cil.cunsafe10.416.185.842s3.777s
ntdrivers/kbfiltr.BUG.i.cil.cunsafe5.012.802.462s0.959s
ntdrivers/parport.BUG.i.cil.cunknown86.1569.7863.841s62.293s
ntdrivers/cdaudio.i.cil.csafe9.204.734.427s2.610s
ntdrivers/diskperf.i.cil.csafe5.412.992.684s1.613s
ntdrivers/floppy.i.cil.csafe12.618.057.705s5.284s
ntdrivers/parport.i.cil.cunknown85.9469.7763.111s61.770s
ssh-simplified/s3_clnt_1_BUG.cil.cunsafe4.012.201.925s0.890s
ssh-simplified/s3_clnt_2_BUG.cil.cunsafe4.062.441.969s0.895s
ssh-simplified/s3_clnt_3_BUG.cil.cunsafe4.082.352.052s0.856s
ssh-simplified/s3_clnt_4_BUG.cil.cunsafe4.312.652.332s1.051s
ssh-simplified/s3_srvr_10_BUG.cil.cunsafe2.561.301.042s0.276s
ssh-simplified/s3_srvr_11_BUG.cil.cunsafe5.983.182.878s1.545s
ssh-simplified/s3_srvr_12_BUG.cil.cunsafe10.447.487.142s5.458s
ssh-simplified/s3_srvr_14_BUG.cil.cunsafe3.051.561.295s0.454s
ssh-simplified/s3_srvr_1_BUG.cil.cunsafe4.132.221.920s0.762s
ssh-simplified/s3_srvr_2_BUG.cil.cunsafe3.811.991.677s0.703s
ssh-simplified/s3_srvr_6_BUG.cil.cunsafe2.161.140.859s0.055s
ssh-simplified/s3_clnt_1.cil.csafe8.495.385.064s3.026s
ssh-simplified/s3_clnt_2.cil.csafe8.435.425.071s3.306s
ssh-simplified/s3_clnt_3.cil.csafe9.796.606.274s3.074s
ssh-simplified/s3_clnt_4.cil.csafe9.486.145.772s3.421s
ssh-simplified/s3_srvr_1a.cil.csafe4.002.271.904s1.192s
ssh-simplified/s3_srvr_1b.cil.csafe2.001.110.832s0.130s
ssh-simplified/s3_srvr_1.cil.csafe37.4132.9632.477s24.240s
ssh-simplified/s3_srvr_3.cil.csafe25.1720.8520.373s13.418s
ssh-simplified/s3_srvr_4.cil.csafe14.3010.209.735s7.986s
ssh-simplified/s3_srvr_6.cil.csafe15.6711.4911.038s9.081s
ssh-simplified/s3_srvr_7.cil.csafe21.4317.4517.012s15.208s
ssh-simplified/s3_srvr_8.cil.csafe12.158.357.932s5.349s
ssh/s3_clnt.blast.01.BUG.i.cil.cunsafe4.822.822.430s1.119s
ssh/s3_clnt.blast.02.BUG.i.cil.cunsafe4.872.512.166s0.959s
ssh/s3_clnt.blast.03.BUG.i.cil.cunsafe4.642.662.224s0.976s
ssh/s3_clnt.blast.04.BUG.i.cil.cunsafe4.332.281.951s0.841s
ssh/s3_srvr.blast.01.BUG.i.cil.cunsafe4.582.332.034s0.857s
ssh/s3_srvr.blast.02.BUG.i.cil.cunsafe4.082.171.863s0.774s
ssh/s3_srvr.blast.03.BUG.i.cil.cunsafe3.771.971.696s0.741s
ssh/s3_srvr.blast.04.BUG.i.cil.cunsafe3.801.981.680s0.677s
ssh/s3_srvr.blast.06.BUG.i.cil.cunsafe4.892.682.368s1.027s
ssh/s3_srvr.blast.07.BUG.i.cil.cunsafe7.504.694.337s2.816s
ssh/s3_srvr.blast.08.BUG.i.cil.cunsafe8.004.754.410s2.466s
ssh/s3_srvr.blast.10.BUG.i.cil.cunsafe7.914.323.969s2.011s
ssh/s3_srvr.blast.11.BUG.i.cil.cunsafe5.833.212.873s1.679s
ssh/s3_srvr.blast.12.BUG.i.cil.cunsafe5.502.862.552s1.164s
ssh/s3_srvr.blast.13.BUG.i.cil.cunsafe10.277.547.249s5.963s
ssh/s3_srvr.blast.14.BUG.i.cil.cunsafe5.112.992.682s1.357s
ssh/s3_srvr.blast.15.BUG.i.cil.cunsafe7.374.283.958s1.994s
ssh/s3_srvr.blast.16.BUG.i.cil.cunsafe5.262.862.480s1.161s
ssh/s3_clnt.blast.01.i.cil.csafe9.096.125.765s3.756s
ssh/s3_clnt.blast.03.i.cil.csafe7.565.565.226s3.105s
ssh/s3_clnt.blast.04.i.cil.csafe10.238.568.216s5.793s
ssh/s3_srvr.blast.01.i.cil.csafe12.4810.919.521s5.917s
ssh/s3_srvr.blast.06.i.cil.csafe13.8410.229.792s8.212s
ssh/s3_srvr.blast.07.i.cil.csafe12.428.938.507s7.191s
ssh/s3_srvr.blast.08.i.cil.cout of memory81.9478.29--
ssh/s3_srvr.blast.09.i.cil.csafe11.247.577.179s5.209s
ssh/s3_srvr.blast.10.i.cil.csafe46.8842.8942.407s13.384s
ssh/s3_srvr.blast.12.i.cil.csafe35.4031.2630.774s14.208s
ssh/s3_srvr.blast.13.i.cil.csafe20.4216.0015.507s13.270s
ssh/s3_srvr.blast.14.i.cil.csafe31.2126.8526.350s20.392s
ssh/s3_srvr.blast.15.i.cil.csafe11.287.597.145s4.948s
ssh/s3_srvr.blast.16.i.cil.csafe14.4410.439.989s6.799s
locks/test_locks_14.BUG.cunsafe1.630.910.675s0.095s
locks/test_locks_15.BUG.cunsafe1.460.870.637s0.101s
locks/test_locks_10.csafe1.380.790.566s0.073s
locks/test_locks_11.csafe1.360.790.564s0.076s
locks/test_locks_12.csafe1.390.810.580s0.084s
locks/test_locks_13.csafe1.460.850.624s0.098s
locks/test_locks_14.csafe1.400.820.592s0.096s
locks/test_locks_15.csafe1.400.820.599s0.103s
locks/test_locks_5.csafe1.280.750.514s0.038s
locks/test_locks_6.csafe1.320.750.525s0.044s
locks/test_locks_7.csafe1.320.760.533s0.051s
locks/test_locks_8.csafe1.340.760.537s0.057s
locks/test_locks_9.csafe1.340.770.546s0.064s
heap-manipulation/bubble_sort_linux_BUG.cil.cunsafe1.901.090.854s0.153s
heap-manipulation/dll_of_dll_BUG.cil.cunknown1.520.860.621s0.076s
heap-manipulation/merge_sort_BUG.cil.cunsafe1.660.950.723s0.134s
heap-manipulation/sll_to_dll_rev_BUG.cil.cunknown63.1160.8160.545s56.864s
heap-manipulation/bubble_sort_linux.cil.cunsafe1.901.080.853s0.157s
heap-manipulation/dll_of_dll.cil.cunknown1.530.860.626s0.075s
heap-manipulation/merge_sort.cil.csafe1.460.840.621s0.067s
heap-manipulation/sll_to_dll_rev.cil.cunknown63.5261.7761.499s55.880s
list-properties/alternating_list.cil.csafe1.510.870.633s0.127s
list-properties/list.cil.csafe1.570.910.681s0.167s
list-properties/list_flag.cil.csafe1.580.900.665s0.147s
list-properties/simple.cil.cunsafe1.530.880.652s0.124s
list-properties/simple_built_from_end.cil.cunsafe1.480.870.641s0.104s
list-properties/splice.cil.cunsafe3.101.961.707s0.832s
systemc/token_ring.01.BUG.cil.cunsafe2.871.541.268s0.519s
systemc/token_ring.02.BUG.cil.cunsafe4.142.211.927s1.154s
systemc/token_ring.03.BUG.cil.cunsafe6.543.353.025s2.179s
systemc/transmitter.01.BUG.cil.cunsafe1.921.100.842s0.255s
systemc/transmitter.02.BUG.cil.cunsafe2.401.361.114s0.483s
systemc/transmitter.03.BUG.cil.cunsafe3.872.021.767s1.050s
systemc/transmitter.04.BUG.cil.cunsafe7.463.973.652s2.700s
systemc/bist_cell.cil.csafe2.071.200.939s0.347s
systemc/kundu.cil.csafe13.7010.489.998s8.642s
systemc/mem_slave_tlm.1.cil.cout of memory46.9143.18--
systemc/mem_slave_tlm.2.cil.cout of memory47.9244.18--
systemc/mem_slave_tlm.4.cil.csegmentation fault55.7550.75--
systemc/pc_sfifo_1.cil.csafe3.952.081.813s1.170s
systemc/pc_sfifo_2.cil.csafe4.392.372.103s1.351s
systemc/pc_sfifo_3.cil.csafe1.881.070.811s0.277s
systemc/token_ring.01.cil.csafe3.942.051.734s1.046s
systemc/token_ring.04.cil.cout of memory70.6058.08--
systemc/toy.cil.cout of memory65.1160.62--
ldv-regression/1_3.c-unsafe.cil.cunsafe1.410.790.556s0.022s
ldv-regression/alt_test.c-unsafe.cil.cunsafe1.380.790.559s0.040s
ldv-regression/callfpointer.c-unsafe.cil.cunsafe1.360.780.548s0.013s
ldv-regression/fo_test.c-unsafe.cil.cunknown1.090.64--
ldv-regression/mutex_lock_int.c-unsafe.cil.cunsafe1.510.820.571s0.014s
ldv-regression/mutex_lock_struct.c-unsafe.cil.cunsafe1.630.910.654s0.015s
ldv-regression/recursive_list.c-unsafe.cil.cunsafe1.600.810.566s0.031s
ldv-regression/rule57_ebda_blast.c-unsafe.cil.cunsafe1.440.840.597s0.035s
ldv-regression/rule60_list2.c-unsafe_1.cil.cunsafe1.710.990.752s0.098s
ldv-regression/stateful_check-unsafe.cil.cunsafe1.911.090.840s0.206s
ldv-regression/test_while_int.c-unsafe.cil.cunsafe1.390.820.584s0.056s
ldv-regression/test_while_int.c-unsafe_1.cil.cunsafe1.370.770.540s0.030s
ldv-regression/alias_of_return.c-safe.cil.csafe1.390.820.598s0.023s
ldv-regression/alias_of_return.c-safe_1.cil.csafe1.290.730.494s0.014s
ldv-regression/alias_of_return_2.c-safe.cil.csafe1.450.820.568s0.019s
ldv-regression/alias_of_return_2.c-safe_1.cil.csafe1.400.800.566s0.015s
ldv-regression/ex3_forlist.c-safe.cil.cunsafe2.101.130.891s0.295s
ldv-regression/just_assert.c-safe.cil.csafe1.420.770.532s0.014s
ldv-regression/mutex_lock_int.c-safe_1.cil.cunsafe1.380.790.513s0.016s
ldv-regression/mutex_lock_struct.c-safe_1.cil.cunsafe1.460.830.587s0.015s
ldv-regression/nested_structure-safe.cil.cunsafe1.550.880.615s0.040s
ldv-regression/nested_structure.c-safe.cil.cunsafe1.420.800.571s0.018s
ldv-regression/nested_structure_noptr-safe.cil.csafe1.420.800.551s0.019s
ldv-regression/nested_structure_noptr.c-safe.cil.csafe1.530.870.614s0.015s
ldv-regression/nested_structure_ptr-safe.cil.cunsafe1.640.940.702s0.101s
ldv-regression/nested_structure_ptr.c-safe.cil.cunsafe1.440.780.534s0.021s
ldv-regression/oomInt.c-safe.cil.csafe1.400.750.516s0.018s
ldv-regression/oomInt.c-safe_1.cil.csafe1.460.760.516s0.016s
ldv-regression/rule57_ebda_blast.c-safe_1.cil.cunsafe1.360.800.572s0.041s
ldv-regression/rule60_list.c-safe.cil.cunsafe1.380.790.549s0.020s
ldv-regression/rule60_list2.c-safe.cil.csafe1.620.940.702s0.092s
ldv-regression/sizeofparameters_test.c-safe.cil.csafe1.460.750.528s0.015s
ldv-regression/structure_assignment.c-safe.cil.cunsafe1.340.740.516s0.016s
ldv-regression/test_address.c-safe.cil.cunsafe1.320.740.510s0.016s
ldv-regression/test_cut_trace.c-safe.cil.csafe1.440.810.569s0.019s
ldv-regression/test_malloc-1-safe.cil.csafe1.520.840.596s0.029s
ldv-regression/test_malloc-2-safe.cil.csafe1.480.790.550s0.026s
ldv-regression/test_overflow.c-safe.cil.csafe1.440.750.508s0.021s
ldv-regression/test_union.c-safe.cil.csafe1.430.800.563s0.014s
ldv-regression/test_union.c-safe_1.cil.cunsafe1.440.810.565s0.018s
ldv-regression/test_union_cast-1-safe.cil.csafe1.410.740.504s0.015s
ldv-regression/test_union_cast-2-safe.cil.csafe1.410.790.555s0.022s
ldv-regression/test_union_cast.c-safe.cil.cunsafe1.490.840.567s0.024s
ldv-regression/test_union_cast.c-safe_1.cil.csafe1.460.760.524s0.015s
ldv-regression/volatile_alias.c-safe.cil.csafe1.450.790.563s0.021s
ldv-regression/volatile_alias.c-safe_1.cil.csafe1.390.740.506s0.016s
ddv-machzwd/ddv_machzwd_all_BUG.cil.cunsafe3.661.951.664s0.514s
ddv-machzwd/ddv_machzwd_inw_BUG.cil.cunsafe3.621.891.642s0.516s
ddv-machzwd/ddv_machzwd_outb_BUG.cil.cunsafe3.791.921.655s0.497s
ddv-machzwd/ddv_machzwd_inb.cil.csafe3.751.871.593s0.532s
ddv-machzwd/ddv_machzwd_inb_p.cil.csafe3.681.811.522s0.455s
ddv-machzwd/ddv_machzwd_inl.cil.csafe3.711.791.513s0.451s
ddv-machzwd/ddv_machzwd_inl_p.cil.csafe3.681.751.497s0.549s
ddv-machzwd/ddv_machzwd_inw_p.cil.csafe3.491.681.401s0.458s
ddv-machzwd/ddv_machzwd_outb_p.cil.csafe3.511.671.407s0.448s
ddv-machzwd/ddv_machzwd_outl.cil.csafe3.591.711.435s0.472s
ddv-machzwd/ddv_machzwd_outl_p.cil.csafe3.441.681.437s0.435s
ddv-machzwd/ddv_machzwd_outw_p.cil.csafe3.721.811.499s0.450s
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.csafe3.671.801.552s0.534s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.cunsafe13.645.244.912s0.357s
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.cunsafe15.568.558.150s5.360s
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.cunknown83.4963.0062.445s60.466s
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.cunsafe13.038.366.201s1.861s
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.cunknown70.6065.0564.587s40.697s
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.cunsafe17.939.458.991s6.532s
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.cunknown83.3964.7064.245s61.501s
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.cunsafe9.563.483.209s0.290s
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.cunsafe20.607.657.343s0.541s
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.cunsafe13.868.908.448s5.849s
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.cunknown87.2064.1363.568s54.217s
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.cunsafe6.353.022.716s0.590s
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.cunsafe46.2536.3934.955s25.421s
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.cunsafe5.603.852.467s0.887s
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.cunknown82.6663.2462.646s60.876s
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.cunknown90.9669.1266.118s61.345s
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.cunknown81.4262.1361.392s60.057s
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.csafe9.165.114.777s3.235s
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.cunknown5.092.422.132s0.883s
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.cunknown92.5068.1367.595s61.840s
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.cunknown4.321.961.646s0.677s
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.cunknown80.5162.4962.024s59.981s
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.cunknown86.3168.6862.619s60.635s
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.csafe3.241.681.397s0.326s
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.cunknown82.3666.0462.472s60.901s
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.cunknown87.6364.6264.107s61.515s
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.cunknown84.2465.1664.661s62.263s
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.csafe8.834.724.387s2.668s
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.cunknown83.8466.8062.717s61.493s
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.cunknown85.1366.4162.931s61.199s
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.cunknown86.3964.2063.622s62.084s
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.cunknown88.5864.2163.718s60.390s
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.cunsafe3.801.771.496s0.403s
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.cunknown96.5363.8163.317s56.955s
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.cunsafe4.251.951.667s0.167s
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.cunknown80.7762.8862.325s59.800s
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.cunknown91.6863.8263.254s60.922s