Tool | BLAST 2.7.1 | CPAchecker 1.1.10-svcomp13 | ESBMC 1.20 | LLBMC SV-COMP-13 | Predator | UFO 2012-10-22 | ||||||||
Limits | timelimit: 900 s, memlimit: 15360 MB | |||||||||||||
System | CPU: Intel(R) Core(TM) i7-2600K CPU @ 3.40GHz with 4 cores, frequency: 3401 MHz; RAM: 16343684 kB | |||||||||||||
Date of run | 2012-11-25 00:16 | 2012-11-14 06:53 | 2012-11-14 08:27 | 2012-11-17 03:16 | 2012-12-04 06:32 | 2012-12-03 03:44 | 2012-12-14 13:52 | |||||||
Options | -alias bdd -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb |
-sv-comp13--explitp-pred -heap 12000m -disable-java-assertions |
-sv-comp13--combinations -heap 12000m -disable-java-assertions |
-t label -m32 |
--cex= |
|||||||||
../sv-benchmarks-trunk/loops/ | status | time | status | time | status | time | status | time | status | time | status | time | status | time |
array_unsafe.i | unsafe | 0.11 | unsafe | 1.6 | unsafe | 1.5 | unsafe | 0.47 | unsafe | 0.09 | unsafe | 0.07 | unsafe | 0.46 |
bubble_sort_unsafe.i | error | 0.09 | unsafe | 5.8 | unsafe | 5.8 | unsafe | 25 | unsafe | 0.05 | unsafe | 0.07 | unsafe | 0.88 |
count_up_down_unsafe.i | unsafe | 0.09 | unsafe | 1.4 | unsafe | 110 | unsafe | 0.15 | unsafe | 0.04 | unsafe | 0.05 | unsafe | 0.43 |
eureka_01_unsafe.i | timeout | 910 | safe | 5.1 | safe | 110 | unsafe | 450 | unsafe | 0.46 | error | 320 | unsafe | 0.98 |
for_bounded_loop1_unsafe.i | unsafe | 0.76 | unsafe | 2.1 | unsafe | 1.4 | unsafe | 0.18 | unsafe | 0.04 | unsafe | 0.04 | unsafe | 0.63 |
insertion_sort_unsafe.i | unsafe | 3.9 | unknown | 12 | unknown | 110 | unsafe | 450 | unsafe | 0.26 | error | 0.05 | unsafe | 0.81 |
invert_string_unsafe.i | unsafe | 0.90 | unknown | 1.4 | unknown | 110 | unsafe | 10 | unsafe | 0.11 | error | 0.06 | unsafe | 0.68 |
kundu_unsafe.i | unsafe | 200 | unsafe | 8.2 | unsafe | 1.9 | unsafe | 1.9 | unsafe | 0.60 | unsafe | 0.07 | unsafe | 6.0 |
linear_search_unsafe.i | unsafe | 0.09 | unknown | 1.4 | unsafe | 1.4 | safe | 450 | unsafe | 0.15 | error | 0.07 | unsafe | 0.52 |
list_unsafe.i | unsafe | 0.11 | unknown | 1.7 | unknown | 2.1 | unsafe | 0.33 | unsafe | 0.06 | unsafe | 0.05 | unsafe | 0.52 |
ludcmp_unsafe.i | unsafe | 1.4 | unsafe | 2.7 | unsafe | 1.7 | unsafe | 450 | unsafe | 0.03 | unsafe | 0.09 | unsafe | 0.41 |
matrix_unsafe.i | error | 0.07 | unknown | 1.4 | unknown | 110 | unsafe | 11 | unsafe | 0.04 | error | 0.05 | unknown | 0.06 |
nec11_unsafe.i | unsafe | 0.09 | unsafe | 1.3 | unsafe | 1.4 | unsafe | 0.17 | unsafe | 0.03 | unsafe | 0.05 | unsafe | 0.47 |
nec20_unsafe.i | unsafe | 0.22 | unsafe | 2.2 | unsafe | 2.1 | unsafe | 98 | unsafe | 0.04 | error | 0.05 | unsafe | 0.54 |
pc_sfifo_2_unsafe.i | unsafe | 0.10 | unsafe | 3.1 | unsafe | 110 | unsafe | 0.23 | unsafe | 0.04 | unsafe | 0.05 | unsafe | 1.2 |
s3_unsafe.i | unsafe | 16 | unsafe | 5.8 | unsafe | 7.5 | safe | 15 | unsafe | 93 | error | 0.06 | unsafe | 4.4 |
string_unsafe.i | unsafe | 1.3 | unknown | 1.5 | unknown | 100 | unsafe | 0.29 | unsafe | 0.07 | error | 0.05 | unsafe | 1.0 |
sum01_bug02_sum01_bug02_base.case_unsafe.i | unsafe | 9.7 | unknown | 1.3 | unknown | 110 | unsafe | 1.9 | unsafe | 0.10 | unsafe | 0.04 | unsafe | 0.63 |
sum01_bug02_unsafe.i | unsafe | 20 | unsafe | 2.4 | unknown | 100 | unsafe | 2.3 | unsafe | 0.15 | unsafe | 0.04 | unsafe | 0.61 |
sum01_unsafe.i | unsafe | 33 | unsafe | 2.6 | unknown | 100 | unsafe | 4.8 | unsafe | 0.25 | unsafe | 0.04 | unsafe | 0.58 |
sum03_unsafe.i | unsafe | 4.2 | unsafe | 2.8 | unsafe | 2.0 | unsafe | 3.1 | unsafe | 0.13 | unsafe | 0.05 | unsafe | 0.57 |
sum04_unsafe.i | unsafe | 1.00 | unsafe | 1.4 | unsafe | 1.3 | unsafe | 0.17 | unsafe | 0.03 | unsafe | 0.04 | unsafe | 0.42 |
sum_array_unsafe.i | unsafe | 0.59 | unsafe | 1.5 | unsafe | 110 | unsafe | 290 | unsafe | 0.04 | error | 0.06 | unsafe | 0.75 |
terminator_01_unsafe.i | unsafe | 0.08 | unsafe | 1.3 | unsafe | 1.2 | unsafe | 0.15 | unsafe | 0.04 | unsafe | 0.04 | unsafe | 0.50 |
terminator_02_unsafe.i | unsafe | 0.08 | unsafe | 1.3 | unsafe | 1.3 | unsafe | 0.17 | unsafe | 0.04 | unsafe | 0.04 | unsafe | 0.69 |
terminator_03_unsafe.i | unsafe | 0.16 | unsafe | 1.3 | unsafe | 1.4 | unsafe | 0.19 | unsafe | 0.04 | unsafe | 0.04 | unsafe | 0.58 |
token_ring01_unsafe.i | unsafe | 69 | unknown | 3.7 | unknown | 110 | unsafe | 0.69 | unsafe | 0.15 | unsafe | 0.12 | unsafe | 2.3 |
transmitter_unsafe.i | unsafe | 0.64 | unsafe | 3.1 | unsafe | 1.5 | unsafe | 2.6 | unsafe | 0.08 | unsafe | 0.05 | unsafe | 1.1 |
trex01_unsafe.i | unsafe | 0.08 | unsafe | 1.3 | unsafe | 1.6 | unsafe | 0.16 | unsafe | 0.05 | unsafe | 0.05 | unsafe | 0.54 |
trex02_unsafe.i | unsafe | 0.08 | unsafe | 1.4 | unsafe | 1.3 | unsafe | 0.15 | unsafe | 0.04 | unsafe | 0.04 | unsafe | 0.43 |
trex03_unsafe.i | unsafe | 0.08 | unsafe | 1.3 | unsafe | 1.3 | unsafe | 0.16 | unsafe | 0.04 | unsafe | 0.04 | unsafe | 0.56 |
verisec_NetBSD-libc__loop_unsafe.i | unsafe | 0.45 | unknown | 1.3 | unknown | 1.5 | unsafe | 0.18 | unsafe | 0.04 | unsafe | 0.05 | unsafe | 0.54 |
verisec_OpenSER__cases1_stripFullBoth_arr_unsafe.i | unsafe | 33 | safe | 1.3 | safe | 100 | unsafe | 0.28 | unsafe | 0.11 | error | 0.06 | failed | 0.56 |
verisec_sendmail__tTflag_arr_one_loop_unsafe.i | safe | 0.27 | safe | 1.3 | safe | 100 | unsafe | 2.6 | unsafe | 0.49 | unsafe | 0.07 | unsafe | 0.56 |
vogal_unsafe.i | timeout | 910 | safe | 6.1 | safe | 110 | unsafe | 2.6 | unsafe | 0.04 | unsafe | 0.08 | unsafe | 4.0 |
while_infinite_loop_4_unsafe.i | unsafe | 0.07 | unsafe | 1.3 | unsafe | 1.2 | unsafe | 0.16 | unsafe | 0.03 | unsafe | 0.04 | unsafe | 0.42 |
array_safe.i | unsafe | 0.10 | unknown | 1.8 | unknown | 1.5 | safe | 0.15 | safe | 0.05 | unsafe | 0.04 | safe | 0.48 |
bist.cell_safe.i | safe | 1.3 | safe | 8.9 | safe | 1.2 | safe | 0.32 | safe | 6.5 | safe | 0.07 | safe | 0.42 |
bubble_sort_safe.i | safe | 0.08 | timeout | 900 | timeout | 900 | safe | 0.30 | safe | 0.04 | error | 0.06 | safe | 0.40 |
count_up_down_safe.i | unsafe | 0.08 | unknown | 1.3 | unknown | 100 | unsafe | 450 | safe | 0.28 | unsafe | 0.06 | safe | 0.39 |
eureka_01_safe.i | timeout | 910 | safe | 220 | safe | 14 | safe | 0.48 | safe | 0.68 | safe | 12 | unsafe | 110 |
eureka_05_safe.i | error | 19 | unknown | 2.2 | unknown | 3.8 | safe | 0.30 | safe | 0.09 | safe | 0.08 | unsafe | 2.8 |
for_infinite_loop_1_safe.i | safe | 0.06 | safe | 1.4 | safe | 110 | safe | 0.18 | safe | 0.10 | safe | 0.08 | safe | 0.43 |
for_infinite_loop_2_safe.i | safe | 0.08 | safe | 1.4 | safe | 100 | safe | 0.19 | safe | 0.11 | safe | 0.08 | safe | 0.40 |
insertion_sort_safe.i | unsafe | 3.4 | unknown | 11 | unknown | 110 | safe | 0.45 | timeout | 910 | error | 0.05 | unsafe | 0.84 |
invert_string_safe.i | unsafe | 1.6 | safe | 2.5 | safe | 1.5 | safe | 14 | safe | 0.03 | error | 0.04 | unsafe | 0.56 |
kundu_safe.i | error | 2.2 | safe | 18 | safe | 5.1 | safe | 540 | timeout | 910 | safe | 0.44 | safe | 170 |
linear_sea.ch_safe.i | unsafe | 0.08 | unknown | 1.4 | unknown | 100 | safe | 0.24 | safe | 0.67 | error | 0.05 | unsafe | 0.53 |
list_safe.i | unsafe | 0.11 | unknown | 2.0 | unknown | 2.4 | safe | 0.43 | safe | 0.07 | safe | 0.10 | unsafe | 0.56 |
lu.cmp_safe.i | safe | 74 | safe | 9.1 | safe | 1.5 | safe | 0.65 | safe | 0.26 | safe | 1.9 | safe | 0.62 |
matrix_safe.i | error | 0.07 | unknown | 13 | unknown | 1.5 | safe | 0.18 | safe | 0.06 | unsafe | 0.04 | unknown | 0.06 |
mem_slave_tlm_safe.i | safe | 57 | safe | 5.3 | safe | 1.6 | safe | 830 | timeout | 910 | safe | 0.11 | safe | 520 |
n.c11_safe.i | safe | 0.63 | safe | 1.4 | safe | 1.5 | safe | 0.24 | safe | 0.10 | safe | 0.05 | safe | 0.94 |
n.c24_safe.i | timeout | 910 | timeout | 900 | timeout | 900 | error | 1.6 | unknown | 170 | error | 0.18 | timeout | 920 |
n.c40_safe.i | error | 3.2 | safe | 1.2 | safe | 100 | safe | 0.16 | safe | 0.97 | safe | 0.05 | safe | 0.36 |
nec40_safe.i | unsafe | 0.26 | safe | 1.3 | safe | 110 | safe | 0.15 | safe | 0.05 | safe | 0.05 | safe | 0.34 |
pc_sfifo_1_safe.i | safe | 10 | safe | 7.5 | safe | 110 | safe | 460 | safe | 120 | unsafe | 0.09 | safe | 7.2 |
string_safe.i | safe | 0.66 | safe | 1.3 | safe | 110 | safe | 450 | safe | 0.43 | error | 1.1 | safe | 0.39 |
sum01_safe.i | safe | 1.2 | unknown | 1.3 | unknown | 110 | safe | 0.19 | safe | 0.31 | unsafe | 0.04 | unsafe | 0.54 |
sum02_safe.i | error | 0.22 | unknown | 1.4 | unknown | 110 | safe | 0.21 | safe | 0.36 | unsafe | 0.04 | unsafe | 0.56 |
sum03_safe.i | safe | 0.19 | safe | 1.2 | safe | 1.3 | safe | 0.22 | safe | 0.14 | unsafe | 0.04 | safe | 0.40 |
sum04_safe.i | safe | 0.79 | safe | 1.3 | safe | 1.8 | safe | 0.16 | safe | 0.04 | safe | 0.05 | safe | 0.44 |
sum_array_safe.i | unsafe | 0.59 | safe | 1.4 | safe | 110 | safe | 0.28 | safe | 14 | error | 0.05 | unsafe | 0.77 |
terminator_01_safe.i | unknown | 0.06 | safe | 1.2 | safe | 1.1 | safe | 0.18 | safe | 0.20 | safe | 0.05 | safe | 0.42 |
terminator_02_safe.i | safe | 0.66 | safe | 1.2 | safe | 1.3 | safe | 0.20 | safe | 0.03 | safe | 0.05 | safe | 0.57 |
terminator_03_safe.i | safe | 0.31 | safe | 1.2 | safe | 1.4 | safe | 0.19 | safe | 0.41 | safe | 0.05 | safe | 0.52 |
token_ring01_safe.i | safe | 1.5 | safe | 5.4 | safe | 3.8 | safe | 460 | safe | 290 | unsafe | 0.05 | safe | 7.9 |
toy_safe.i | timeout | 910 | timeout | 900 | timeout | 900 | timeout | 910 | timeout | 910 | timeout | 900 | timeout | 920 |
trex01_safe.i | safe | 0.66 | safe | 1.3 | safe | 1.6 | safe | 0.27 | safe | 0.32 | unsafe | 0.07 | safe | 0.86 |
trex02_safe.i | safe | 0.14 | safe | 1.2 | safe | 1.4 | safe | 0.21 | safe | 0.33 | safe | 0.05 | safe | 0.44 |
trex03_safe.i | unsafe | 0.10 | unknown | 1.4 | unknown | 1.5 | safe | 0.22 | safe | 0.91 | safe | 0.06 | safe | 0.65 |
trex04_safe.i | safe | 0.36 | safe | 1.2 | safe | 1.4 | safe | 0.22 | safe | 0.48 | safe | 0.05 | safe | 0.52 |
veris.c_NetBSD-libc__loop_safe.i | safe | 0.21 | safe | 1.2 | safe | 1.4 | safe | 0.17 | safe | 0.06 | safe | 0.05 | safe | 0.40 |
veris.c_OpenSER__cases1_stripFullBoth_arr_safe.i | safe | 0.08 | safe | 1.3 | safe | 100 | safe | 1.4 | safe | 1.5 | timeout | 900 | safe | 0.39 |
veris.c_sendmail__tTflag_arr_one_loop_safe.i | safe | 0.27 | safe | 1.3 | safe | 100 | safe | 0.27 | safe | 0.18 | unknown | 0.10 | safe | 0.41 |
vogal_safe.i | timeout | 910 | safe | 5.4 | safe | 100 | safe | 450 | safe | 0.19 | error | 24 | unsafe | 0.87 |
while_infinite_loop_1_safe.i | safe | 0.07 | safe | 1.2 | safe | 1.1 | safe | 0.15 | safe | 0.10 | safe | 0.07 | safe | 0.40 |
while_infinite_loop_2_safe.i | safe | 0.08 | safe | 1.2 | safe | 1.1 | safe | 0.14 | safe | 0.08 | safe | 0.08 | safe | 0.38 |
while_infinite_loop_3_safe.i | safe | 0.07 | safe | 1.2 | safe | 1.1 | safe | 0.15 | safe | 0.09 | safe | 0.08 | safe | 0.39 |
total files | 79 | 6000 | 79 | 3100 | 79 | 5900 | 79 | 6800 | 79 | 4400 | 79 | 2200 | 79 | 2700 |
correct results | 55 | 550 | 53 | 370 | 52 | 1400 | 74 | 5000 | 74 | 540 | 49 | 17 | 64 | 750 |
false negatives | 1 | 0.27 | 4 | 14 | 4 | 420 | 2 | 470 | 0 | 0 | 0 | 0 | 0 | 0 |
false positives | 9 | 6.3 | 0 | 0 | 0 | 0 | 1 | 450 | 0 | 0 | 9 | 0.47 | 10 | 120 |
false properties | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
score (79 files, max score: 122) | 35 | 51 | 50 | 94 | 112 | 36 | 54 |