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 35 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
de1dd38 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:46:45+01:00 | ||
b96002e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-30T00:29:58Z | ||
d74e631 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:05:33+01:00 | de1dd38 | |
52af73a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T07:52:48+01:00 | ||
d49d884 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T20:35:32+01:00 | ||
cbc6efd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T17:05:36+01:00 | ||
28103c7 | 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 | 22 | 2023-12-02T11:39:33Z | ||
a3fbd19 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | PredatorHP | 4 | 2023-11-30T08:25:09Z | ||
5c2b536 | 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-29T06:36:13Z | ||
7b37672 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 22 | 2023-12-03T03:39:04Z | ||
4aaa3d1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 42 | 2023-12-01T02:06:19Z | ||
39e1f35 | 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 | 22 | 2023-11-28T19:35:09Z | ||
83667f9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:51:23+01:00 | ||
ba78c6d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:49:44Z | ||
6134987 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 18 | 2023-12-02T11:53:13Z | ||
01e4a05 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 18 | 2023-12-02T22:01:19Z | ||
963b1eb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T14:34:37+01:00 | e5f1a25 | |
3b8f884 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T04:35:09+01:00 | 7afb4f6 | |
3b9a317 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:08:48+01:00 | 3745ee2 | |
b030716 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:47:22+01:00 | 6134987 | |
243428a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T02:05:32+01:00 | c881af2 | |
fbfe917 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:29:38+01:00 | 83667f9 | |
d949657 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T09:54:43+01:00 | ba78c6d | |
82e33fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:47:01+01:00 | 01e4a05 | |
b8be6a4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T13:07:51+01:00 | 2f0279a | |
2f0279a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T02:07:31+01:00 | ||
af9c654 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:07:09+01:00 | 9da7cee | |
c881af2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T18:08:25+01:00 | ||
3745ee2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2023-12-17T00:10:51+01:00 | ||
7afb4f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T16:47:29+01:00 | ||
9da7cee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 18 | 2023-11-29T04:29:50Z | ||
64728b0 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: bfddb3db-86d4-48db-9145-686980f009c9 creation_time: '2023-12-02T23:01: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_2c03b3c7-edc5-469b-a7e7-022edc4c0d8f/sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2c03b3c7-edc5-469b-a7e7-022edc4c0d8f/sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i : 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:39:20+01:00 | ||
e8d7dfa | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 9e88aa42-8759-436f-9cdf-8252029389c9 creation_time: '2023-11-29T05:29:51+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2cbf6910-12d2-48cf-ad26-d7ea15febacd/sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2cbf6910-12d2-48cf-ad26-d7ea15febacd/sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i : 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T07:46:56+01:00 | ||
a887341 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 97dad1a7-9583-4046-888d-818e765862ec creation_time: '2023-12-02T12:53:13+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_85bd23e7-fadc-411a-adf5-a7dbc5c4c9b8/sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_85bd23e7-fadc-411a-adf5-a7dbc5c4c9b8/sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i : 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T11:54:17+01:00 | ||
523790f | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: ddec7412-3db6-4ae8-8afd-34528d284309 creation_time: 2023-12-01T01:42: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/b.03_assume-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca.i: 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-01T04:51:38+01:00 |
Found 28 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e83362d | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:10:42+01:00 | ||
c215047 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:18:00+01:00 | e83362d | |
e148d0b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T18:59:14+01:00 | ||
620f795 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T23:26:22+01:00 | ||
bd72d61 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T03:53:23+01:00 | ||
afd7fa2 | 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 | 21 | 2022-12-14T06:29:21Z | ||
34a6966 | 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 | 2022-12-11T10:37:18Z | ||
54a49c4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 21 | 2022-12-14T17:20:33Z | ||
ca9b6dc | 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 | 20 | 2022-12-13T13:26:43Z | ||
aa18157 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:03:05+01:00 | ||
3508c9b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:10:17Z | ||
2ed058e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 17 | 2022-12-14T13:17:27Z | ||
058ee70 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 17 | 2022-12-14T21:37:05Z | ||
db9cf73 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:09:40+01:00 | 2ed058e | |
d49d4de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T07:40:33+01:00 | 9ce923b | |
779e2de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:23:11+01:00 | 058ee70 | |
857fb70 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T02:33:16+01:00 | a2c097e | |
1fe9965 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T00:06:28+01:00 | 0c074c7 | |
1e6fa04 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:50:29+01:00 | aa18157 | |
f897ccf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T18:50:13+01:00 | a3ea21f | |
153678a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:38:17+01:00 | 3508c9b | |
22f48a3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T10:54:26+01:00 | fe4f874 | |
4306e82 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T01:01:07+01:00 | 798d7d1 | |
fe4f874 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T19:03:04+01:00 | ||
a2c097e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T21:44:07+01:00 | ||
798d7d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2022-12-25T07:20:11+01:00 | ||
a3ea21f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T02:09:53+01:00 | ||
9ce923b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 17 | 2022-12-13T11:32:40Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a19e4bc | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:01:17 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e1b71a3 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:29:02 | ||
b1d51a2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:46:38 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.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/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
028996a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T20:20 CET (sv-comp) | ||
0fa8d4f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 28 | 2017-12-01T11:47 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.03_assume-alloca_true-termination_true-no-overflow.c.i, 1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1dfda05d3675e1795581ea2bc298236cc0d085a96432f97caff9d055d75a6052.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |