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).
Key | Value |
programName | sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i |
programSHA | 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0 |
witnessName | results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-memsafety.dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i.files/witness.graphml |
witnessSHA | cfdb3dc5e843551bca1cc87616523bd8e7270ebccac48a4ddce36c2b7016efb4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T02:26 CET (sv-comp) |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | CBMC |
programfile | ../../sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i |
programhash | cfdde8b1798318c3bb26b76a748741913b280952 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/cfdb3dc5e843551bca1cc87616523bd8e7270ebccac48a4ddce36c2b7016efb4.graphml |
witness-sha256 | cfdb3dc5e843551bca1cc87616523bd8e7270ebccac48a4ddce36c2b7016efb4 |
witness-size | 43158 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 20 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fb155b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-11-29T19:31:56+01:00 | ||
1032e36 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 13 | 2019-12-01T02:10:28+01:00 | ||
cc048f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T23:12 CET (comp) | ||
1d6b604 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:19:47+01:00 | 844c13e | |
29b9fa7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:17:16+01:00 | 0485118 | |
8c028c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:08:02+01:00 | 024d0be | |
71012b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:02:24+01:00 | 02a55f1 | |
73aa208 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-08T00:59:30+01:00 | aad3fa1 | |
68c7321 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T23:45:44+01:00 | 0196caa | |
be74e2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T23:39:55+01:00 | 1114ef6 | |
e04fbd5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-07T19:45:24+01:00 | d048edc | |
69ad586 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-06T02:08:16+01:00 | 7ffe55e | |
fdce832 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T19:12:47+01:00 | 6e84dfd | |
e885984 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T19:03:12+01:00 | baeb9c5 | |
aeb68f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-04T02:07:50+01:00 | cc048f5 | |
f8f8e9c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-11-30T19:07:39+01:00 | 5594376 | |
8ef5cbc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-11-30T17:04:13+01:00 | 8356fe8 | |
8356fe8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 14 | 2019-11-29T16:24:30+01:00 | ||
aad3fa1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 14 | 2019-12-07T11:23:33+01:00 | ||
024d0be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 15 | 2019-12-01T18:06:19+01:00 |
Found 26 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c089244 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T12:31 CET (sv-comp) | ||
4aa51d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-05T09:38:40+01:00 | ||
70b2c37 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 13 | 2018-12-07T12:29:17+01:00 | ||
efd0e45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:10 CET (sv-comp) | ||
bb5deca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T17:20:34 | ||
029579e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-06T23:54 CET (sv-comp) | ||
af88994 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-06T21:27:29+01:00 | ||
a9fb3c7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T20:06:36+01:00 | ce13fb7 | |
8584994 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T10:30:48+01:00 | d17a7c8 | |
a9148c3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:31:53+01:00 | e2604cc | |
9999dcb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:12:29+01:00 | 6e42ff4 | |
77830b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T19:47:54+01:00 | e05bbf4 | |
14aaabb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:21:09+01:00 | efd0e45 | |
822c2c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T21:32:45+01:00 | bb5deca | |
996b623 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T06:42:53+01:00 | af88994 | |
5e8605d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T02:58:31+01:00 | d17a7c8 | |
14f297d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T02:49:23+01:00 | 8e95cc0 | |
e2febe4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T17:44:02+01:00 | 5a69854 | |
806b63a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T16:39:22+01:00 | 029579e | |
0299071 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T08:28:46+01:00 | fd171d0 | |
9ec1f71 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:28:55+01:00 | 3296366 | |
47f4aaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:11:05+01:00 | 34b3c8b | |
0cc8ef4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T08:19:38+01:00 | 52d280e | |
1fdcd95 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T08:18:19+01:00 | 15146ef | |
34b3c8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T07:51:42+01:00 | ||
9430d0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T07:05:06+01:00 | 37d38d2 |
Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i, 8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8614ddc5f0c2b457a16fef06e86e73c0ad96dbd510947d66891be609ebdee9f0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |