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 39 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
730913e | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:05:22+01:00 | ||
d7aba05 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T04:08:35Z | ||
8f7e64e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:05:36+01:00 | 730913e | |
aa30e5a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T08:45:15+01:00 | ||
ad2ef2b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-04T00:37:15+01:00 | ||
27efbfa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2023-12-18T01:35:19+01:00 | ||
fad62ee | 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 | 12 | 2023-12-02T15:13:59Z | ||
a520bce | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T12:14:52Z | ||
1f7983a | 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 | 12 | 2023-11-29T02:50:35Z | ||
ec356ef | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-19T01:34:53+01:00 | ||
1c8320d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2023-12-18T04:42:38+01:00 | ||
9fff98d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:16:48+01:00 | ||
fe187fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:19:51Z | ||
1fadaf1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 11 | 2023-12-02T18:26:01Z | ||
9c7e0a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T02:15:47Z | ||
3ae32a2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T18:41:21Z | ||
bb4e781 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 11 | 2023-12-03T02:46:03Z | ||
899101f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 9 | 2023-12-01T00:56:12Z | ||
5073b88 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T04:16:07+01:00 | 90975d0 | |
01ad4cf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T06:11:37+01:00 | 1c8320d | |
a7869fc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:17:31+01:00 | 9c7e0a1 | |
29e67df | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:37:07+01:00 | 1fadaf1 | |
9e05798 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T02:10:16+01:00 | 72c5a5f | |
ae90c6a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:32:42+01:00 | 9fff98d | |
f0fb5a4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T09:54:14+01:00 | fe187fe | |
a53d918 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T06:03:01+01:00 | bb4e781 | |
7e52e5f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T03:35:50+01:00 | 899101f | |
bce49c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T12:21:06+01:00 | 78053a1 | |
78053a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T08:56:03+01:00 | ||
f1b89de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T02:33:41+01:00 | 3ae32a2 | |
c80af1e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:07:31+01:00 | c6f0a68 | |
72c5a5f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T21:10:20+01:00 | ||
90975d0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T19:02:55+01:00 | ||
c6f0a68 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 11 | 2023-11-28T23:32:00Z | ||
390f80d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:44:57Z | ||
c6638be | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: ad33e9e1-8593-4e94-9b00-fefcb7658414 creation_time: 2023-11-29T00:32+01:00 producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_907b9da7-135d-41d1-b7ad-650f58a0fa3d/sv-benchmarks/c/termination-dietlibc/strrchr_short.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_907b9da7-135d-41d1-b7ad-650f58a0fa3d/sv-benchmarks/c/termination-dietlibc/strrchr_short.i : 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T07:42:53+01:00 | ||
7e4b714 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 5c1c10ba-7655-427d-97f3-d3ec0d65c7e9 creation_time: '2023-12-02T19:26:01+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_47ccb134-6f6b-4754-854b-695821affbd7/sv-benchmarks/c/termination-dietlibc/strrchr_short.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_47ccb134-6f6b-4754-854b-695821affbd7/sv-benchmarks/c/termination-dietlibc/strrchr_short.i : 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T12:04:17+01:00 | ||
265081d | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 44212541-a1a5-42f8-a645-f8e1bbd7a71c creation_time: '2023-12-03T03:46:03+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_67ccedce-c6d6-46f4-9740-1a4a674d376e/sv-benchmarks/c/termination-dietlibc/strrchr_short.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_67ccedce-c6d6-46f4-9740-1a4a674d376e/sv-benchmarks/c/termination-dietlibc/strrchr_short.i : 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:32:26+01:00 | ||
19c3479 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 8b38963b-8597-4017-800f-5c59b9b14b4d creation_time: 2023-12-01T00:56:12Z 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-dietlibc/strrchr_short.i''' task: input_files: - ../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i input_file_hashes: ../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i: 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i file_hash: 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1 line: 511 column: 8 function: strrchr value: 0 == l format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i file_hash: 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1 line: 511 column: 8 function: strrchr value: c == ch format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i file_hash: 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1 line: 511 column: 8 function: strrchr value: l == 0 format: c_expression | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T04:31:04+01:00 |
Found 34 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
798bb2a | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:30:44+01:00 | ||
b6d812d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T08:49:29Z | ||
e2a1a4e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T04:19:22+01:00 | b57e407 | |
5cf0c61 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:21:11+01:00 | 798bb2a | |
53ecb24 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T18:03:45+01:00 | ||
d9591b6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T23:48:52+01:00 | ||
3911b23 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-09T16:56:30+01:00 | ||
f53ce87 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2022-12-09T02:43:48+01:00 | ||
d6887d5 | 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 | 11 | 2022-12-14T11:46:14Z | ||
685a894 | 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 | 10 | 2022-12-13T10:25:39Z | ||
8a76ef6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2022-12-09T04:59:15+01:00 | ||
c225e31 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:52:09+01:00 | ||
b731cea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T09:56:27Z | ||
2c25207 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 10 | 2022-12-14T07:40:32Z | ||
5de1ee1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T11:58:41Z | ||
f05c62a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T15:03:00Z | ||
ded99ca | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 10 | 2022-12-15T01:32:37Z | ||
859b864 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 12 | 2022-12-10T07:40:04Z | ||
775a4c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:11:23+01:00 | 2c25207 | |
a5d9765 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T07:38:00+01:00 | 67ce7fe | |
962e7b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:30:27+01:00 | ded99ca | |
68b97d5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T05:18:45+01:00 | f05c62a | |
d7732d2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T02:33:47+01:00 | bc65beb | |
c8783e2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:51:22+01:00 | c225e31 | |
565200c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:37:45+01:00 | 859b864 | |
dab934a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T18:45:09+01:00 | dd127fa | |
4944bbe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:38:50+01:00 | b731cea | |
cb07a6e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T11:25:49+01:00 | f5ca03d | |
de1823e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T08:34:06+01:00 | 8a76ef6 | |
572a785 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T01:02:44+01:00 | 5de1ee1 | |
f5ca03d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T19:57:31+01:00 | ||
bc65beb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T22:19:53+01:00 | ||
dd127fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T01:52:32+01:00 | ||
67ce7fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 10 | 2022-12-13T17:19:54Z |
Found 1 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
598b23e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:45:17 |
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7785b8b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T17:07:46 | ||
e5c0b40 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T19:46:07 |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strrchr_short_true-termination.c.i, 5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5714449da9967bbd2918d4305e52dc9c1161024d975984886640d613abe881d1.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |