A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).
Found 31 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
69bff6c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2023-12-18T05:13:37+01:00 | ||
bf73915 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 7 | 2023-12-02T15:25:18Z | ||
183806f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2023-11-29T20:09:20Z | ||
78712d3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 7 | 2023-12-03T03:06:00Z | ||
bde527a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.4.0 kind | 4 | 2023-12-01T16:55:15Z | ||
b2af090 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-19T15:33:06+01:00 | a1e4b08 | |
91e34d9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-19T05:28:06+01:00 | 16ff5a5 | |
df4ce9d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 8 | 2023-12-18T06:03:13+01:00 | 69bff6c | |
771e00e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-05T14:40:06+01:00 | fe6d6f9 | |
16d340c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-04T16:46:14+01:00 | 6f80ab3 | |
76bd61d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 8 | 2023-12-04T12:12:29+01:00 | bf73915 | |
5cbec80 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-04T02:27:03+01:00 | 94cffe3 | |
807362a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-03T18:31:55+01:00 | b1e720c | |
59bba41 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-03T09:54:29+01:00 | b7df6db | |
534bf6f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 8 | 2023-12-03T06:18:57+01:00 | 78712d3 | |
1614736 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-01T18:29:06+01:00 | bde527a | |
506742a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T13:44:08+01:00 | e760031 | |
e760031 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T08:07:15+01:00 | ||
cc9f4d4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T03:01:22+01:00 | 183806f | |
57c7fd7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 8 | 2023-11-29T08:32:15+01:00 | c79c9b0 | |
94cffe3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T22:33:23+01:00 | ||
16ff5a5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T23:07:49+01:00 | ||
0b167c0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 7 | 2023-12-17T20:17:31+01:00 | ||
fe6d6f9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-05T12:46:13Z | ||
6f80ab3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-04T12:52:29Z | ||
c79c9b0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 7 | 2023-11-29T06:05:39Z | ||
b1e720c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:21:29+01:00 | ||
b7df6db | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:05:26Z | ||
a4ab390 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T22:07:29+01:00 | 0b167c0 | |
ac256de | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 63a2e02a-913f-4eca-b758-edadf02d7e00 creation_time: 2023-12-01T01:31:26Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i: d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | violation_witness | CPAchecker 2.3 | 8 | 2023-12-01T04:46:52+01:00 | ||
86dc44c | Inspect | - content: - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483646 location: column: 33 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_86735797-7679-41ad-98e4-94ab6303c1d3/sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i line: 550 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483647 location: column: 36 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_86735797-7679-41ad-98e4-94ab6303c1d3/sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i line: 551 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 1 location: column: 53 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_86735797-7679-41ad-98e4-94ab6303c1d3/sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i line: 555 type: function_return - segment: - waypoint: action: follow location: column: 17 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_86735797-7679-41ad-98e4-94ab6303c1d3/sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i line: 557 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:09:20Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_86735797-7679-41ad-98e4-94ab6303c1d3/sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i : d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_86735797-7679-41ad-98e4-94ab6303c1d3/sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 10 | 2023-11-30T02:57:48+01:00 |
Found 28 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
232fe42 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2022-12-09T04:53:36+01:00 | ||
31c995c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 7 | 2022-12-14T04:37:10Z | ||
a7af9b3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2022-12-12T16:07:08Z | ||
819c2aa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 7 | 2022-12-15T02:25:05Z | ||
8b72286 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.0.0 kind | 4 | 2022-12-18T19:15:10Z | ||
bbae05e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 6.8.0 kind | 4 | 2022-12-25T11:26:52Z | ||
19f5501 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 8 | 2023-01-29T10:45:27+01:00 | 31c995c | |
74d9a22 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 8 | 2023-01-29T06:54:36+01:00 | a5247ab | |
62b6f09 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 8 | 2023-01-29T06:38:02+01:00 | 819c2aa | |
2852867 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T05:58:20+01:00 | a7af9b3 | |
ceb6d46 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T01:30:45+01:00 | d4641cf | |
05298e0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T00:53:17+01:00 | 8811727 | |
3dd8084 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:51:14+01:00 | 43a297c | |
4ee7b32 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T21:08:37+01:00 | a2a9b88 | |
92ae0f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T17:38:23+01:00 | 33512bf | |
d6930f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T15:41:21+01:00 | 8b72286 | |
2810e03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T08:57:18+01:00 | 362c8b6 | |
b889d97 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 8 | 2023-01-28T08:33:21+01:00 | 232fe42 | |
54df699 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T02:23:24+01:00 | bbae05e | |
362c8b6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 7 | 2022-12-10T20:08:57+01:00 | ||
d4641cf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-11T22:48:45+01:00 | ||
a2a9b88 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-09T17:27:08+01:00 | ||
9d882d3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 7 | 2022-12-08T08:06:39+01:00 | ||
c59b04e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2022-12-08T17:15:41Z | ||
a5247ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 7 | 2022-12-13T16:10:23Z | ||
43a297c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:03:00+01:00 | ||
33512bf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T08:42:26Z | ||
8af71a5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T04:21:22+01:00 | 9d882d3 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4aaeb1f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T16:48 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/GulwaniJainKoskinen-2009PLDI-Fig1-alloca_true-termination.c.i, d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d0878af360c86b536b5b3bc8d222f1c5ce26337b4ad6227d126c258cfe065cc9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |