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/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i |
programSHA | 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58 |
witnessName | results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-memsafety.sll2n_append_equal_true-unreach-call_true-valid-memsafety.i.files/witness.graphml |
witnessSHA | d01f2d2798929143dbe595f14d8b356aeb706945307c995a74311d61f753268a |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T17:41:41.357115 |
producer | DepthK v3.0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_1b4171fa-24a2-45d8-90c7-ef7c63af8323/sv-benchmarks/c/list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i |
programhash | 1c66d86f2cb93b92fe110cb1d9c29158a00f0747 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file | witnessFileByHash/d01f2d2798929143dbe595f14d8b356aeb706945307c995a74311d61f753268a.graphml |
witness-sha256 | d01f2d2798929143dbe595f14d8b356aeb706945307c995a74311d61f753268a |
witness-size | 3507 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.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/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.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/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.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/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 17 witnesses for program sv-benchmarks/c/list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
90deaa6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 12 | 2019-11-30T07:41:56+01:00 | ||
96f2cb2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 12 | 2019-11-30T23:37:47+01:00 | ||
d34a505 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:37 CET (comp) | ||
fa926f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-11T20:38:47+01:00 | 7b216a9 | |
7d81ca1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-11T20:35:00+01:00 | ddb99d0 | |
1ae949e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-11T20:17:35+01:00 | 26cce8d | |
dfe09be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-08T01:09:23+01:00 | 1584efa | |
d2a94a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-08T00:02:30+01:00 | 38196a3 | |
b134d3c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-07T19:54:33+01:00 | b93233c | |
90d1dcf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-06T02:26:54+01:00 | a063088 | |
16e2b45 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-05T19:27:54+01:00 | b68f5af | |
849c06d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-12-04T02:22:12+01:00 | d34a505 | |
d5767f1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-11-30T20:12:18+01:00 | 1f2bd46 | |
5d577ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 12 | 2019-11-30T17:14:32+01:00 | f9a43d6 | |
f9a43d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 37 | 2019-11-30T03:10:32+01:00 | ||
1584efa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 14 | 2019-12-07T22:22:09+01:00 | ||
ddb99d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 13 | 2019-11-30T23:26:37+01:00 |
Found 22 witnesses for program sv-benchmarks/c/list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
55edfe4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T04:22 CET (sv-comp) | ||
91921e3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 12 | 2018-12-07T06:50:48+01:00 | ||
26fb706 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-05T14:49:46+01:00 | ||
7f554f8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T05:39 CET (sv-comp) | ||
50ec26b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T00:33:39 | ||
2288eb9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-06T20:48 CET (sv-comp) | ||
e923005 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 14 | 2018-12-10T17:30:49+01:00 | ||
48fb01f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 41 | 2018-12-06T20:08:26+01:00 | ||
b25c13a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T20:02:49+01:00 | e923005 | |
dd2bfab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-10T10:31:43+01:00 | 9e71dbf | |
96a8008 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T23:12:50+01:00 | 7f554f8 | |
e1b2a3c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T21:48:08+01:00 | 50ec26b | |
7c98530 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T06:16:11+01:00 | 48fb01f | |
f82edc1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T02:50:49+01:00 | 9a86e8d | |
2a04380 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T01:48:38+01:00 | 9e71dbf | |
65f0515 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-07T16:38:10+01:00 | 2288eb9 | |
011c67e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-07T08:53:03+01:00 | 602ae39 | |
8c28fb8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-06T09:28:50+01:00 | ff2b28a | |
4e3959e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T08:57:34+01:00 | 1edc38f | |
007258b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T08:04:51+01:00 | ab2414a | |
33734a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T08:02:25+01:00 | d737317 | |
1edc38f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-05T21:20:41+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.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/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i, 6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6708b9931b9b637c7a50ccf1befdf5df3b457e425dc4aa89a5f79a9f73521b58.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |