| Tool | CPAchecker ABE r4569 | CPAchecker ABM r4573 | ESBMC 1.17 | LLBMC 0.9 | Predator | |||||
| Limits | timelimit: 900 s, memlimit: 15000 MB | |||||||||
| System | os: Linux 2.6.35-30-generic x86_64 cpu: Intel(R) Core(TM) i7-2600K CPU @ 3.40GHz cores: 4, frequency: 3401 MHz, ram: 16375440 kB | |||||||||
| Date of run | 2011-12-03 10:32 | 2011-12-04 14:36 | 2011-12-04 08:46 | 2011-12-07 02:12 | 2011-12-04 23:44 | |||||
| Benchmark | heap | heap | heap | heap | heap | |||||
| Options | -heap 12500m -sv-comp12 | -heap 12500m -sv-comp12-abm | --64 --error-label ERROR --no-bounds-check --no-div-by-zero-check --no-assertions --no-pointer-check --no-unwinding-assertions --partial-loops --unwind 8 | -m32 | ||||||
| ../sv-benchmarks/ | status | runtime | status | runtime | status | runtime | status | runtime | status | runtime |
| total files | 14 | 26 | 14 | 26 | 14 | 2400 | 14 | 1300 | 14 | 1800 |
| correct results | 9 | 16 | 9 | 16 | 6 | 220 | 10 | 210 | 12 | 1.0 |
| false negatives | 0 | 0 | 0 | 0 | 1 | 220 | 0 | 0 | 0 | 0 |
| false positives | 5 | 9.4 | 5 | 10 | 3 | 1.1 | 0 | 0 | 0 | 0 |
| score (14 files, max score: 24) | 4 | 4 | 1 | 17 | 20 | |||||
| heap-manipulation/bubble_sort_linux_BUG.cil.c | unsafe | 1.7 | unsafe | 2.3 | unknown | 86 | unsafe | 0.34 | unsafe | 0.05 |
| heap-manipulation/dll_of_dll_BUG.cil.c | unsafe | 1.7 | unsafe | 2.1 | timeout | 900 | unknown | 0.05 | unsafe | 0.04 |
| heap-manipulation/merge_sort_BUG.cil.c | unsafe | 2.1 | unsafe | 1.7 | safe | 220 | unsafe | 0.48 | unsafe | 0.04 |
| heap-manipulation/sll_to_dll_rev_BUG.cil.c | unsafe | 2.1 | unsafe | 1.6 | unsafe | 0.96 | unsafe | 0.36 | unsafe | 0.04 |
| heap-manipulation/bubble_sort_linux.cil.c | unsafe | 2.2 | unsafe | 2.3 | unknown | 87 | timeout | 910 | safe | 0.08 |
| heap-manipulation/dll_of_dll.cil.c | unsafe | 2.1 | unsafe | 2.1 | timeout | 900 | unknown | 0.04 | safe | 0.08 |
| heap-manipulation/merge_sort.cil.c | unsafe | 2.1 | unsafe | 2.2 | safe | 220 | unknown | 200 | safe | 0.29 |
| heap-manipulation/sll_to_dll_rev.cil.c | unsafe | 1.6 | unsafe | 2.2 | unsafe | 0.91 | safe | 170 | safe | 0.11 |
| list-properties/alternating_list.cil.c | safe | 1.4 | safe | 2.0 | safe | 0.11 | safe | 2.3 | timeout | 900 |
| list-properties/list.cil.c | safe | 1.9 | safe | 1.5 | safe | 0.13 | safe | 9.6 | safe | 0.08 |
| list-properties/list_flag.cil.c | safe | 1.9 | safe | 1.5 | safe | 0.09 | safe | 2.4 | safe | 0.08 |
| list-properties/simple.cil.c | safe | 1.4 | safe | 1.7 | unsafe | 0.11 | safe | 1.8 | safe | 0.06 |
| list-properties/simple_built_from_end.cil.c | unsafe | 1.4 | unsafe | 1.5 | unsafe | 0.10 | safe | 1.9 | safe | 0.06 |
| list-properties/splice.cil.c | safe | 2.1 | safe | 1.7 | safe | 0.15 | safe | 20 | timeout | 900 |