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-queue_false-unreach-call_false-valid-memcleanup.i |
programSHA | 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6 |
witnessName | results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.sll-queue_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml |
witnessSHA | 6d1d78226473c1f4473c117d530f9755f0ad953dbe9206b38dee02515eca5aa1 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T20:26:23+01:00 |
producer | CPAchecker 1.6.1-svn 26725 |
program-sha256 | 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6 |
programfile | ../../sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i |
programhash | e5083763cd1026dac92f37bc5a05779baf01a71b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/6d1d78226473c1f4473c117d530f9755f0ad953dbe9206b38dee02515eca5aa1.graphml |
witness-sha256 | 6d1d78226473c1f4473c117d530f9755f0ad953dbe9206b38dee02515eca5aa1 |
witness-size | 5242 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.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-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
59e2685 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 2 | 2019-12-01 13:50:57 | ||
c9c4e46 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 20 | 2019-12-11T21:50:22+01:00 | 9c5541d | |
53a548e | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 21 | 2019-12-11T21:09:09+01:00 | 59e2685 | |
07bd561 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 20 | 2019-12-08T00:07:36+01:00 | b5c0fac | |
7b519f5 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 20 | 2019-12-03T08:08:37+01:00 | ac5ebd4 | |
ac5ebd4 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 19 | 2019-11-30T04:01:55+01:00 | ||
9c5541d | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 19 | 2019-12-01T16:39:39+01:00 | ||
c0be9a0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-01 23:35:22 | ||
e4db163 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-11T21:45:10+01:00 | 2d3772c | |
f06d82a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-11T20:55:11+01:00 | c631585 | |
5b3ed24 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-08T00:06:06+01:00 | f9cfa9c | |
ea92810 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-07T21:16:58+01:00 | d4f88b2 | |
d6acd20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 24 | 2019-12-03T08:56:54+01:00 | 6dffe2a | |
d0baf3e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 26 | 2019-11-30T13:26:39+01:00 | ||
6f643d7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 8 | 2019-12-07T12:03:30+01:00 | ||
744b156 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 26 | 2019-12-01T06:27:49+01:00 | ||
4afdb58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-11T21:40:24+01:00 | 744b156 | |
510ef77 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-11T21:09:25+01:00 | c0be9a0 | |
b80fbd1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-11T20:45:59+01:00 | d30b2f5 | |
f1c7e76 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-08T01:51:46+01:00 | 6f643d7 | |
9dcafc7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-05T20:20:13+01:00 | 2a72d7a | |
8787137 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-03T08:08:46+01:00 | d0baf3e |
Found 29 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
61164d9 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2018-12-08T11:16 CET (sv-comp) | ||
4ee312e | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T15:51:19 | ||
a634d21 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-08T23:42:23+01:00 | 61164d9 | |
a640ad3 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-08T22:10:48+01:00 | 4ee312e | |
035c624 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-07T09:26:52+01:00 | 3db8ce3 | |
a296c1d | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-06T10:19:10+01:00 | 9aaa724 | |
c167de0 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 19 | 2018-12-06T09:48:54+01:00 | 29d9b79 | |
29d9b79 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 22 | 2018-12-06T05:23:05+01:00 | ||
cce89fe | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:18:33+01:00 | b48a4fb | |
a54df21 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T10:34 CET (sv-comp) | ||
5f7be1b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T19:26:30 | ||
fd24fba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 8 | 2018-12-10T19:03:28+01:00 | ||
ccd0fdb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 25 | 2018-12-07T23:01:06+01:00 | ||
d2b8bcf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-10T10:48:49+01:00 | 63bb772 | |
2fa1710 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-09T20:37:54+01:00 | 058cb3f | |
6730d4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-09T20:18:45+01:00 | d33c6a3 | |
e28c323 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-08T22:10:53+01:00 | 5f7be1b | |
c1bbe00 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-08T04:53:00+01:00 | 0e5c529 | |
646c38e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-08T04:26:16+01:00 | 63bb772 | |
463154b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-07T09:13:10+01:00 | 159eca1 | |
8a204c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T10:19:14+01:00 | f179af7 | |
0f30ad9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 23 | 2018-12-06T09:08:41+01:00 | ed82537 | |
4b5a4fc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 25 | 2018-12-05T22:39:49+01:00 | ||
7bd241c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-10T20:36:17+01:00 | fd24fba | |
dc56ef7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-09T18:21:35+01:00 | fe2057b | |
7f8dfe8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T23:43:14+01:00 | a54df21 | |
e2d634e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T08:49:16+01:00 | ccd0fdb | |
6af62e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-07T01:22:27+01:00 | 048e9c9 | |
9871f1e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:48:37+01:00 | 4b5a4fc |
Found 11 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
19986d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T07:40 CET (sv-comp) | ||
159eca1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 6 | 2017-12-01T20:46 CET (sv-comp) | ||
050a1a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 21 | 2017-12-02T10:01Z | ||
4180031 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Forester | 12 | 2017-12-01T17:45 CET (sv-comp) | ||
d88a46a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 6 | 2017-12-01T20:26:06.684831 | ||
a627b22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T13:52:19.303359 | ||
43a4a68 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-11-30T22:44 CET (sv-comp) | ||
5cdc9d8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 24 | 2017-11-30T16:55:49+01:00 | ||
6d1d782 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-11-30T20:26:23+01:00 | ||
55ae228 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 16 | 2017-12-02T13:16:41+01:00 | ||
8123ad6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 19 | 2017-11-30T11:25 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i, 1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1b7bfff579d3ec79008d5257a9571809d6e472d6bba721261e7093b8662050c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |