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/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i |
programSHA | 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751 |
witnessName | results-verified/smack.2018-12-07_1913.logfiles/sv-comp19_prop-memsafety.sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml |
witnessSHA | 42a56a4db0307603f28f65aebe0b1edb6c67586d72895436d3f25a2103f5e26e |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T10:25:12 |
producer | SMACK 1.9.3 |
program-sha256 | 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_f0cb404b-5a08-430e-844a-742088cdfdcd/sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i |
programhash | 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memcleanup) ) |
witness-file | witnessFileByHash/42a56a4db0307603f28f65aebe0b1edb6c67586d72895436d3f25a2103f5e26e.graphml |
witness-sha256 | 42a56a4db0307603f28f65aebe0b1edb6c67586d72895436d3f25a2103f5e26e |
witness-size | 3289 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751).
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 22 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a0f15ba | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2019-12-02 04:11:45 | ||
67aa82c | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-11T21:50:26+01:00 | 65a3f79 | |
e2d7dbb | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 12 | 2019-12-11T21:09:03+01:00 | a0f15ba | |
2d1f0b2 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-08T00:07:37+01:00 | 7f42477 | |
7329ae9 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-07T21:14:50+01:00 | 6fa8401 | |
cac0195 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-03T08:09:42+01:00 | 79aeec1 | |
79aeec1 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-11-30T14:09:22+01:00 | ||
65a3f79 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 10 | 2019-11-30T20:55:45+01:00 | ||
87c48a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 18:13:48 | ||
4638e5e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T21:47:33+01:00 | 0e42b1b | |
0921d86 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T21:45:39+01:00 | 8126286 | |
c4595db | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-08T00:06:02+01:00 | 4e6947b | |
395d8fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-07T21:17:22+01:00 | cc4c869 | |
da7a8ab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-03T08:57:31+01:00 | b4a19e2 | |
cfda812 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-03T08:10:02+01:00 | e01464a | |
e01464a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 16 | 2019-11-30T01:42:12+01:00 | ||
b90aa70 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 7 | 2019-12-07T14:41:18+01:00 | ||
8126286 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 16 | 2019-11-30T21:27:24+01:00 | ||
d12ef21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-11T21:09:18+01:00 | 87c48a5 | |
ceb9c38 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-11T20:45:54+01:00 | 9eb58fd | |
d32cfd0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-08T01:51:19+01:00 | b90aa70 | |
868fa26 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-05T20:21:48+01:00 | 5f2edce |
Found 29 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e7c519b | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:35 CET (sv-comp) | ||
42a56a4 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T10:25:12 | ||
cbcdc34 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T23:44:42+01:00 | e7c519b | |
3b1604a | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T22:09:47+01:00 | 42a56a4 | |
68fb635 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T09:14:58+01:00 | 8a77f61 | |
05af135 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T10:17:20+01:00 | 8316090 | |
ffbbd93 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:48:20+01:00 | dc1a4d3 | |
dc1a4d3 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-05T13:41:08+01:00 | ||
3406397 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T09:20:13+01:00 | 334a77b | |
525739b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T04:07 CET (sv-comp) | ||
39f4e30 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T11:45:21 | ||
0cf7c9d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 7 | 2018-12-10T18:14:40+01:00 | ||
c6036a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 16 | 2018-12-07T11:00:48+01:00 | ||
3497672 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-10T10:48:53+01:00 | fc79e00 | |
a6180cd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:39:37+01:00 | a131153 | |
16aad16 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:26:04+01:00 | b32293e | |
5f7f9c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T22:07:32+01:00 | 39f4e30 | |
0f12999 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T08:17:56+01:00 | c6036a0 | |
93a5f79 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T04:59:00+01:00 | 5c65b81 | |
0428ef4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T03:44:12+01:00 | fc79e00 | |
5aa566e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-07T09:28:26+01:00 | e23eab4 | |
b4ef143 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T10:18:31+01:00 | ab9f9db | |
455f96f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T09:48:47+01:00 | 503d449 | |
03ae420 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T09:19:39+01:00 | 2107cbb | |
503d449 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T01:44:09+01:00 | ||
48345d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-10T20:35:00+01:00 | 0cf7c9d | |
267f743 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-09T18:23:08+01:00 | ad9f391 | |
3ef4984 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-08T23:43:10+01:00 | 525739b | |
1202b85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-07T01:09:31+01:00 | cc9f011 |
Found 13 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cecb261 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T06:02 CET (sv-comp) | ||
e23eab4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 5 | 2017-12-01T20:24 CET (sv-comp) | ||
0354ac2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T20:40 CET (sv-comp) | ||
27c6e0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 14 | 2017-12-02T08:25Z | ||
ede7017 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Forester | 8 | 2017-12-01T17:47 CET (sv-comp) | ||
536e4e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 6 | 2017-12-01T22:26:54.017662 | ||
64f2648 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 6 | 2017-12-01T17:32:11.437240 | ||
b3d2ac9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T04:37 CET (sv-comp) | ||
13d9fa1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 14 | 2017-12-01T01:04:23+01:00 | ||
17f720d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 23 | 2017-11-30T13:34:09+01:00 | ||
a6d6689 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-12-01T02:39:19+01:00 | ||
991371d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 12 | 2017-11-30T17:45 CET (sv-comp) | ||
cfe9433 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 14 | 2017-12-02T13:41Z |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i, 913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/913b97cfe4f6fdcc0739b6d9570a857b7ac829e7240d60a6e67e408efd533751.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |