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 40 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f0c952b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:46:55+01:00 | ||
7c28ea0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T00:56:26Z | ||
5993e8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-18T12:05:21+01:00 | f0c952b | |
9879651 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T06:08:41+01:00 | ||
b9bcebf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T22:02:27+01:00 | ||
29ff3f9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 11 | 2023-12-18T02:03:48+01:00 | ||
d31c6a0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 7 | 2023-12-19T12:35:12+01:00 | ||
b5f1f4a | 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 | 13 | 2023-11-28T23:28:37Z | ||
0ac238a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T19:37:47+01:00 | ||
a1dafe1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:45:21+01:00 | ||
bf235de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:19:18Z | ||
93b408e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 12 | 2023-12-02T17:53:23Z | ||
ae0ec70 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T02:12:52Z | ||
9f04966 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T22:48:26Z | ||
cb2e7c2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T15:33:11Z | ||
71b4178 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 12 | 2023-12-03T03:06:02Z | ||
da50507 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 10 | 2023-12-01T01:14:03Z | ||
cc18ecb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T14:38:52+01:00 | 2db36be | |
84eded5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T03:29:25+01:00 | 56e9a1e | |
9680831 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-17T06:13:17+01:00 | ae0ec70 | |
cebecda | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T11:37:50+01:00 | 93b408e | |
60f1b65 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T01:56:17+01:00 | 6d90f32 | |
489f77d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T18:34:19+01:00 | a1dafe1 | |
86b3535 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T09:54:31+01:00 | bf235de | |
27cbdc5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:49:15+01:00 | 71b4178 | |
64bcf54 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-01T03:35:54+01:00 | da50507 | |
a9ede75 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T12:24:55+01:00 | 8ed7796 | |
8ed7796 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T04:52:12+01:00 | ||
21f81fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T02:33:48+01:00 | 9f04966 | |
ae871aa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T18:22:24+01:00 | cb2e7c2 | |
4dc5b69 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T07:54:17+01:00 | 78b004f | |
6d90f32 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-04T00:37:11+01:00 | ||
2db36be | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2023-12-19T13:35:25+01:00 | ||
56e9a1e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T22:09:34+01:00 | ||
78b004f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 12 | 2023-11-29T02:49:23Z | ||
2a0138f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-11-30T22:42:30Z | ||
43d7aee | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 728b6738-3f22-46b7-b58b-fbee1bdddd7f creation_time: '2023-12-03T04:06:02+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cfa61d12-d626-4a56-9693-2eaad085c465/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cfa61d12-d626-4a56-9693-2eaad085c465/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i : 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:33:52+01:00 | ||
6c0c70d | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 6f441aaa-628d-4325-b378-217ada737edd creation_time: '2023-11-29T03:49:23+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_696c1ed6-e93c-4c9e-a40f-08a60353e88b/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_696c1ed6-e93c-4c9e-a40f-08a60353e88b/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i : 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T07:46:09+01:00 | ||
8f43c81 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 5bf49e41-03d8-47ef-bc22-c0f371afd1af creation_time: '2023-12-02T18:53:23+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c0be1598-29ce-443b-ba04-ad5ecd45b516/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c0be1598-29ce-443b-ba04-ad5ecd45b516/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i : 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T12:04:36+01:00 | ||
d7d677e | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 174e64e1-6724-4920-b262-e58c1245914a creation_time: 2023-12-01T01:14:03Z 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/openbsd_cstrcpy-alloca-1.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca-1.i: 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395 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/openbsd_cstrcpy-alloca-1.i file_hash: 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395 line: 551 column: 5 function: cstrcpy value: to == save format: c_expression | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T04:27:46+01:00 |
Found 35 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
185e349 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:23:59+01:00 | ||
3078557 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T11:11:52Z | ||
7fd6f43 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T14:10:41+01:00 | 185e349 | |
77bec5b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T19:57:23+01:00 | ||
c542dde | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-11T23:23:16+01:00 | ||
36c0cee | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2022-12-11T04:08:27+01:00 | ||
eebf261 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 11 | 2022-12-09T02:49:14+01:00 | ||
c9bff2c | 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 | 2022-12-13T13:06:53Z | ||
61ceddd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T02:49:48+01:00 | ||
5685015 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:47:57+01:00 | ||
bd432aa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T09:25:51Z | ||
7a24ec5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 12 | 2022-12-14T07:57:42Z | ||
d986723 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T10:41:41Z | ||
196232e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T13:00:12Z | ||
9a06126 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:18:46Z | ||
ff2daab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 11 | 2022-12-15T01:50:28Z | ||
d109f9c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 15 | 2022-12-10T09:09:59Z | ||
183c9ba | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T10:52:30+01:00 | 7a24ec5 | |
0e69f76 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T07:17:05+01:00 | a6f8373 | |
3b4d533 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T06:28:18+01:00 | ff2daab | |
d346ddb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T05:20:02+01:00 | 196232e | |
0660bdf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T03:45:52+01:00 | 9a06126 | |
05d2d47 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T03:00:12+01:00 | 0f6ef97 | |
e88700a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T00:06:32+01:00 | 3fbddb0 | |
9730e2e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:51:04+01:00 | 5685015 | |
a3eb2e3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:25:51+01:00 | d109f9c | |
ab818f8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T18:56:09+01:00 | 7bc5e63 | |
fc75fb0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T17:38:12+01:00 | bd432aa | |
6ea195f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T12:23:28+01:00 | 5d8f399 | |
f86f884 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T01:00:52+01:00 | d986723 | |
5d8f399 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T14:48:12+01:00 | ||
0f6ef97 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T01:48:27+01:00 | ||
3fbddb0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2022-12-11T04:55:55+01:00 | ||
7bc5e63 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T03:21:50+01:00 | ||
a6f8373 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 11 | 2022-12-13T20:44:33Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c9562ab | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:56:10 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8a19d0c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T14:20:15 | ||
8ad040f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T15:23:44 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.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/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.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/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.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/openbsd_cstrcpy-alloca_true-termination.c.i, 96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/96d73e5144e69b17de356213175b4cac1e1bd0fb8c4e4377e7e151c0511f2395.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |