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 32 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2e02874 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:35:27+01:00 | ||
dbf009e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:27:10Z | ||
389f111 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-18T12:06:15+01:00 | 2e02874 | |
2c44e4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T05:09:27+01:00 | ||
2f28351 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-03T21:24:57+01:00 | ||
a991611 | 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 | 24 | 2023-12-02T16:14:04Z | ||
4dc3e21 | 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:26:06Z | ||
5089bfb | 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-29T11:35:49Z | ||
75b87a2 | 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 | 24 | 2023-12-03T01:01:28Z | ||
9aeeeb6 | 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) | 43 | 2023-12-01T01:39:35Z | ||
f2da096 | 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 | 24 | 2023-11-28T19:36:49Z | ||
fb2d8a4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-19T01:20:48+01:00 | ||
bdf5045 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:49:03+01:00 | ||
f7f86d2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T08:05:47Z | ||
f91feb0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 21 | 2023-12-02T18:18:00Z | ||
6c883e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-19T14:30:10+01:00 | de87087 | |
cef27ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-19T05:08:50+01:00 | 3e1eb91 | |
0570bff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-17T06:05:00+01:00 | ec23326 | |
11b10dd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T11:45:49+01:00 | f91feb0 | |
a5f78a0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T01:16:47+01:00 | f7e83ac | |
a511e56 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T18:29:45+01:00 | bdf5045 | |
373ebdd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T09:54:27+01:00 | f7f86d2 | |
94c8a1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T12:34:26+01:00 | 2c010f2 | |
2c010f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T06:20:39+01:00 | ||
6a78e40 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T08:15:44+01:00 | f5a8866 | |
f7e83ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-04T00:41:02+01:00 | ||
ec23326 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2023-12-17T01:39:21+01:00 | ||
3e1eb91 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-18T21:08:38+01:00 | ||
f5a8866 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 20 | 2023-11-28T23:19:41Z | ||
c7142fd | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: a0cdb15f-be18-4f84-9336-2e78c1101985 creation_time: 2023-12-02T19:18+01:00 producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_85c220b9-1042-466b-be9e-41bf7bb29359/sv-benchmarks/c/termination-memory-alloca/b.18-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_85c220b9-1042-466b-be9e-41bf7bb29359/sv-benchmarks/c/termination-memory-alloca/b.18-alloca.i : 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T11:56:47+01:00 | ||
8f46624 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 27d004e3-c641-4851-9659-63c843ba52c8 creation_time: '2023-11-29T00:19:41+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2c437136-104f-479f-9073-c10beef29c57/sv-benchmarks/c/termination-memory-alloca/b.18-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2c437136-104f-479f-9073-c10beef29c57/sv-benchmarks/c/termination-memory-alloca/b.18-alloca.i : 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-29T07:43:12+01:00 | ||
ec8fe04 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 8ce39e8d-6b81-4025-a33d-0e90a4ff259b creation_time: 2023-12-01T01:57:05Z 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.18-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/b.18-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/b.18-alloca.i: 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-01T05:18:35+01:00 |
Found 26 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7203697 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:32:39+01:00 | ||
93f5992 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T14:19:45+01:00 | 7203697 | |
d017416 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T21:28:59+01:00 | ||
94baa7a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-12T01:01:47+01:00 | ||
28cab73 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T02:52:04+01:00 | ||
abc35ef | 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 | 23 | 2022-12-14T14:01:39Z | ||
17a8b07 | 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-11T12:21:14Z | ||
bd306d1 | 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 | 23 | 2022-12-15T02:44:25Z | ||
23b7d7b | 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 | 23 | 2022-12-13T16:09:51Z | ||
dcbc74b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:18:30+01:00 | ||
dcd2c7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T12:50:59Z | ||
632f131 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 22 | 2022-12-14T04:49:03Z | ||
0076836 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T10:51:46+01:00 | 632f131 | |
ada3ac0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T07:27:27+01:00 | 04baafd | |
931cc3a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T03:08:07+01:00 | 986fc9e | |
b4367c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T00:06:24+01:00 | db0f0e9 | |
61d2346 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T22:51:47+01:00 | dcbc74b | |
8779f7e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T17:58:31+01:00 | 684da83 | |
9f7bf24 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T17:38:18+01:00 | dcd2c7f | |
83c59cf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T11:39:48+01:00 | 08de6b4 | |
9f0ed2b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T00:48:25+01:00 | 5d315f4 | |
08de6b4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T18:43:05+01:00 | ||
986fc9e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-12T00:43:34+01:00 | ||
5d315f4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2022-12-25T12:43:18+01:00 | ||
684da83 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T01:44:16+01:00 | ||
04baafd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 22 | 2022-12-13T14:54:10Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ed79acb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:22:51 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e277904 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T14:34:45 | ||
c8edb4c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T13:48:49 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.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.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.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.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8db0095 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 9 | 2017-12-01T15:34 CET (sv-comp) | ||
02626d1 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 29 | 2017-12-01T15:22 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/b.18-alloca_true-termination_true-no-overflow.c.i, 64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/64e9a02fe4d55a12958b5de8c28c6c0ab007c7a3dc976261fd9d4ec11bf5feff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |