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_false-unreach-call.cil.out.i |
programSHA | 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-cpa-bam-bnb.2018-12-05_1542.logfiles/sv-comp19_prop-reachsafety.module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i.files/witness.graphml |
witnessSHA | 7bf05ac39a5a0d5c834a32545610f8eadcecd47c2550747162f92f4c3d0dcbbd |
Key | Value |
architecture | 64bit |
creationtime | 2018-12-05T16:12:33+01:00 |
inputwitnesshash | ad7f7eecdba1825715867783253b3c9a0849f06d53e38c010f68349f6af04074 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe |
programfile | ../../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i |
programhash | 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/7bf05ac39a5a0d5c834a32545610f8eadcecd47c2550747162f92f4c3d0dcbbd.graphml |
witness-sha256 | 7bf05ac39a5a0d5c834a32545610f8eadcecd47c2550747162f92f4c3d0dcbbd |
witness-size | 16518 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe).
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 12 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
22f20e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 6 | 2018-12-08T04:35:04 | ||
bb5dd5f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 23 | 2018-12-10T17:46:59+01:00 | ||
8206d24 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 19 | 2018-12-07T09:25:26+01:00 | ||
95d3334 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-10T20:36:51+01:00 | bb5dd5f | |
c28b903 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-08T22:11:02+01:00 | 22f20e6 | |
865f139 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-08T08:42:48+01:00 | 8206d24 | |
1907540 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-08T05:01:34+01:00 | 0dfea1f | |
84f4267 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-06T09:48:22+01:00 | c690046 | |
be802ad | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 37 | 2018-12-06T09:19:19+01:00 | e544cb5 | |
c690046 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-05T18:05:09+01:00 | ||
7bf05ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-05T16:12:33+01:00 | ad7f7ee | |
ad7f7ee | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29794 | 18 | 2018-12-05T05:49:52+01:00 |
Found 0 witnesses for program sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.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_false-unreach-call.cil.out.i, 0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0240a58a1d211714124d2332b7d89f99342c5992fcca90758b3f3499b856a5fe.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |