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_remove_all_reverse_true-unreach-call_true-valid-memsafety.i |
programSHA | 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62 |
witnessName | results-verified/predatorhp.2018-12-07_0408.logfiles/sv-comp19_prop-memsafety.sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i.files/witness.graphml |
witnessSHA | 4d8de1f475c05f813744690a87deaf86705d33aac9532d9e1738ee31001b9165 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T05:49 CET (sv-comp) |
error-specification-length | Key 'specification' longer than 100 characters. |
memorymodel | precise |
producer | PredatorHP |
programfile | ../../sv-benchmarks/c/list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i |
programhash | 13cb8f020c937b6a3b0b6c39b85904cffb8b3ba5 |
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/4d8de1f475c05f813744690a87deaf86705d33aac9532d9e1738ee31001b9165.graphml |
witness-sha256 | 4d8de1f475c05f813744690a87deaf86705d33aac9532d9e1738ee31001b9165 |
witness-size | 3664 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.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_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.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_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.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_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
945e456 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 10 | 2019-12-01T17:14:50+01:00 | ||
0749ea4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 10 | 2019-11-30T12:06:56+01:00 | ||
1cfe5b3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-04T00:29 CET (comp) | ||
6e488ec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-11T20:27:56+01:00 | 7f8d65a | |
5369781 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-11T20:17:33+01:00 | b1dd8e8 | |
f515bd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-11T20:09:47+01:00 | 0238464 | |
4b48ba5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-11T20:02:35+01:00 | 5814d52 | |
f8f833a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-08T00:36:48+01:00 | 07a2f50 | |
c00dd88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-07T23:46:09+01:00 | e5d25c1 | |
4b3388d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-07T19:41:43+01:00 | 30c8150 | |
71ebbbc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-06T02:15:33+01:00 | 718ce69 | |
31d00bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-05T19:13:11+01:00 | 221788f | |
add2ba5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-04T02:07:56+01:00 | 1cfe5b3 | |
74c0831 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-11-30T19:50:24+01:00 | b58fe82 | |
213fa41 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-11-30T16:21:34+01:00 | d560840 | |
d560840 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 12 | 2019-11-29T23:27:27+01:00 | ||
07a2f50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 11 | 2019-12-07T14:09:34+01:00 | ||
0238464 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 12 | 2019-12-01T06:40:57+01:00 |
Found 24 witnesses for program sv-benchmarks/c/list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9bc86c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-07T22:58 CET (sv-comp) | ||
d0aa41f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T07:34:31+01:00 | ||
86db087 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T20:21:47+01:00 | ||
e92a385 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T06:43 CET (sv-comp) | ||
a6c4f12 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T05:59:48 | ||
59e1d03 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T01:33 CET (sv-comp) | ||
1cced0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 11 | 2018-12-10T18:11:23+01:00 | ||
688eaf2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 12 | 2018-12-07T01:28:58+01:00 | ||
8d2b21b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-10T19:45:54+01:00 | 1cced0f | |
c5ba168 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-10T10:31:26+01:00 | 45019fe | |
080de65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-09T20:12:06+01:00 | ab7e498 | |
b981b21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-09T19:56:23+01:00 | a3103db | |
a07ee14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T23:10:13+01:00 | e92a385 | |
0cad1f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T21:49:45+01:00 | a6c4f12 | |
48c0b98 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-08T06:40:32+01:00 | 688eaf2 | |
da46a5b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T04:30:12+01:00 | f182104 | |
6910cd6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T01:56:22+01:00 | 45019fe | |
b71e3f7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-07T16:38:52+01:00 | 59e1d03 | |
b59897b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-07T08:09:25+01:00 | 577b56c | |
460ab1f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:28:19+01:00 | 42f84db | |
2435fa5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T08:55:28+01:00 | 874085c | |
44607fa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T07:49:33+01:00 | 9315527 | |
9dc70de | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T07:46:43+01:00 | 6628f48 | |
874085c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-05T20:04:34+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.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_remove_all_reverse_true-unreach-call_true-valid-memsafety.i, 2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2b06caf525a4b8b82cb7f3cc300bcd495a022e60617d702db2ecf4c94af30c62.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |