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-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
31ed9ac | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:10:25+01:00 | ||
9be0218 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T12:04:54+01:00 | 31ed9ac | |
f6fc7d9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:56:54+01:00 | ||
0c2d077 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T23:52:25+01:00 | ||
cbddf1e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2023-12-17T01:44:13+01:00 | ||
7ed1c5c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-19T01:36:25+01:00 | ||
2840170 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2023-12-18T02:04:32+01:00 | ||
81ac2ca | 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 | 2023-12-02T12:56:36Z | ||
73ceef7 | 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 | 11 | 2023-11-29T01:58:48Z | ||
2f4d7c6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 5 | 2023-12-19T12:39:39+01:00 | ||
3e5d508 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:39:09+01:00 | ||
39d688d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:29:15Z | ||
ab04937 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2023-12-02T18:24:31Z | ||
e18a91d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T22:29:20Z | ||
9c080bc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T13:08:09Z | ||
bb92021 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 9 | 2023-12-03T01:35:53Z | ||
540fa46 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 7 | 2023-12-01T01:19:52Z | ||
78365c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T14:56:42+01:00 | 30c7e33 | |
b457db9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T04:43:22+01:00 | c9b6e2b | |
b38a37c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T06:08:44+01:00 | 96552ff | |
ee77590 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T11:48:48+01:00 | ab04937 | |
10f4415 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T01:48:39+01:00 | fe49258 | |
0b09412 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:30:27+01:00 | 3e5d508 | |
d9f9fc6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T09:54:48+01:00 | 39d688d | |
e2aa98b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T06:04:41+01:00 | bb92021 | |
18b8d24 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T03:52:16+01:00 | 540fa46 | |
e45d832 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T13:06:02+01:00 | a59cbe6 | |
a59cbe6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T06:35:17+01:00 | ||
3e9194a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T02:28:37+01:00 | e18a91d | |
45a551d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T18:26:26+01:00 | 9c080bc | |
8b4f617 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:16:06+01:00 | 8b6caf4 | |
fe49258 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T20:19:45+01:00 | ||
96552ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2023-12-17T02:12:25+01:00 | ||
30c7e33 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 5 | 2023-12-19T10:48:06+01:00 | ||
c9b6e2b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T18:37:50+01:00 | ||
8b6caf4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2023-11-29T02:50:37Z | ||
534d2c2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:56:27Z | ||
442a0dd | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: b5dd6b8d-f7e5-4abe-b95f-328c03fb04b4 creation_time: '2023-12-03T02:35:53+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5ab00cec-9a57-434b-8829-2cd59b3f010e/sv-benchmarks/c/termination-15/cstrlen_malloc.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5ab00cec-9a57-434b-8829-2cd59b3f010e/sv-benchmarks/c/termination-15/cstrlen_malloc.i : 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:44:29+01:00 | ||
0bfe685 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 8e452983-f735-4b63-83b8-6a507270ab13 creation_time: '2023-12-02T19:24:31+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_469e6193-15e2-4934-9c01-9203349aa688/sv-benchmarks/c/termination-15/cstrlen_malloc.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_469e6193-15e2-4934-9c01-9203349aa688/sv-benchmarks/c/termination-15/cstrlen_malloc.i : 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:03:54+01:00 | ||
d09e001 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 6e8d240e-132a-4112-87d9-da32c0452138 creation_time: '2023-11-29T03:50:37+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f0d915a0-ae45-4b13-9b6c-15688ed09504/sv-benchmarks/c/termination-15/cstrlen_malloc.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f0d915a0-ae45-4b13-9b6c-15688ed09504/sv-benchmarks/c/termination-15/cstrlen_malloc.i : 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T07:49:07+01:00 | ||
20afe3f | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 80ccb972-f2ea-4c17-b711-4741bff50546 creation_time: 2023-12-01T01:19: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-15/cstrlen_malloc.i''' task: input_files: - ../../sv-benchmarks/c/termination-15/cstrlen_malloc.i input_file_hashes: ../../sv-benchmarks/c/termination-15/cstrlen_malloc.i: 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-15/cstrlen_malloc.i file_hash: 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4 line: 367 column: 12 function: cstrlen value: s == p format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T05:11:50+01:00 |
Found 34 witnesses for program sv-benchmarks/c/termination-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b750a00 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:00:34+01:00 | ||
1ee7e03 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T14:18:22+01:00 | b750a00 | |
53d334f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T15:43:35+01:00 | ||
d16effa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T00:04:11+01:00 | ||
96dd875 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2022-12-25T11:38:30+01:00 | ||
e428def | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2022-12-11T01:59:22+01:00 | ||
acaa377 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T04:12:07+01:00 | ||
c4778bc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2022-12-09T03:06:54+01:00 | ||
272b063 | 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 | 10 | 2022-12-14T13:11:53Z | ||
29c7d9d | 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-13T11:55:57Z | ||
4147062 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:05:10+01:00 | ||
600f260 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:59:59Z | ||
2b5384d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2022-12-14T13:30:27Z | ||
3f2f1ce | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:39:31Z | ||
cf99e71 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 9 | 2022-12-14T20:47:14Z | ||
8fbc2dc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 10 | 2022-12-10T07:43:33Z | ||
a9d737d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T10:51:22+01:00 | 2b5384d | |
a6f6105 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T07:31:19+01:00 | bf447ea | |
a4d9173 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:23:20+01:00 | cf99e71 | |
c16dbd0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T03:55:53+01:00 | 3f2f1ce | |
998a3ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T02:50:59+01:00 | 4318113 | |
8d75878 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T00:07:18+01:00 | 76601c6 | |
be75fdb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:50:52+01:00 | 4147062 | |
609665e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:26:59+01:00 | 8fbc2dc | |
d2f2fe2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T18:29:54+01:00 | 8121ab0 | |
570b88b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:38:38+01:00 | 600f260 | |
b162ed9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T11:07:47+01:00 | c53c342 | |
ad8ada8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:53:05+01:00 | b64c099 | |
c53c342 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T19:25:46+01:00 | ||
4318113 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T02:43:52+01:00 | ||
b64c099 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2022-12-25T13:32:41+01:00 | ||
76601c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 5 | 2022-12-11T04:22:50+01:00 | ||
8121ab0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-09T17:43:17+01:00 | ||
bf447ea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2022-12-13T18:53:48Z |
Found 1 witnesses for program sv-benchmarks/c/termination-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c4735aa | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:33:12 |
Found 2 witnesses for program sv-benchmarks/c/termination-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1434dc8 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T23:45:06 | ||
da7e9af | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T13:51:59 |
Found 0 witnesses for program sv-benchmarks/c/termination-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
63e95c3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T20:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-15/cstrlen_malloc_true-termination.c.i, 828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/828f2d43c6fb78b536699442877ab1c5eeed38c7b04fa279d6e864f4ea28e6e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |