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 37 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ac2f26a | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:31:36+01:00 | ||
af7ce46 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T01:58:49Z | ||
1298973 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-18T12:01:46+01:00 | ac2f26a | |
9ae49da | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T09:09:11+01:00 | ||
59aa699 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T20:37:23+01:00 | ||
940465f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 13 | 2023-12-18T01:44:18+01:00 | ||
9ea6a92 | 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 | 19 | 2023-11-29T01:17:04Z | ||
60c9173 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 7 | 2023-12-19T10:37:30+01:00 | ||
d7f9a85 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-19T01:19:19+01:00 | ||
ddc10cb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:57:12+01:00 | ||
0d50766 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T08:02:36Z | ||
969ddd4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 17 | 2023-12-02T14:40:21Z | ||
cc386da | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T01:58:42Z | ||
da0f498 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:28:53Z | ||
67ba7a5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T09:22:08Z | ||
805fa67 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 17 | 2023-12-02T19:52:19Z | ||
0056e90 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T14:54:04+01:00 | f36a167 | |
0c7465e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T02:59:47+01:00 | 738290a | |
47df936 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-17T06:08:44+01:00 | cc386da | |
bbc3f3d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T11:30:43+01:00 | 969ddd4 | |
57c5fbb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T02:12:32+01:00 | 17dd34a | |
3b22ead | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T18:33:16+01:00 | ddc10cb | |
7001795 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T09:54:22+01:00 | 0d50766 | |
b2b27ae | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:49:26+01:00 | 805fa67 | |
7826dc0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T11:37:26+01:00 | 57f7d25 | |
57f7d25 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T06:41:20+01:00 | ||
333da15 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T02:30:09+01:00 | da0f498 | |
c377879 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T18:25:55+01:00 | 67ba7a5 | |
5c0604c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T08:02:44+01:00 | ad07e7a | |
17dd34a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T21:54:02+01:00 | ||
f36a167 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2023-12-19T12:12:31+01:00 | ||
738290a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T20:49:10+01:00 | ||
ad07e7a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 17 | 2023-11-29T03:25:19Z | ||
216a25b | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: f7a1ad6b-9cd6-4990-a928-5e1c41ca0e96 creation_time: '2023-11-29T04:25:19+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dfaa01d4-cf61-4214-a1dc-c2d0aa683211/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dfaa01d4-cf61-4214-a1dc-c2d0aa683211/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i : ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T07:47:09+01:00 | ||
04fcf89 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: e2b761ae-c080-4499-a149-3468d668d394 creation_time: '2023-12-02T20:52:19+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5da0c7f4-f4c9-4ce4-aebb-6c46cf072f09/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5da0c7f4-f4c9-4ce4-aebb-6c46cf072f09/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i : ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T05:35:45+01:00 | ||
1a79577 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 1841af8d-4851-4589-8319-4bd7b8a99d7b creation_time: '2023-12-02T15:40:21+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1edc6e2c-0959-4049-840b-5b2f28d7bd2d/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1edc6e2c-0959-4049-840b-5b2f28d7bd2d/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i : ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T12:01:27+01:00 | ||
b008b27 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 55f78097-b1e4-4704-a5d2-5259b1761eef creation_time: 2023-12-01T01:38:52Z 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_cstpncpy-alloca-2.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 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_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 557 column: 11 function: cstpncpy value: (n != 18446744073709551615UL && (((n != 18446744073709551614UL && (((n != 18446744073709551613UL && (((n != 18446744073709551612UL && (((n != 18446744073709551611UL && (((n != 18446744073709551610UL && (((n <= 2147483640UL && n != 18446744073709551609UL) || ((1UL <= n && n <= 2147483641UL) && n != 0UL)) || n <= 2147483641UL)) || ((1UL <= n && n <= 2147483642UL) && n != 0UL)) || n <= 2147483642UL)) || ((1UL <= n && n <= 2147483643UL) && n != 0UL)) || n <= 2147483643UL)) || ((1UL <= n && n <= 2147483644UL) && n != 0UL)) || n <= 2147483644UL)) || ((1UL <= n && n <= 2147483645UL) && n != 0UL)) || n <= 2147483645UL)) || ((1UL <= n && n <= 2147483646UL) && n != 0UL)) || n <= 2147483646UL)) || ((1UL <= n && n <= 2147483647UL) && n != 0UL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 555 column: 8 function: cstpncpy value: 1UL <= n format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 555 column: 8 function: cstpncpy value: n <= 2147483647UL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 555 column: 8 function: cstpncpy value: n != 0UL format: c_expression | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-01T04:35:16+01:00 |
Found 33 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
43b5a42 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:13:52+01:00 | ||
c259925 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T12:06:01Z | ||
cd2b794 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T14:18:06+01:00 | 43b5a42 | |
88330e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T15:59:48+01:00 | ||
cde2ac8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-12T02:38:02+01:00 | ||
b3137cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2022-12-11T02:05:45+01:00 | ||
708c645 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-09T18:12:37+01:00 | ||
bfe5cd8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 13 | 2022-12-09T03:14:06+01:00 | ||
a8cd393 | 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 | 18 | 2022-12-13T16:20:23Z | ||
b87e10b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T21:59:13+01:00 | ||
ec67ff6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T12:54:12Z | ||
5adfbc6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 16 | 2022-12-14T14:35:29Z | ||
0fab770 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T12:35:45Z | ||
ce793ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T13:43:00Z | ||
f3d6e85 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T09:24:21Z | ||
bbac80f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 16 | 2022-12-14T19:49:09Z | ||
23d75cd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T11:06:21+01:00 | 5adfbc6 | |
54ee6cf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T07:16:09+01:00 | e5732d5 | |
8c3f897 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T06:24:52+01:00 | bbac80f | |
dd9e2ad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T05:31:12+01:00 | ce793ab | |
7c0698a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T03:46:23+01:00 | f3d6e85 | |
5ee6243 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T02:49:22+01:00 | 4dbaafc | |
c1276f1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T00:07:03+01:00 | 47954d7 | |
fa4131e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:50:45+01:00 | b87e10b | |
f367004 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T19:00:27+01:00 | 2cdd821 | |
a9ccf43 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T17:38:04+01:00 | ec67ff6 | |
319a24c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T11:26:49+01:00 | bb61950 | |
6da782b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T01:01:07+01:00 | 0fab770 | |
bb61950 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T20:09:26+01:00 | ||
4dbaafc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-11T23:31:35+01:00 | ||
47954d7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2022-12-11T04:03:30+01:00 | ||
2cdd821 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T01:47:48+01:00 | ||
e5732d5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 16 | 2022-12-13T14:32:31Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
93d9671 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T18:42:28 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0d24544 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T15:34:34 | ||
b52b915 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:39:21 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.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_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.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_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.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_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |