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/heap-manipulation/tree_false-unreach-call_false-valid-deref.i |
programSHA | 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-veriabs.2018-12-10_2034.logfiles/sv-comp19_prop-reachsafety.tree_false-unreach-call_false-valid-deref.i.files/witness.graphml |
witnessSHA | 776e210c8534f9c6054239edd7d9b723b12d5da37346894820fb37d1c946250d |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-10T20:38:07+01:00 |
inputwitnesshash | 78476f541e450c5fe8c552482f2340fdd4ce0f481509cb05d5c81bbf8405c621 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4 |
programfile | ../../sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i |
programhash | 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/776e210c8534f9c6054239edd7d9b723b12d5da37346894820fb37d1c946250d.graphml |
witness-sha256 | 776e210c8534f9c6054239edd7d9b723b12d5da37346894820fb37d1c946250d |
witness-size | 16164 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4).
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 22 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
31ab2d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2019-12-01 23:58:15 | ||
5dfd3e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-08T00:07:31+01:00 | ddc2ce8 | |
c5c8034 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 16 | 2019-12-05T20:21:32+01:00 | e801bad | |
e8172ae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 16 | 2019-12-03T08:10:40+01:00 | b0ee3b7 | |
b0ee3b7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 16 | 2019-11-29T18:03:36+01:00 | ||
dbb05f4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 16 | 2019-12-01T00:53:15+01:00 | ||
03534e6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-11T21:55:19+01:00 | 7d867c3 | |
ad18b2c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-11T21:09:39+01:00 | 31ab2d3 | |
ac5f469 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 07:23:12 | ||
8bd78fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T21:58:06+01:00 | 681457f | |
10f0820 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T21:40:12+01:00 | f31078c | |
7cc4637 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 17 | 2019-12-05T20:20:42+01:00 | cf4bbb8 | |
30423f3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-03T08:56:51+01:00 | 94f12f8 | |
7026e7c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-03T08:10:37+01:00 | 72428fe | |
72428fe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 15 | 2019-11-29T16:44:30+01:00 | ||
69e2538 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 13 | 2019-12-07T15:06:38+01:00 | ||
681457f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 15 | 2019-11-30T23:14:09+01:00 | ||
9c74b70 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T21:09:31+01:00 | ac5f469 | |
a19d64d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T20:54:21+01:00 | 72b1591 | |
3fd4246 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T20:44:26+01:00 | 3fb1040 | |
bab4108 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-08T01:52:08+01:00 | 69e2538 | |
d688905 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-08T00:06:52+01:00 | df49d78 |
Found 27 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
230de16 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:22:54+01:00 | c10a716 | |
30cf8d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T10:21:00+01:00 | 9e33870 | |
4b02185 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T22:10:24+01:00 | 31fa444 | |
25a953c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T09:12:45+01:00 | 02a9688 | |
31fa444 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-07T20:23:29 | ||
15cbfe6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:39:28+01:00 | 759aaf2 | |
03647bc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-08T05:00:39+01:00 | d5fa1cb | |
a3627e6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T04:08:08+01:00 | 73722ea | |
a4cbd7f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T09:09:28+01:00 | bf99eb2 | |
8926360 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-05T22:36:12+01:00 | ||
a34e2be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T03:59 CET (sv-comp) | ||
bd772f6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 4 | 2018-12-08T05:14:05 | ||
78476f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 13 | 2018-12-10T17:30:01+01:00 | ||
c915809 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 14 | 2018-12-08T03:28:32+01:00 | ||
f798af7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:39:39+01:00 | 41aa7ae | |
b333c2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:35:02+01:00 | b7fdd0a | |
09f6a11 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T08:46:06+01:00 | c915809 | |
ef8ae87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T04:51:48+01:00 | 2a271ab | |
533af32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 18 | 2018-12-06T10:12:00+01:00 | e11599c | |
e921eec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T09:48:01+01:00 | c807a81 | |
81d8808 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T09:12:22+01:00 | 53db481 | |
c807a81 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-05T17:32:11+01:00 | ||
776e210 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-10T20:38:07+01:00 | 78476f5 | |
ba7d1c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:53:10+01:00 | ee0cadb | |
c2869eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T18:19:48+01:00 | a54314c | |
3566617 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T23:43:26+01:00 | a34e2be | |
ba8dcf5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T22:10:31+01:00 | bd772f6 |
Found 21 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
39eb909 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:08 CET (sv-comp) | ||
6a139c6 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 6 | 2017-12-02T11:10:19.678040 | ||
3c3d498 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T23:29:47.694296 | ||
f047427 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T09:24 CET (sv-comp) | ||
d75a59a | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 16 | 2017-12-03T03:48Z | ||
d3cd8ce | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 42 | 2017-12-01T08:23 CET (sv-comp) | ||
78e3a73 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 16 | 2017-12-03T04:06Z | ||
02a9688 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 5 | 2017-12-01T22:16 CET (sv-comp) | ||
fdc987f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:39 CET (sv-comp) | ||
b3e04d9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-01T22:55 CET (sv-comp) | ||
01a86a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T21:30 CET (sv-comp) | ||
6b5ac02 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 15 | 2017-12-02T12:01Z | ||
22b232d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 6 | 2017-12-01T22:03:53.148914 | ||
e5bdb0e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 6 | 2017-12-01T07:49:54.321980 | ||
d2a19f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-11-30T19:31 CET (sv-comp) | ||
b7509fb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-11-30T19:04:47+01:00 | ||
fb00309 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 20 | 2017-12-01T01:05:51+01:00 | ||
cd6c9a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 12 | 2017-11-30T22:07:41+01:00 | ||
e902816 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 14 | 2017-12-02T08:01:41+01:00 | ||
973df16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 13 | 2017-12-01T00:53 CET (sv-comp) | ||
2224324 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 15 | 2017-12-02T08:09Z |
Found 0 witnesses for program sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i, 219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/219b024195f4bee3b0c05567d84c18481f53dfb42dca03a02e31f84d5a2d73e4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |