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/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i |
programSHA | 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f |
witnessName | results-verified/pesco.2018-12-06_1244.logfiles/sv-comp19_prop-reachsafety.module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.files/witness.graphml |
witnessSHA | 088cc905ddfef79ef20b3c1789c8a68b66410c44ffd426e242a570d886de74c9 |
Key | Value |
architecture | 64bit |
creationtime | 2018-12-08T02:07:21+01:00 |
producer | CPAchecker 1.7-svn b8d6131600+ |
program-sha256 | 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f |
programfile | ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i |
programhash | 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/088cc905ddfef79ef20b3c1789c8a68b66410c44ffd426e242a570d886de74c9.graphml |
witness-sha256 | 088cc905ddfef79ef20b3c1789c8a68b66410c44ffd426e242a570d886de74c9 |
witness-size | 4294810 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 10 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9c8741f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T13:15:19 | ||
088cc90 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4295 | 2018-12-08T02:07:21+01:00 | ||
77465ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4295 | 2018-12-10T20:05:32+01:00 | a46863f | |
846e68e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4295 | 2018-12-09T20:19:36+01:00 | 4f5db2d | |
a806ee1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4295 | 2018-12-08T21:35:22+01:00 | 9c8741f | |
fb1c5a2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4295 | 2018-12-08T05:27:39+01:00 | 088cc90 | |
ea4d3be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4295 | 2018-12-06T09:03:05+01:00 | 87bcbac | |
87bcbac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4295 | 2018-12-05T20:19:28+01:00 | ||
451c28a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4295 | 2018-12-05T14:53:14+01:00 | ef53a09 | |
ef53a09 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29794 | 6665 | 2018-12-05T00:10:40+01:00 |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i, 7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/7d5e6ba534dccbc530b9197f5104a56027789244d5e4d7890f678bc3c351ad5f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |