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 42 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c7e9aa9 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:51:16+01:00 | ||
99275a3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T03:44:38Z | ||
b07fb40 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:02:04+01:00 | c7e9aa9 | |
d4ec5f3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T07:44:52+01:00 | ||
a329982 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T22:43:13+01:00 | ||
c98734e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 6 | 2023-12-19T10:37:39+01:00 | ||
919508d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-19T00:42:07+01:00 | ||
590b322 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 11 | 2023-12-18T01:56:59+01:00 | ||
14b0c3a | 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 | 15 | 2023-11-29T05:58:57Z | ||
649e262 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:52:45+01:00 | ||
effb8bc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T04:12:48Z | ||
f408a82 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2023-12-02T14:53:20Z | ||
810a9c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:20:04Z | ||
a13e439 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T23:09:26 | ||
7e23a23 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T12:29:33Z | ||
339ca80 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 15 | 2023-12-02T23:44:21Z | ||
15465a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 11 | 2023-12-01T01:48:08Z | ||
e044549 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-20T02:16:40+01:00 | a13e439 | |
f9d31c9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T15:14:49+01:00 | 101cbcb | |
5e750c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T03:14:11+01:00 | eadc622 | |
57ff481 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:23:01+01:00 | 914d50e | |
dc6b351 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:27:40+01:00 | f408a82 | |
39283f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T01:50:56+01:00 | 5a04032 | |
cc017a0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:31:04+01:00 | 649e262 | |
fdb48b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T09:54:10+01:00 | effb8bc | |
3a5204a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T06:02:53+01:00 | 339ca80 | |
62afbf1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T03:40:10+01:00 | 15465a1 | |
bcf9d87 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T12:43:00+01:00 | 7e5a177 | |
7e5a177 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T05:45:04+01:00 | ||
1e34315 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T02:27:25+01:00 | 810a9c4 | |
2e55e0c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T18:28:18+01:00 | 7e23a23 | |
016e575 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:22:26+01:00 | 9eb735c | |
5a04032 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-04T00:28:05+01:00 | ||
914d50e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2023-12-17T04:02:24+01:00 | ||
101cbcb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2023-12-19T13:06:18+01:00 | ||
eadc622 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T17:08:57+01:00 | ||
9eb735c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2023-11-29T03:41:06Z | ||
7f54dde | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:56:17Z | ||
66a1922 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: cf7d484a-a08a-4800-b46d-caedd481cae5 creation_time: '2023-11-29T04:41:06+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6dc74d27-aed4-40ac-acf2-43dad8ce4867/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6dc74d27-aed4-40ac-acf2-43dad8ce4867/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i : de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T07:43:38+01:00 | ||
1dd2539 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 84048007-fcca-4daa-84fc-46e9ec8f443e creation_time: '2023-12-03T00:44:21+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6a4ba9b8-6a0e-4be2-ba65-d8bb75478323/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6a4ba9b8-6a0e-4be2-ba65-d8bb75478323/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i : de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:44:59+01:00 | ||
08ca59e | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 66323204-b01c-4424-9f80-e0aa544781d3 creation_time: '2023-12-02T15:53:20+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_228498bb-dace-426a-95a2-c8739d7b9800/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_228498bb-dace-426a-95a2-c8739d7b9800/sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i : de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T11:59:41+01:00 | ||
fe5cee3 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: d110d245-0b0f-43f7-8ff9-f904cd72632b creation_time: 2023-12-01T01:48:08Z 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_cstrcspn-alloca-1.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i: de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4 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_cstrcspn-alloca-1.i file_hash: de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4 line: 556 column: 8 function: cstrcspn value: c == (char)0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i file_hash: de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4 line: 556 column: 8 function: cstrcspn value: sc == (char)0 || s2 == spanp format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca-1.i file_hash: de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4 line: 553 column: 2 function: cstrcspn value: s1 == p format: c_expression | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T04:48:59+01:00 |
Found 36 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
255b6b9 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:36:06+01:00 | ||
21606bb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T09:14:23Z | ||
a23a255 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:14:03+01:00 | 255b6b9 | |
722f0a4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T21:06:55+01:00 | ||
686a207 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T01:37:24+01:00 | ||
33e0b2e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 6 | 2022-12-11T04:51:40+01:00 | ||
c245c74 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T04:21:21+01:00 | ||
0d35ef8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 11 | 2022-12-09T02:35:27+01:00 | ||
7091506 | 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 | 14 | 2022-12-14T11:35:50Z | ||
c0cf216 | 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 | 14 | 2022-12-13T11:28:24Z | ||
08d8742 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:46:26+01:00 | ||
662c882 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:42:43Z | ||
e5ceb70 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 14 | 2022-12-14T14:52:20Z | ||
33211f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T16:05:44 | ||
53d8bb3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:55:38Z | ||
0bac071 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 14 | 2022-12-14T20:53:22Z | ||
6c790b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 16 | 2022-12-10T04:03:28Z | ||
43999ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T10:51:39+01:00 | e5ceb70 | |
5f71403 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T07:17:04+01:00 | aeea2b3 | |
46ce9c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:23:19+01:00 | 0bac071 | |
1730339 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T04:49:30+01:00 | 33211f6 | |
8048a2b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T03:45:41+01:00 | 53d8bb3 | |
2718e18 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T02:35:14+01:00 | b60c5b8 | |
88c770e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T00:18:22+01:00 | 695f656 | |
4e3bd3a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:51:22+01:00 | 08d8742 | |
1645d2e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:28:06+01:00 | 6c790b8 | |
704974b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T18:54:36+01:00 | aa3c53c | |
ef4fbce | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:38:36+01:00 | 662c882 | |
8ba7290 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T10:58:31+01:00 | 597382b | |
27826e1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T01:01:25+01:00 | 1ed1860 | |
597382b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T18:51:23+01:00 | ||
b60c5b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T22:24:11+01:00 | ||
1ed1860 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2022-12-25T11:10:05+01:00 | ||
695f656 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2022-12-11T06:01:44+01:00 | ||
aa3c53c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T04:04:17+01:00 | ||
aeea2b3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 14 | 2022-12-13T14:08:32Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ff1622e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:42:56 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
26ff178 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T21:13:39 | ||
4b34e75 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T13:53:51 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.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_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.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_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.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_cstrcspn-alloca_true-termination.c.i, de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/de88cb9f8af309bfee7e34496a9472de4d446e8ed690818c0d2fc3e900b2d7c4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |