Tool | CPAchecker 1.1.10-svcomp13 | ESBMC 1.20 | LLBMC SV-COMP-13 | Predator | ||||||
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-14 06:53 | 2012-11-14 08:27 | 2012-11-17 03:16 | 2012-12-04 06:32 | 2012-12-03 03:44 | |||||
Options | -sv-comp13--explitp-pred -heap 12000m -disable-java-assertions -spec valid-free -spec valid-deref -spec valid-memtrack |
-sv-comp13--combinations -heap 12000m -disable-java-assertions -spec valid-free -spec valid-deref -spec valid-memtrack |
memsafety | -mem-safety | -t memory -m32 |
|||||
../sv-benchmarks-trunk/memsafety/ | status | time | status | time | status | time | status | time | status | time |
960521-1_false-valid-deref.c | unsupported property | 0.18 | unsupported property | 0.19 | false(valid-deref) | 0.56 | false(valid-deref) | 0.69 | false(valid-deref) | 7.2 |
test-0137_false-valid-deref.c | unsupported property | 0.18 | unsupported property | 0.19 | error | 0.58 | false(valid-deref) | 0.07 | false(valid-deref) | 0.05 |
test-0235_false-valid-deref.c | unsupported property | 0.17 | unsupported property | 0.17 | timeout | 900 | false(valid-deref) | 0.11 | false(valid-deref) | 0.30 |
960521-1_false-valid-free.c | unsupported property | 0.18 | unsupported property | 0.19 | false(valid-free) | 0.43 | false(valid-free) | 0.27 | false(valid-free) | 7.0 |
test-0158_false-valid-free.c | unsupported property | 0.17 | unsupported property | 0.18 | error | 0.38 | false(valid-free) | 0.03 | false(valid-free) | 0.04 |
test-0232_false-valid-free.c | unsupported property | 0.17 | unsupported property | 0.19 | error | 0.36 | false(valid-free) | 0.09 | false(valid-free) | 0.06 |
20020406-1_false-valid-memtrack.c | unsupported property | 0.17 | unsupported property | 0.18 | false(valid-memtrack) | 1.4 | false(valid-memtrack) | 0.06 | false(valid-memtrack) | 0.08 |
20051113-1.c_false-valid-memtrack.c | unsupported property | 0.18 | unsupported property | 0.19 | error | 0.09 | false(valid-memtrack) | 0.05 | false(valid-memtrack) | 0.05 |
lockfree-3.1_false-valid-memtrack.c | unsupported property | 0.18 | unsupported property | 0.18 | false(valid-memtrack) | 420 | false(valid-memtrack) | 4.7 | false(valid-memtrack) | 6.5 |
lockfree-3.2_false-valid-memtrack.c | unsupported property | 0.17 | unsupported property | 0.18 | false(valid-memtrack) | 420 | false(valid-memtrack) | 0.07 | false(valid-memtrack) | 10 |
lockfree-3.3_false-valid-memtrack.c | unsupported property | 0.18 | unsupported property | 0.18 | false(valid-memtrack) | 480 | false(valid-memtrack) | 31 | false(valid-memtrack) | 10 |
test-0019_false-valid-memtrack.c | unsupported property | 0.18 | unsupported property | 0.18 | false(valid-memtrack) | 0.34 | false(valid-memtrack) | 0.03 | false(valid-memtrack) | 0.05 |
test-0102_false-valid-memtrack.c | unsupported property | 0.17 | unsupported property | 0.18 | error | 0.61 | false(valid-memtrack) | 0.03 | false(valid-memtrack) | 2.1 |
test-0158_false-valid-memtrack.c | unsupported property | 0.18 | unsupported property | 0.18 | false(valid-memtrack) | 0.30 | false(valid-memtrack) | 0.03 | false(valid-memtrack) | 0.05 |
test-0220_false-valid-memtrack.c | unsupported property | 0.17 | unsupported property | 0.18 | error | 0.70 | false(valid-memtrack) | 0.44 | false(valid-memtrack) | 0.06 |
test-0232_false-valid-memtrack.c | unsupported property | 0.17 | unsupported property | 0.18 | false(valid-memtrack) | 5.7 | false(valid-memtrack) | 0.03 | false(valid-memtrack) | 0.05 |
test-0234_false-valid-memtrack.c | unsupported property | 0.18 | unsupported property | 0.18 | timeout | 900 | false(valid-memtrack) | 0.04 | false(valid-memtrack) | 0.10 |
test-0235_false-valid-memtrack.c | unsupported property | 0.17 | unsupported property | 0.19 | timeout | 900 | false(valid-memtrack) | 0.05 | false(valid-memtrack) | 0.53 |
960521-1_true.c | unsupported property | 0.18 | unsupported property | 0.18 | false(valid-free) | 0.34 | safe | 0.34 | timeout | 900 |
lockfree-3.0_true.c | unsupported property | 0.18 | unsupported property | 0.18 | false(valid-memtrack) | 560 | timeout | 910 | safe | 11 |
test-0019_true.c | unsupported property | 0.18 | unsupported property | 0.18 | safe | 0.35 | safe | 0.13 | safe | 0.05 |
test-0102_true.c | unsupported property | 0.18 | unsupported property | 0.18 | error | 0.68 | timeout | 910 | safe | 2.5 |
test-0134_true.c | unsupported property | 0.18 | unsupported property | 0.18 | error | 0.54 | timeout | 910 | safe | 0.10 |
test-0158_true.c | unsupported property | 0.18 | unsupported property | 0.19 | error | 0.32 | safe | 0.08 | safe | 0.05 |
test-0214_true.c | unsupported property | 0.18 | unsupported property | 0.18 | error | 0.19 | timeout | 900 | safe | 0.08 |
test-0217_true.c | unsupported property | 0.18 | unsupported property | 0.18 | error | 0.22 | timeout | 910 | safe | 0.09 |
test-0218_true.c | unsupported property | 0.17 | unsupported property | 0.18 | error | 0.20 | timeout | 910 | safe | 0.09 |
test-0219_true.c | unsupported property | 0.18 | unsupported property | 0.18 | error | 0.80 | timeout | 910 | safe | 0.07 |
test-0232_true.c | unsupported property | 0.18 | unsupported property | 0.18 | error | 0.33 | timeout | 910 | safe | 0.05 |
test-0234_true.c | unsupported property | 0.18 | unsupported property | 0.18 | timeout | 900 | unknown | 160 | safe | 0.11 |
test-0235_true.c | unsupported property | 0.18 | unsupported property | 0.18 | timeout | 900 | unknown | 170 | safe | 1.2 |
test-0236_true.c | unsupported property | 0.17 | unsupported property | 0.18 | timeout | 900 | unknown | 170 | safe | 0.17 |
test-0237_true.c | unsupported property | 0.18 | unsupported property | 0.18 | timeout | 900 | unknown | 170 | safe | 0.19 |
test-0504_true.c | unsupported property | 0.18 | unsupported property | 0.18 | timeout | 900 | timeout | 910 | safe | 0.17 |
test-0513_true.c | unsupported property | 0.18 | unsupported property | 0.18 | error | 150 | timeout | 910 | safe | 0.10 |
test-0521_true.c | unsupported property | 0.18 | unsupported property | 0.19 | timeout | 900 | unknown | 320 | safe | 0.41 |
total files | 36 | 6.4 | 36 | 6.6 | 36 | 10000 | 36 | 10000 | 36 | 960 |
correct results | 0 | 0 | 0 | 0 | 10 | 1300 | 21 | 38 | 35 | 61 |
false negatives | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
false positives | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
false properties | 0 | 0 | 0 | 0 | 2 | 560 | 0 | 0 | 0 | 0 |
score (36 files, max score: 54) | 0 | 0 | 3 | 24 | 52 |