Tool CPAchecker 1.1-svn
Limits timelimit: 900 s, memlimit: 15000 MB
OS Linux 2.6.35-32-generic x86_64
System CPU: Intel(R) Core(TM) i7-2600K CPU @ 3.40GHz with 4 cores, frequency: 3401 MHz; RAM: 16375440 kB
Test Impact (Original) Impact with FC (Original) Impact (Framework) Impact with FC (Framework)
Options -setprop statistics.memory=false
-noout
-heap 12000m
-impact-algorithm-sbe
-setprop impact.useForcedCovering=false		 -setprop statistics.memory=false
-noout
-heap 12000m
-impact-algorithm-sbe
-setprop impact.useForcedCovering=true		 -setprop cpa.conditions.global.time.wall=-1
-setprop statistics.memory=false
-noout
-heap 12000m
-impact-refiner-sbe		 -setprop cpa.conditions.global.time.wall=-1
-setprop statistics.memory=false
-noout
-heap 12000m
-setprop cpa.forcedCovering=cpa.predicate.PredicateForcedCovering
-impact-refiner-sbe
test/programs/benchmarks/ status cputime walltime refinements status cputime walltime refinements status cputime walltime refinements status cputime walltime refinements
pthread/fib_bench_BUG.cil.c unknown - - - unknown - - - unknown - - - unknown - - -
pthread/fib_bench_longer_BUG.cil.c unknown - - - unknown - - - unknown - - - unknown - - -
pthread/queue_BUG.cil.c safe - - - safe - - - unknown - - - unknown - - -
pthread/reorder_5_BUG.cil.c safe - - - safe - - - unknown - - - unknown - - -
pthread/twostage_3_BUG.cil.c safe - - - safe - - - unknown - - - unknown - - -
pthread/fib_bench.cil.c unknown - - - unknown - - - unknown - - - unknown - - -
pthread/fib_bench_longer.cil.c unknown - - - unknown - - - unknown - - - unknown - - -
pthread/queue_ok.cil.c safe 1.40 0.88 3 safe 1.41 0.89 1 unknown - - - unknown - - -
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.c unsafe 753.80 739.62 8219 unsafe 20.75 17.96 161 timeout - - - unsafe 15.59 12.66 228
ntdrivers-simplified/floppy_simpl3_BUG.cil.c unsafe 149.64 145.88 3379 unsafe 15.32 13.16 61 unsafe 362.69 350.20 5938 unsafe 9.32 7.44 88
ntdrivers-simplified/floppy_simpl4_BUG.cil.c unsafe 172.30 168.48 3672 unsafe 13.50 11.30 74 timeout - - - unsafe 11.12 8.81 102
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.c unsafe 31.90 30.23 1378 unsafe 6.28 4.63 40 unsafe 58.33 54.80 1905 unsafe 7.05 5.22 64
ntdrivers-simplified/cdaudio_simpl1.cil.c safe 749.84 737.20 7758 safe 20.22 17.22 157 timeout - - - safe 23.30 20.72 244
ntdrivers-simplified/diskperf_simpl1.cil.c safe 653.21 637.88 5289 safe 21.92 19.11 92 timeout - - - safe 19.89 17.09 144
ntdrivers-simplified/floppy_simpl3.cil.c safe 94.49 91.81 2265 safe 12.07 9.88 53 timeout - - - safe 14.57 12.31 94
ntdrivers-simplified/floppy_simpl4.cil.c safe 110.61 107.52 2466 safe 12.68 10.23 66 timeout - - - safe 17.33 14.61 113
ntdrivers-simplified/kbfiltr_simpl1.cil.c safe 9.33 7.77 443 safe 4.81 3.21 32 safe 15.19 13.18 636 safe 3.90 2.49 33
ntdrivers-simplified/kbfiltr_simpl2.cil.c safe 23.83 22.09 1113 safe 5.67 3.94 37 safe 41.21 38.28 1439 safe 4.61 2.66 49
ntdrivers/cdaudio.BUG.i.cil.c timeout - - - unsafe 44.81 40.65 128 unsafe 16.41 14.30 40 unsafe 10.01 7.84 24
ntdrivers/diskperf.BUG.i.cil.c timeout - - - unsafe 46.33 43.04 95 unsafe 5.36 4.13 10 unsafe 3.93 2.68 6
ntdrivers/floppy.BUG.i.cil.c timeout - - - unsafe 63.36 60.02 136 unsafe 6.56 4.38 16 unsafe 4.70 3.13 8
ntdrivers/kbfiltr.BUG.i.cil.c timeout - - - unsafe 22.81 20.57 67 unsafe 212.18 209.65 875 unsafe 14.79 12.52 40
ntdrivers/parport.BUG.i.cil.c timeout - - - unsafe 94.88 90.43 158 unsafe 17.36 15.16 30 unsafe 6.20 4.32 7
ntdrivers/cdaudio.i.cil.c timeout - - - safe 43.52 39.41 121 timeout - - - safe 105.06 99.78 309
ntdrivers/diskperf.i.cil.c timeout - - - safe 50.54 47.40 94 timeout - - - safe 94.38 90.83 207
ntdrivers/floppy.i.cil.c timeout - - - safe 67.80 64.27 133 timeout - - - safe 143.08 139.19 278
ntdrivers/parport.i.cil.c timeout - - - safe 107.47 102.65 157 timeout - - - segmentation fault - - -
ssh-simplified/s3_clnt_1_BUG.cil.c timeout - - - unsafe 111.36 108.83 9 timeout - - - unsafe 52.24 49.86 14
ssh-simplified/s3_clnt_2_BUG.cil.c timeout - - - unsafe 46.97 44.76 9 timeout - - - unsafe 105.24 102.59 10
ssh-simplified/s3_clnt_3_BUG.cil.c timeout - - - unsafe 47.12 44.84 9 unsafe 11.82 9.59 382 unsafe 66.06 63.47 14
ssh-simplified/s3_clnt_4_BUG.cil.c timeout - - - unsafe 112.01 109.45 9 timeout - - - unsafe 80.79 78.09 12
ssh-simplified/s3_srvr_10_BUG.cil.c unsafe 4.43 3.19 260 unsafe 7.23 5.75 8 unsafe 2.36 1.45 36 unsafe 2.25 1.30 4
ssh-simplified/s3_srvr_11_BUG.cil.c timeout - - - out of native memory - - - timeout - - - unsafe 117.96 114.98 7
ssh-simplified/s3_srvr_12_BUG.cil.c timeout - - - out of native memory - - - timeout - - - unsafe 31.64 29.44 19
ssh-simplified/s3_srvr_13_BUG.cil.c timeout - - - out of native memory - - - timeout - - - unsafe 6.05 4.64 13
ssh-simplified/s3_srvr_14_BUG.cil.c timeout - - - unsafe 101.03 99.10 11 timeout - - - unsafe 6.11 4.35 9
ssh-simplified/s3_srvr_1_BUG.cil.c timeout - - - unsafe 100.07 97.91 8 timeout - - - out of native memory - - -
ssh-simplified/s3_srvr_2_BUG.cil.c timeout - - - unsafe 124.65 122.12 9 timeout - - - out of native memory - - -
ssh-simplified/s3_srvr_6_BUG.cil.c unsafe 1.62 0.98 5 unsafe 2.55 1.54 5 timeout - - - out of native memory - - -
ssh-simplified/s3_clnt_1.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh-simplified/s3_clnt_2.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh-simplified/s3_clnt_3.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh-simplified/s3_clnt_4.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh-simplified/s3_srvr_1.cil.c timeout - - - safe 52.46 50.52 3 timeout - - - safe 155.73 153.36 10
ssh-simplified/s3_srvr_1a.cil.c timeout - - - safe 13.35 12.00 2 timeout - - - safe 7.42 5.76 9
ssh-simplified/s3_srvr_1b.cil.c safe 3.42 2.19 217 safe 2.83 1.90 2 safe 14.17 11.83 1792 safe 2.11 1.37 7
ssh-simplified/s3_srvr_2.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh-simplified/s3_srvr_3.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh-simplified/s3_srvr_4.cil.c timeout - - - safe 49.35 47.30 4 timeout - - - safe 116.51 114.14 9
ssh-simplified/s3_srvr_6.cil.c timeout - - - segmentation fault - - - timeout - - - out of native memory - - -
ssh-simplified/s3_srvr_7.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh-simplified/s3_srvr_8.cil.c timeout - - - segmentation fault - - - timeout - - - out of native memory - - -
ssh/s3_clnt.blast.01.BUG.i.cil.c timeout - - - unsafe 20.26 18.10 5 timeout - - - unsafe 133.15 130.58 11
ssh/s3_clnt.blast.02.BUG.i.cil.c unsafe 256.76 255.59 672 unsafe 45.94 43.80 4 timeout - - - unsafe 11.43 9.52 3
ssh/s3_clnt.blast.03.BUG.i.cil.c unsafe 166.60 165.16 593 unsafe 44.11 42.09 4 timeout - - - unsafe 11.14 9.56 3
ssh/s3_clnt.blast.04.BUG.i.cil.c unsafe 204.24 202.88 626 unsafe 44.42 42.42 4 timeout - - - unsafe 10.30 8.49 3
ssh/s3_srvr.blast.01.BUG.i.cil.c unsafe 459.59 458.11 1211 unsafe 69.24 66.88 5 unsafe 70.37 66.14 777 unsafe 14.74 12.85 4
ssh/s3_srvr.blast.02.BUG.i.cil.c unsafe 706.18 704.96 1521 unsafe 73.06 70.90 4 unsafe 67.56 64.11 694 unsafe 45.04 43.10 3
ssh/s3_srvr.blast.03.BUG.i.cil.c unsafe 629.62 628.49 1462 unsafe 73.75 71.41 4 timeout - - - unsafe 145.24 142.34 4
ssh/s3_srvr.blast.04.BUG.i.cil.c unsafe 819.72 819.09 1554 unsafe 67.22 64.88 4 unsafe 146.18 139.69 1219 unsafe 45.88 43.94 3
ssh/s3_srvr.blast.06.BUG.i.cil.c timeout - - - unsafe 45.81 43.64 4 timeout - - - out of native memory - - -
ssh/s3_srvr.blast.07.BUG.i.cil.c timeout - - - out of native memory - - - timeout - - - segmentation fault - - -
ssh/s3_srvr.blast.08.BUG.i.cil.c timeout - - - unsafe 41.50 39.38 4 timeout - - - unsafe 140.51 137.96 4
ssh/s3_srvr.blast.09.BUG.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.10.BUG.i.cil.c timeout - - - unsafe 41.80 39.83 4 timeout - - - unsafe 115.15 112.92 3
ssh/s3_srvr.blast.11.BUG.i.cil.c timeout - - - unsafe 174.02 170.98 5 timeout - - - unsafe 14.54 12.57 4
ssh/s3_srvr.blast.12.BUG.i.cil.c timeout - - - unsafe 44.72 42.60 4 out of native memory - - - out of native memory - - -
ssh/s3_srvr.blast.13.BUG.i.cil.c timeout - - - unsafe 349.02 343.90 5 timeout - - - out of native memory - - -
ssh/s3_srvr.blast.14.BUG.i.cil.c timeout - - - unsafe 45.13 42.94 4 timeout - - - out of native memory - - -
ssh/s3_srvr.blast.15.BUG.i.cil.c timeout - - - unsafe 42.05 40.03 4 timeout - - - unsafe 118.22 115.98 3
ssh/s3_srvr.blast.16.BUG.i.cil.c timeout - - - unsafe 44.91 42.84 4 timeout - - - out of native memory - - -
ssh/s3_clnt.blast.01.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_clnt.blast.02.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_clnt.blast.03.i.cil.c timeout - - - segmentation fault - - - timeout - - - out of native memory - - -
ssh/s3_clnt.blast.04.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.01.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.02.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.06.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.07.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.08.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.09.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.10.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.11.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.12.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.13.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.14.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.15.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ssh/s3_srvr.blast.16.i.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
locks/test_locks_14.BUG.c unsafe 1.44 0.82 2 unsafe 1.37 0.86 2 unsafe 2.47 1.65 43 unsafe 2.17 1.49 30
locks/test_locks_15.BUG.c unsafe 1.26 0.79 2 unsafe 1.44 0.83 2 unsafe 3.14 2.41 73 unsafe 3.25 2.24 47
locks/test_locks_10.c timeout - - - out of native memory - - - out of native memory - - - out of native memory - - -
locks/test_locks_11.c timeout - - - out of native memory - - - out of native memory - - - out of native memory - - -
locks/test_locks_12.c timeout - - - out of native memory - - - out of native memory - - - out of native memory - - -
locks/test_locks_13.c timeout - - - out of native memory - - - out of native memory - - - out of native memory - - -
locks/test_locks_14.c timeout - - - out of native memory - - - out of native memory - - - out of native memory - - -
locks/test_locks_15.c timeout - - - out of native memory - - - out of native memory - - - out of native memory - - -
locks/test_locks_5.c safe 4.66 3.61 228 safe 4.84 3.70 5 safe 4.50 3.01 224 safe 4.91 3.51 31
locks/test_locks_6.c safe 21.13 19.83 549 safe 12.93 11.73 6 safe 10.56 9.28 544 safe 13.40 11.67 63
locks/test_locks_7.c safe 260.91 260.28 1286 safe 49.55 47.87 7 safe 38.75 37.20 1280 safe 48.62 46.58 127
locks/test_locks_8.c timeout - - - safe 204.29 201.40 8 safe 177.97 174.53 2944 safe 201.09 198.18 255
locks/test_locks_9.c timeout - - - out of native memory - - - out of native memory - - - out of native memory - - -
heap-manipulation/bubble_sort_linux_BUG.cil.c timeout - - - timeout - - - unsafe 1.81 1.12 2 unsafe 1.80 1.11 2
heap-manipulation/dll_of_dll_BUG.cil.c unsafe 41.31 39.92 128 unsafe 5.12 4.25 33 unsafe 1.40 0.88 1 unsafe 1.39 0.89 1
heap-manipulation/merge_sort_BUG.cil.c unsafe 10.63 9.24 56 unsafe 17.06 15.77 23 unsafe 1.69 0.98 4 unsafe 1.80 1.05 4
heap-manipulation/sll_to_dll_rev_BUG.cil.c timeout - - - unsafe 27.70 26.19 27 timeout - - - timeout - - -
heap-manipulation/bubble_sort_linux.cil.c timeout - - - unsafe - - - unsafe - - - unsafe - - -
heap-manipulation/dll_of_dll.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
heap-manipulation/merge_sort.cil.c unsafe - - - unsafe - - - safe 1.54 0.97 4 safe 1.41 0.90 1
heap-manipulation/sll_to_dll_rev.cil.c timeout - - - unsafe - - - timeout - - - timeout - - -
list-properties/alternating_list.cil.c unsafe - - - unsafe - - - unsafe - - - safe 1.46 0.92 2
list-properties/list.cil.c unsafe - - - safe 2.98 2.10 3 unsafe - - - safe 1.55 1.00 1
list-properties/list_flag.cil.c unsafe - - - safe 2.52 1.81 3 unsafe - - - safe 1.48 0.92 1
list-properties/simple.cil.c unsafe - - - unsafe - - - unsafe - - - safe 1.70 0.99 1
list-properties/simple_built_from_end.cil.c unsafe - - - unsafe - - - unsafe - - - safe 1.43 0.91 2
list-properties/splice.cil.c unsafe - - - unsafe - - - unsafe - - - exception - - -
systemc/kundu1_BUG.cil.c timeout - - - unsafe 44.74 41.88 27 timeout - - - unsafe 12.26 10.53 23
systemc/kundu2_BUG.cil.c timeout - - - unsafe 125.89 121.25 58 timeout - - - unsafe 38.18 35.29 238
systemc/pc_sfifo_1_BUG.cil.c unsafe 2.27 1.44 49 unsafe 1.80 1.19 7 unsafe 4.12 2.61 62 unsafe 3.69 2.44 10
systemc/pc_sfifo_2_BUG.cil.c unsafe 2.76 1.62 47 unsafe 2.49 1.57 7 unsafe 16.42 13.81 689 unsafe 6.79 4.66 77
systemc/pipeline_BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.01.BUG.cil.c unsafe 60.90 57.88 1001 unsafe 12.41 10.43 8 unsafe 392.56 380.90 8792 unsafe 41.17 38.54 164
systemc/token_ring.02.BUG.cil.c timeout - - - unsafe 52.42 49.67 12 timeout - - - unsafe 71.57 67.67 90
systemc/token_ring.03.BUG.cil.c timeout - - - unsafe 243.12 236.25 14 timeout - - - unsafe 349.94 339.52 188
systemc/token_ring.04.BUG.cil.c timeout - - - segmentation fault - - - timeout - - - out of native memory - - -
systemc/token_ring.05.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.06.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.07.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.08.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.09.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.10.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.11.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.12.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.13.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.14.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.15.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/toy1_BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/toy2_BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/transmitter.01.BUG.cil.c unsafe 3.74 2.55 122 unsafe 9.59 7.75 6 unsafe 100.13 96.77 2639 unsafe 10.60 8.18 44
systemc/transmitter.02.BUG.cil.c unsafe 76.80 74.24 1359 unsafe 66.74 63.62 9 timeout - - - unsafe 136.56 131.94 271
systemc/transmitter.03.BUG.cil.c unsafe 692.28 686.07 4028 unsafe 250.04 242.59 11 timeout - - - unsafe 229.63 222.31 116
systemc/transmitter.04.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/transmitter.05.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/transmitter.06.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/transmitter.07.BUG.cil.c timeout - - - out of native memory - - - timeout - - - segmentation fault - - -
systemc/transmitter.08.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/transmitter.09.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/transmitter.10.BUG.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/transmitter.11.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/transmitter.12.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/transmitter.13.BUG.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/transmitter.15.BUG.cil.c unsafe 252.38 245.86 569 segmentation fault - - - timeout - - - timeout - - -
systemc/transmitter.16.BUG.cil.c unsafe 333.41 323.16 610 out of native memory - - - timeout - - - timeout - - -
systemc/bist_cell.cil.c timeout - - - safe 37.16 34.96 14 timeout - - - out of native memory - - -
systemc/kundu.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/mem_slave_tlm.1.cil.c timeout - - - safe 43.11 39.99 26 timeout - - - safe 57.92 55.13 135
systemc/mem_slave_tlm.2.cil.c timeout - - - safe 154.08 148.63 28 timeout - - - safe 146.40 143.72 121
systemc/mem_slave_tlm.3.cil.c timeout - - - safe 416.88 408.08 30 timeout - - - safe 333.89 330.83 132
systemc/mem_slave_tlm.4.cil.c timeout - - - timeout - - - timeout - - - safe 658.76 653.74 139
systemc/mem_slave_tlm.5.cil.c timeout - - - timeout - - - timeout - - - timeout - - -
systemc/pc_sfifo_1.cil.c safe 487.89 482.60 3648 safe 6.03 4.50 8 safe 52.29 49.15 1054 safe 5.56 4.18 11
systemc/pc_sfifo_2.cil.c timeout - - - safe 9.78 7.98 12 safe 438.13 424.83 6028 safe 23.02 20.35 61
systemc/pc_sfifo_3.cil.c timeout - - - safe 42.19 39.06 10 timeout - - - safe 140.50 137.69 17
systemc/pipeline.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.01.cil.c timeout - - - safe 11.05 9.08 3 timeout - - - safe 16.73 14.86 10
systemc/token_ring.02.cil.c timeout - - - safe 42.57 39.89 7 timeout - - - safe 121.26 117.70 94
systemc/token_ring.03.cil.c timeout - - - safe 312.14 304.07 9 timeout - - - out of native memory - - -
systemc/token_ring.04.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.05.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.06.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.07.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.08.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.09.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.10.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
systemc/token_ring.11.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.12.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/token_ring.13.cil.c timeout - - - out of native memory - - - timeout - - - timeout - - -
systemc/toy.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ldv-regression/1_3.c-unsafe.cil.c unsafe 1.20 0.76 3 unsafe 1.30 0.82 3 unsafe 1.24 0.79 1 unsafe 1.25 0.80 1
ldv-regression/alt_test.c-unsafe.cil.c unsafe 1.32 0.84 7 unsafe 1.42 0.93 4 unsafe 1.27 0.81 1 unsafe 1.44 0.83 1
ldv-regression/callfpointer.c-unsafe.cil.c safe - - - safe - - - safe - - - safe - - -
ldv-regression/fo_test.c-unsafe.cil.c unsafe 1.37 0.80 2 unsafe 1.38 0.81 2 unsafe 1.27 0.82 2 unsafe 1.51 0.88 2
ldv-regression/mutex_lock_int.c-unsafe.cil.c unsafe 1.19 0.75 3 unsafe 1.22 0.76 3 unsafe 1.38 0.81 1 unsafe 1.39 0.81 1
ldv-regression/mutex_lock_struct.c-unsafe.cil.c unsafe 1.18 0.75 3 unsafe 1.30 0.81 3 unsafe 1.40 0.81 1 unsafe 1.40 0.81 1
ldv-regression/recursive_list.c-unsafe.cil.c unsafe 1.36 0.79 2 unsafe 1.28 0.82 2 unsafe 1.26 0.81 1 unsafe 1.26 0.81 1
ldv-regression/rule57_ebda_blast.c-unsafe.cil.c unsafe 1.43 0.84 5 unsafe 1.39 0.90 4 unsafe 1.30 0.83 3 unsafe 1.44 0.86 2
ldv-regression/rule60_list2.c-unsafe_1.cil.c unsafe 2.44 1.76 41 unsafe 3.59 2.38 10 unsafe 1.68 0.99 4 unsafe 1.79 1.07 4
ldv-regression/stateful_check-unsafe.cil.c unsafe 4.92 3.85 341 unsafe 5.82 4.48 14 unsafe 6.44 4.36 291 unsafe 4.64 3.34 8
ldv-regression/test_while_int.c-unsafe.cil.c unsafe 1.19 0.76 4 unsafe 1.40 0.83 4 unsafe 1.41 0.83 3 unsafe 1.51 0.89 3
ldv-regression/test_while_int.c-unsafe_1.cil.c unsafe 1.18 0.74 4 unsafe 1.22 0.78 3 unsafe 1.24 0.80 3 unsafe 1.30 0.82 3
ldv-regression/alias_of_return.c-safe.cil.c safe 1.17 0.73 1 safe 1.28 0.79 1 safe 1.39 0.81 1 safe 1.24 0.78 1
ldv-regression/alias_of_return.c-safe_1.cil.c safe 1.18 0.73 1 safe 1.33 0.76 1 safe 1.23 0.78 1 safe 1.23 0.78 1
ldv-regression/alias_of_return_2.c-safe.cil.c safe 1.18 0.74 2 safe 1.24 0.77 1 safe 1.39 0.81 2 safe 1.25 0.79 1
ldv-regression/alias_of_return_2.c-safe_1.cil.c safe 1.34 0.76 1 safe 1.22 0.77 1 safe 1.38 0.79 1 safe 1.23 0.78 1
ldv-regression/ex3_forlist.c-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/just_assert.c-safe.cil.c safe 1.16 0.73 0 safe 1.26 0.77 0 safe 1.37 0.79 0 safe 1.21 0.76 0
ldv-regression/mutex_lock_int.c-safe_1.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/mutex_lock_struct.c-safe_1.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/nested_structure-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/nested_structure.c-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/nested_structure_noptr-safe.cil.c safe 1.18 0.73 1 safe 1.32 0.75 1 safe 1.39 0.80 1 safe 1.23 0.78 1
ldv-regression/nested_structure_noptr.c-safe.cil.c safe 1.33 0.77 1 safe 1.24 0.76 1 safe 1.39 0.81 1 safe 1.24 0.78 1
ldv-regression/nested_structure_ptr-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/nested_structure_ptr.c-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/oomInt.c-safe.cil.c safe 1.18 0.74 2 safe 1.27 0.80 1 safe 1.40 0.81 2 safe 1.24 0.79 1
ldv-regression/oomInt.c-safe_1.cil.c safe 1.33 0.77 2 safe 1.31 0.76 1 safe 1.24 0.77 2 safe 1.25 0.79 2
ldv-regression/rule57_ebda_blast.c-safe_1.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/rule60_list.c-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/rule60_list2.c-safe.cil.c safe 2.37 1.63 36 safe 2.04 1.43 10 safe 2.24 1.51 24 safe 1.85 1.22 9
ldv-regression/sizeofparameters_test.c-safe.cil.c safe 1.16 0.73 1 safe 1.23 0.76 1 safe 1.23 0.77 1 safe 1.40 0.81 1
ldv-regression/structure_assignment.c-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/test_address.c-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/test_cut_trace.c-safe.cil.c safe 1.33 0.77 2 safe 1.32 0.77 2 safe 1.23 0.78 2 safe 1.23 0.78 2
ldv-regression/test_malloc-1-safe.cil.c safe 1.20 0.76 1 safe 1.31 0.81 1 safe 1.40 0.82 1 safe 1.26 0.79 1
ldv-regression/test_malloc-2-safe.cil.c safe 1.19 0.75 1 safe 1.34 0.78 1 safe 1.40 0.82 1 safe 1.24 0.80 1
ldv-regression/test_overflow.c-safe.cil.c safe 1.18 0.74 1 safe 1.22 0.77 1 safe 1.40 0.81 1 safe 1.39 0.82 1
ldv-regression/test_union.c-safe.cil.c safe 1.18 0.73 1 safe 1.27 0.78 1 safe 1.39 0.81 1 safe 1.24 0.78 1
ldv-regression/test_union.c-safe_1.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/test_union_cast-1-safe.cil.c safe 1.29 0.76 1 safe 1.34 0.79 1 safe 1.24 0.78 1 safe 1.39 0.81 1
ldv-regression/test_union_cast-2-safe.cil.c safe 1.18 0.74 1 safe 1.21 0.77 1 safe 1.26 0.80 1 safe 1.25 0.79 1
ldv-regression/test_union_cast.c-safe.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-regression/test_union_cast.c-safe_1.cil.c safe 1.34 0.78 1 safe 1.29 0.79 1 safe 1.39 0.81 1 safe 1.40 0.82 1
ldv-regression/volatile_alias.c-safe.cil.c safe 1.17 0.74 1 safe 1.22 0.76 1 safe 1.39 0.81 1 safe 1.40 0.87 1
ldv-regression/volatile_alias.c-safe_1.cil.c safe 1.17 0.73 1 safe 1.31 0.76 1 safe 1.35 0.80 1 safe 1.22 0.78 1
ddv-machzwd/ddv_machzwd_all_BUG.cil.c safe - - - safe - - - safe - - - safe - - -
ddv-machzwd/ddv_machzwd_inw_BUG.cil.c safe - - - safe - - - safe - - - safe - - -
ddv-machzwd/ddv_machzwd_outb_BUG.cil.c safe - - - safe - - - safe - - - safe - - -
ddv-machzwd/ddv_machzwd_inb.cil.c safe 2.32 1.26 0 safe 2.70 1.34 0 safe 2.62 1.42 0 safe 2.63 1.42 0
ddv-machzwd/ddv_machzwd_inb_p.cil.c safe 2.68 1.32 0 safe 2.55 1.40 0 safe 2.65 1.42 0 safe 2.60 1.42 0
ddv-machzwd/ddv_machzwd_inl.cil.c safe 2.32 1.27 0 safe 2.54 1.40 0 safe 2.61 1.41 0 safe 2.60 1.41 0
ddv-machzwd/ddv_machzwd_inl_p.cil.c safe 2.31 1.25 0 safe 2.55 1.39 0 safe 3.06 1.47 0 safe 2.64 1.42 0
ddv-machzwd/ddv_machzwd_inw_p.cil.c safe 2.71 1.47 0 safe 2.70 1.33 0 safe 2.63 1.41 0 safe 2.66 1.42 0
ddv-machzwd/ddv_machzwd_outb_p.cil.c safe 2.32 1.27 0 safe 2.70 1.34 0 safe 3.14 1.50 0 safe 2.63 1.42 0
ddv-machzwd/ddv_machzwd_outl.cil.c safe 2.30 1.25 0 safe 2.69 1.34 0 safe 3.01 1.45 0 safe 3.02 1.45 0
ddv-machzwd/ddv_machzwd_outl_p.cil.c safe 2.68 1.32 0 safe 2.69 1.33 0 safe 2.79 1.51 0 safe 2.67 1.42 0
ddv-machzwd/ddv_machzwd_outw_p.cil.c safe 2.33 1.26 0 safe 2.69 1.33 0 safe 2.96 1.58 0 safe 2.63 1.42 0
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.c safe 2.32 1.27 0 safe 2.63 1.43 0 safe 2.61 1.41 0 safe 2.61 1.42 0
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-unsafe.cil.out.i.pp.cil.c unsafe 114.45 109.99 58 unsafe 14.97 9.84 5 unsafe 10.54 4.74 1 unsafe 11.17 4.52 1
ldv-drivers/module_get_put-drivers-block-loop.ko-unsafe.cil.out.i.pp.cil.c timeout - - - unsafe 718.22 678.16 119 timeout - - - unsafe 174.91 169.92 10
ldv-drivers/module_get_put-drivers-block-pktcdvd.ko-unsafe.cil.out.i.pp.cil.c timeout - - - segmentation fault - - - timeout - - - unsafe 232.41 226.16 5
ldv-drivers/module_get_put-drivers-isdn-gigaset-gigaset.ko-unsafe.cil.out.i.pp.cil.c timeout - - - unsafe 187.09 178.51 24 unsafe 20.96 16.71 14 unsafe 14.83 7.47 4
ldv-drivers/module_get_put-drivers-isdn-mISDN-mISDN_core.ko-unsafe.cil.out.i.pp.cil.c unsafe 563.76 558.89 402 unsafe 43.18 37.17 5 unsafe 15.55 11.11 9 unsafe 10.12 6.06 3
ldv-drivers/module_get_put-drivers-net-ppp_generic.ko-unsafe.cil.out.i.pp.cil.c timeout - - - out of native memory - - - timeout - - - unsafe 392.17 383.71 12
ldv-drivers/module_get_put-drivers-net-wan-farsync.ko-unsafe.cil.out.iunsafe.cil.out.i.pp.cil.c timeout - - - out of native memory - - - timeout - - - segmentation fault - - -
ldv-drivers/module_get_put-drivers-tty-synclink_gt.ko-unsafe.cil.out.i.pp.cil.c timeout - - - exception - - - timeout - - - timeout - - -
ldv-drivers/module_get_put-drivers-usb-core-usbcore.ko-unsafe.cil.out.i.pp.cil.c unsafe 442.94 438.01 118 unsafe 41.95 35.14 10 unsafe 114.66 109.35 20 unsafe 35.85 30.20 7
ldv-drivers/usb_urb-drivers-hid-usbhid-usbmouse.ko-unsafe.cil.out.i.pp.cil.c unsafe 701.00 697.58 502 unsafe 83.64 69.65 12 timeout - - - unsafe 42.81 40.16 16
ldv-drivers/usb_urb-drivers-input-misc-keyspan_remote.ko-unsafe.cil.out.i.pp.cil.c timeout - - - timeout - - - timeout - - - unsafe 216.95 211.59 18
ldv-drivers/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko-unsafe.cil.out.i.pp.cil.c timeout - - - unsafe 60.89 55.92 15 unsafe 250.97 244.96 138 unsafe 137.93 131.70 64
ldv-drivers/usb_urb-drivers-net-can-usb-ems_usb.ko-unsafe.cil.out.i.pp.cil.c unsafe 863.33 858.44 454 out of native memory - - - unsafe 67.81 65.55 55 unsafe 23.78 20.96 10
ldv-drivers/usb_urb-drivers-net-usb-catc.ko-unsafe.cil.out.i.pp.cil.c timeout - - - out of native memory - - - timeout - - - unsafe 304.57 300.64 40
ldv-drivers/usb_urb-drivers-staging-lirc-lirc_imon.ko-unsafe.cil.out.i.pp.cil.c timeout - - - unsafe 42.84 38.74 10 timeout - - - unsafe 33.38 30.05 15
ldv-drivers/usb_urb-drivers-usb-misc-iowarrior.ko-unsafe.cil.out.i.pp.cil.c timeout - - - unsafe 215.24 175.46 16 timeout - - - unsafe 140.61 137.38 38
ldv-drivers/module_get_put-drivers-atm-eni.ko-safe.cil.out.i.pp.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ldv-drivers/module_get_put-drivers-block-drbd-drbd.ko-safe.cil.out.i.pp.cil.c timeout - - - segmentation fault - - - timeout - - - safe 54.97 46.60 1
ldv-drivers/module_get_put-drivers-block-paride-pt.ko-safe.cil.out.i.pp.cil.c timeout - - - segmentation fault - - - timeout - - - out of native memory - - -
ldv-drivers/module_get_put-drivers-bluetooth-btmrvl.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 5.83 2.89 1 timeout - - - safe 5.54 3.00 1
ldv-drivers/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.c unknown - - - unknown - - - unknown - - - unknown - - -
ldv-drivers/module_get_put-drivers-gpu-drm-i915-i915.ko-safe.cil.out.i.pp.cil.c safe 819.68 796.50 198 safe 16.35 9.15 1 timeout - - - safe 19.51 11.46 1
ldv-drivers/module_get_put-drivers-hid-hid-magicmouse.ko-safe.cil.out.i.pp.cil.c unknown - - - unknown - - - timeout - - - unknown - - -
ldv-drivers/module_get_put-drivers-hwmon-it87.ko-safe.cil.out.i.pp.cil.c timeout - - - segmentation fault - - - timeout - - - safe 7.87 4.75 1
ldv-drivers/module_get_put-drivers-net-atl1c-atl1c.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 16.18 11.31 1 timeout - - - safe 46.86 34.96 1
ldv-drivers/module_get_put-drivers-net-pppox.ko-safe.cil.out.i.pp.cil.c safe 16.45 15.19 17 safe 5.18 3.91 3 safe 544.30 542.70 292 safe 5.69 4.47 3
ldv-drivers/module_get_put-drivers-net-sis900.ko-safe.cil.out.i.pp.cil.c timeout - - - segmentation fault - - - timeout - - - out of native memory - - -
ldv-drivers/module_get_put-drivers-scsi-megaraid.ko-safe.cil.out.i.pp.cil.c timeout - - - timeout - - - timeout - - - out of native memory - - -
ldv-drivers/module_get_put-drivers-staging-et131x-et131x.ko-safe.cil.out.i.pp.cil.c exception - - - exception - - - timeout - - - timeout - - -
ldv-drivers/module_get_put-drivers-video-aty-aty128fb.ko-safe.cil.out.i.pp.cil.c timeout - - - segmentation fault - - - timeout - - - timeout - - -
ldv-drivers/usb_urb-drivers-input-tablet-kbtab.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 17.20 14.68 10 timeout - - - safe 24.00 21.70 15
ldv-drivers/usb_urb-drivers-media-video-c-qcam.ko-safe.cil.out.i.pp.cil.c timeout - - - out of native memory - - - timeout - - - out of native memory - - -
ldv-drivers/usb_urb-drivers-media-video-msp3400.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 32.42 26.82 2 timeout - - - safe 254.52 218.84 2
ldv-drivers/usb_urb-drivers-misc-c2port-core.ko-safe.cil.out.i.pp.cil.c exception - - - exception - - - timeout - - - safe 833.65 826.94 2
ldv-drivers/usb_urb-drivers-mtd-sm_ftl.ko-safe.cil.out.i.pp.cil.c unknown - - - unknown - - - unknown - - - unknown - - -
ldv-drivers/usb_urb-drivers-scsi-dc395x.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 21.65 14.96 2 timeout - - - safe 30.18 17.97 2
ldv-drivers/usb_urb-drivers-usb-serial-ir-usb.ko-safe.cil.out.i.pp.cil.c unsafe - - - unsafe - - - unsafe - - - unsafe - - -
ldv-drivers/usb_urb-drivers-usb-serial-whiteheat.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 29.44 25.37 6 timeout - - - safe 92.29 87.37 9
ldv-drivers/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko-safe.cil.out.i.pp.cil.c timeout - - - timeout - - - unsafe - - - unsafe - - -
ldv-drivers/usb_urb-drivers-vhost-vhost_net.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 281.11 274.17 2 timeout - - - safe 21.32 13.58 2
ldv-drivers/usb_urb-drivers-video-arkfb.ko-safe.cil.out.i.pp.cil.c timeout - - - safe 10.21 7.24 2 timeout - - - safe 16.69 11.64 2
total files 277 11847.79 11656.65 60013 277 6847.04 6435.50 2776 277 3397.09 3236.84 41059 277 8013.76 7626.14 5074
correct results 86 11847.79 11656.65 60013 142 6847.04 6435.50 2776 80 3397.09 3236.84 41059 146 8013.76 7626.14 5074
false negatives 7 0 0 0 7 0 0 0 4 0 0 0 4 0 0 0
false positives 22 0 0 0 22 0 0 0 23 0 0 0 17 0 0 0
score (277 files, max score: 435) 59 142 60 172