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 41 witnesses for program sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
53e2ce8 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:01:56+01:00 | ||
eea0e56 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T03:55:51Z | ||
66943cc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T12:02:15+01:00 | 53e2ce8 | |
3679d13 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T06:27:18+01:00 | ||
3ec2124 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T20:39:38+01:00 | ||
62e065a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2023-12-19T10:37:10+01:00 | ||
5d467b4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T20:40:10+01:00 | ||
d38e3d0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2023-12-18T01:33:26+01:00 | ||
8ce3538 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 9 | 2023-12-02T13:54:41Z | ||
3f8cafd | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 9 | 2023-11-29T05:50:38Z | ||
d32be94 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:22:25+01:00 | ||
df47a33 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:44:39Z | ||
9f027af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2023-12-02T19:08:22Z | ||
af38a91 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:20:48Z | ||
56db32d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T12:46:26Z | ||
128c4de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 9 | 2023-12-02T19:56:33Z | ||
5eb1f6e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 7 | 2023-12-01T01:23:28Z | ||
8b29278 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T15:14:34+01:00 | 830e57b | |
f7ebd38 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T02:57:52+01:00 | 4e79533 | |
06561c5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T06:19:19+01:00 | ae023f6 | |
22ef919 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T11:38:10+01:00 | 9f027af | |
be6cf22 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T01:50:51+01:00 | 38867ab | |
8c09d0e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:29:56+01:00 | d32be94 | |
9e5ab23 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T09:54:40+01:00 | df47a33 | |
1a44d59 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T05:51:00+01:00 | 128c4de | |
75203a7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T03:41:46+01:00 | 5eb1f6e | |
fe2c0f1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T12:53:06+01:00 | 9d1aa61 | |
9d1aa61 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:41:08+01:00 | ||
af66a26 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T02:43:50+01:00 | af38a91 | |
d39e473 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T18:19:52+01:00 | 56db32d | |
8e195ae | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:07:09+01:00 | 923a66a | |
38867ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-04T00:02:11+01:00 | ||
ae023f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2023-12-17T03:59:06+01:00 | ||
830e57b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 5 | 2023-12-19T12:40:02+01:00 | ||
4e79533 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T20:08:27+01:00 | ||
923a66a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2023-11-29T00:07:52Z | ||
773f037 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:12:56Z | ||
4a83c92 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: f8a1130d-6658-4335-aa65-ecfb7510cd62 creation_time: '2023-12-02T20:56:33+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec62543c-dc88-4aa1-aaf6-3e2154ccecc2/sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec62543c-dc88-4aa1-aaf6-3e2154ccecc2/sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i : 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:46:35+01:00 | ||
d99417f | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 6fa0aaf2-ef9a-4633-ba74-99d4244ece47 creation_time: '2023-11-29T01:07:52+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fd9b8347-56fc-4e72-80b4-8e8cb20b9b3d/sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fd9b8347-56fc-4e72-80b4-8e8cb20b9b3d/sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i : 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T07:51:19+01:00 | ||
9f4c1aa | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 15bcc80c-ae1c-447e-9be0-c641c8e96510 creation_time: '2023-12-02T20:08:22+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_09f0556e-266a-4d94-9410-92f5f69b395b/sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_09f0556e-266a-4d94-9410-92f5f69b395b/sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i : 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:03:30+01:00 | ||
7ad7695 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: c6d4c9b9-2d9d-475d-8a20-72b0f142ec19 creation_time: 2023-12-01T01:23:28Z 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/cstrlen-alloca-1.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i: 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca-1.i file_hash: 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee line: 550 column: 12 function: cstrlen value: s == p format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T04:15:42+01:00 |
Found 33 witnesses for program sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
87c7872 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:09:48+01:00 | ||
110705f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T10:09:50Z | ||
1e5b34f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T14:17:11+01:00 | 87c7872 | |
5c8a320 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T20:06:51+01:00 | ||
8f768dd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T00:58:20+01:00 | ||
a01a584 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2022-12-11T04:23:17+01:00 | ||
c16fd6f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T03:29:02+01:00 | ||
e680e86 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2022-12-09T02:52:20+01:00 | ||
3fec1e6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 8 | 2022-12-13T17:30:18Z | ||
900ee26 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:52:06+01:00 | ||
af837b1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T09:39:58Z | ||
3950ad8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2022-12-14T12:41:43Z | ||
d95a941 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T09:50:33Z | ||
44acb3b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 8 | 2022-12-14T21:12:49Z | ||
7c4e822 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 9 | 2022-12-10T08:31:41Z | ||
bc0e3ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T10:51:21+01:00 | 3950ad8 | |
fda826e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T07:25:13+01:00 | 49e20ab | |
f5996c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:23:28+01:00 | 44acb3b | |
9a34753 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T03:46:25+01:00 | d95a941 | |
e34e88f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T02:35:01+01:00 | 1315d47 | |
9ae7991 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T00:07:06+01:00 | 24ddfd3 | |
cdc4cae | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:51:35+01:00 | 900ee26 | |
fe813b7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:40:12+01:00 | 7c4e822 | |
d536789 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T18:46:54+01:00 | 0d1d036 | |
9089ae1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:38:23+01:00 | af837b1 | |
8541acc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T12:20:48+01:00 | 28900b0 | |
f337001 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T01:00:33+01:00 | f577938 | |
28900b0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T21:43:10+01:00 | ||
1315d47 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T01:04:21+01:00 | ||
f577938 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2022-12-25T10:08:41+01:00 | ||
24ddfd3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 5 | 2022-12-11T04:36:04+01:00 | ||
0d1d036 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T03:40:24+01:00 | ||
49e20ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2022-12-13T11:40:19Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bdaa908 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:29:48 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
dab4e89 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T22:36:43 | ||
038a20c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T13:54:08 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.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/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.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/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ed58fea | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T21:05 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/cstrlen-alloca_true-termination.c.i, 55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/55b7e97c43627abc3b3fb7d9c27999e540608fa7f6d0b7e81ad0fc505311daee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |